\documentclass[10pt,a4paper,oneside,ngerman,numbers=noenddot]{scrartcl}
\usepackage[T1]{fontenc}
\usepackage[utf8x]{inputenc}
\usepackage[ngerman]{babel}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{paralist}
\usepackage{gauss}
\usepackage{pgfplots}
\usepackage[locale=DE,exponent-product=\cdot,detect-all]{siunitx}
\usepackage{tikz}
\usetikzlibrary{automata,matrix,fadings,calc,positioning,decorations.pathreplacing,arrows,decorations.markings,petri,shapes}
\usepackage{polynom}
\usepackage{multirow}
\usepackage[german]{fancyref}
\usepackage{morefloats}
\usepackage{lmerge}
\polyset{style=C, div=:,vars=x}
\pgfplotsset{compat=1.8}
\pagenumbering{arabic}
% ensures that paragraphs are separated by empty lines
\parskip 12pt plus 1pt minus 1pt
\parindent 0pt
% define how the sections are rendered
\def\thesection{13.\arabic{section})}
\def\thesubsection{\arabic{subsection}.}
\def\thesubsubsection{(\alph{subsubsection})}
% some matrix magic
\makeatletter
\renewcommand*\env@matrix[1][*\c@MaxMatrixCols c]{%
  \hskip -\arraycolsep
  \let\@ifnextchar\new@ifnextchar
  \array{#1}}
\makeatother

\tikzset{
    place/.style={
        circle,
        thick,
        draw=black,
        fill=white,
        minimum size=6mm,
        font=\bfseries
    },
    transitionH/.style={
        rectangle,
        thick,
        draw=black,
        fill=white,
        minimum width=8mm,
        inner ysep=4pt,
        font=\bfseries
    },
    transitionV/.style={
        rectangle,
        thick,
        fill=black,
        minimum height=8mm,
        inner xsep=2pt
    }
}

\renewcommand{\vec}[1]{\underline{#1}}

\begin{document}
\author{Benjamin Kuffel, Jim Martens\\Gruppe 6}
\title{Hausaufgaben zum 26. Januar}
\maketitle

\setcounter{section}{3}
\section{} % 13.4
    \subsection{}
    Die Prozessgraphen für \(t_6\) und \(t_7\) befinden sich auf \fref{fig:t6-graph} bzw. \fref{fig:t7-graph}.

    Es existiert dabei folgende Bisimulationsrelation: \(\mathbb{B} = \{(c, \partial_H(c)), (b \cdot c, \partial_H(b \cdot c)), (b \cdot c, \partial_H((b + b) \cdot c)), ((a + b) \leftmerge (b \cdot c), \partial_H((a \leftmerge (b + b) + (d \parallel e) \cdot b) \cdot c))\}\)
    \begin{figure}
        \begin{tikzpicture}[node distance=1cm]
            \node (t6-start) {\((a + b) \leftmerge (b \cdot c)\)};
            \node (bc) [below=of t6-start] {\(b \cdot c\)};
            \node (c) [below=of bc] {\(c\)};
            \node (finish) [below=of c] {\(\surd\)};

            \path[->] (t6-start) edge[bend right] node[left] {\(a\)} (bc)
                (t6-start) edge[bend left] node[right] {\(b\)} (bc)
                (bc) edge node[right] {\(b\)} (c)
                (c) edge node[right] {\(c\)} (finish);
        \end{tikzpicture}
        \caption{Prozessgraph von \(t_6\)}
        \label{fig:t6-graph}
    \end{figure}

    \begin{figure}
        \begin{tikzpicture}[node distance=1cm]
            \node (start) {\(\partial_H((a \leftmerge (b + b) + (d \parallel e) \cdot b) \cdot c)\)};
            \node (a-left) [below left=of start] {\(\partial_H((b + b) \cdot c)\)};
            \node (de-right) [below right=of start] {\(\partial_H(b \cdot c)\)};
            \node (c) [below=3 of start] {\(\partial_H(c)\)};
            \node (finish) [below=of c] {\(\surd\)};

            \path[->] (start) edge node[above left] {\(a\)} (a-left)
                (start) edge node[above right] {\(f\)} (de-right)
                (a-left) edge[bend right] node[below left] {\(b\)} (c)
                (a-left) edge[bend left] node[above right] {\(b\)} (c)
                (de-right) edge node[above left] {\(b\)} (c)
                (c) edge node[right] {\(c\)} (finish);
        \end{tikzpicture}
        \caption{Prozessgraph von \(t_7\)}
        \label{fig:t7-graph}
    \end{figure}

    \subsection{}
    Nachweis des ersten Übergangs:
    \begin{alignat*}{2}
        &\; a \overset{a}{\rightarrow} \surd \\
        T^{\surd}_{+R} &\; a + b \overset{a}{\rightarrow} \surd \\
        T^{\surd}_{\leftmerge} &\; (a + b) \leftmerge b \cdot c \overset{a}{\rightarrow} b \cdot c
    \end{alignat*}

    Nachweis des zweiten Übergangs:
    \begin{alignat*}{2}
        T_{\parallel \gamma}^{\surd \surd} &&\; d \parallel e \overset{f}{\rightarrow} \surd \\
        T^{\surd}_{.} &&\; (d \parallel e) \cdot b \overset{f}{\rightarrow} b \\
        T_{+L} &&\; a \leftmerge (b + b) + (d \parallel e) \cdot b \overset{f}{\rightarrow} b \\
        T_{.} &&\; (a \leftmerge (b + b) + (d \parallel e) \cdot b) \cdot c \overset{f}{\rightarrow} b \cdot c \\
        T_{\partial} &&\; \partial_H((a \leftmerge (b + b) + (d \parallel e) \cdot b) \cdot c) \overset{f}{\rightarrow} \partial_H(b \cdot c)
    \end{alignat*}

    \subsection{}
    Die folgende Umformung wurde so weit es möglich war gezeigt.
    \begin{alignat*}{2}
        && (a + b) \leftmerge (b \cdot c) \\
        &\overset{LM2}{=}& (a + b) \cdot (b \cdot c) \\
        &\overset{A5}{=}& ((a + b) \cdot b) \cdot c \\
        &\overset{A4}{=}& (a \cdot b + b \cdot b) \cdot c \\
        &\overset{LM2}{=}& (a \leftmerge b + b \cdot b) \cdot c \\
        &\overset{A3}{=}& (a \leftmerge (b + b) + (b \cdot b + b \cdot b)) \cdot c \\
        &\overset{LM2}{=}& (a \leftmerge (b + b) + (b \leftmerge b + b \leftmerge b)) \cdot c
    \end{alignat*}

\setcounter{section}{5}
\section{} % 13.6
    \subsection{}
    Umformen von \(X\):
    \begin{alignat*}{2}
        X &=& (a + b) \cdot Y + c \cdot X \\
        X &=& a \cdot Y + b \cdot Y + c \cdot X
    \end{alignat*}

    Umformen von \(Y\):
    \begin{alignat*}{2}
        Y &=& X \cdot d + e \\
        Y &=& (a \cdot Y + b \cdot Y + c \cdot X) \cdot d + e
    \end{alignat*}
    \(Y\) lässt sich nicht in die notwendige Form überführen. Daher ist \(E\) keine geschützte rekursive Spezifikation.

    \subsection{}
    \begin{tikzpicture}[node distance=1cm]
        \node (start) {\(\langle X|E \rangle\)};
        \node (y) [right=of start] {\(\langle Y|E \rangle\)};
        \node (finish) [below=of y] {\(\surd\)};

        \path[->] (start) edge[bend left] node[above] {\(a\)} (y)
            (start) edge[bend right] node[below] {\(b\)} (y)
            (start) edge[loop left] node[left] {\(c\)} (start)
            (y) edge node[right] {\(e\)} (finish)
            (y) edge[loop above] node[above] {\(a\)} (y)
            (y) edge[loop right] node[right] {\(b\)} (y)
            (y) edge[bend left=90] node[below] {\(c\)} (start);
    \end{tikzpicture}

    \subsection{}
    Ableiten des Übergangs:
    \begin{alignat*}{2}
        &\; c \overset{c}{\rightarrow} \surd \\
        T^{\surd}_{.} &\; c \cdot \langle X|E \rangle \cdot d \overset{c}{\rightarrow} \langle X|E \rangle \cdot d \\
        T_{X} &\; \langle X|E \rangle \cdot d \overset{c}{\rightarrow} \langle X|E \rangle \cdot d \\
        T_{Y} &\; \langle Y|E \rangle \overset{c}{\rightarrow} \langle X|E \rangle \cdot d
    \end{alignat*}
\end{document}