diff --git a/Cheatsheet.tex b/Cheatsheet.tex
index 9d668393d46fa99b06343d65ff63e07a79a9f54a..b9ebf86b82af41f09500e07105941199c1cf157f 100644
--- a/Cheatsheet.tex
+++ b/Cheatsheet.tex
@@ -31,6 +31,11 @@
%\end{abstract}
\pagenumbering{gobble}
+\section*{Lambda-Kalkül}
+\textbf{$\alpha$-Äquivalenz}: Umbenennung von Variablen, z.B. $\lambda x.x \rightarrow_\alpha \lambda y.y$ (wenn $y\notin FV(t)$) \\
+\textbf{$\beta$-Reduktion}: Argument anwenden, z.B. $(\lambda xy.yx)~a \rightarrow_\beta \lambda y.ya$\\
+\textbf{$\delta$-Reduktion}: Ausdruck durch Definition ersetzen, z.B. $true \rightarrow_\delta \lambda xy.x$\\
+\textbf{$\mu$-Reduktion}: Streichen von ungenutzten Argumenten, z.B. $\lambda x.yx \rightarrow_\mu y$
\section*{Konfluenz und Terminierung}
\textbf{SN + WCR $\Rightarrow$ CR}
@@ -43,11 +48,31 @@
Linke Seiten der einen Regel als Teilterme einer anderen (nicht notwendigerweise verschiedenen) Regel.
Variablen durch ganze Terme zu ersetzen ist trivial und kann ignoriert werden.
-\section*{Lambda-Kalkül}
-\textbf{$\alpha$-Äquivalenz}: Umbenennung von Variablen, z.B. $\lambda x.x \rightarrow_\alpha \lambda y.y$ (wenn $y\notin FV(t)$) \\
-\textbf{$\beta$-Reduktion}: Argument anwenden, z.B. $(\lambda xy.yx)~a \rightarrow_\beta \lambda y.ya$\\
-\textbf{$\delta$-Reduktion}: Ausdruck durch Definition ersetzen, z.B. $true \rightarrow_\delta \lambda xy.x$\\
-\textbf{$\mu$-Reduktion}: Streichen von ungenutzten Argumenten, z.B. $\lambda x.yx \rightarrow_\mu y$
+\section*{Strukturelle Induktion und Folds}
+Am Beispiel von Listen:
+\subsection*{Induktions-Anfang}
+Eine Variable (Typ: Liste) auf $Nil$ setzen, damit Gleichheit von linker und rechter Seite zeigen.
+\subsection*{Induktions-Voraussetzung}
+Variable aus IA auf $Cons~x~xs$ setzen, Gleichung mit Substitution explizit angeben.
+\subsection*{Induktions-Schritt}
+Gleichheit von linker und rechter Seite zeigen, dabei IV nutzen.
+
+Wenn linke und rechte Seite nicht durch einfache Umformungsregeln gleichzusetzen sind: Lemma einführen und beweisen (andere Variable als in IV verwenden).
+
+\section*{Korekursion und Koinduktion}
+Definition von korekursiven Funktionen mittels mit Kodaten als \textit{Ausgabe}. Am Beispiel von $map$:
+\begin{align*}
+hd(map~f~s)&=f(hd~s)\\
+tl(map~f~s)) &= (map~f)(tl~s)
+\end{align*}
+Bei der Koinduktion ist zu beweisen, dass eine \textit{Bisimulation} $R$ existiert:
+\begin{align*}
+hd~s~&=hd~t\\
+(tl~s)~&R~(tl~t)
+\end{align*}
+für alle $(s,t)\in R$.
+
+% TODO \section*{System F}
\section*{Auswertungsstrategien}
\textbf{Normal} (auch: leftmost-outermost) $\rightarrow_n$:
@@ -70,8 +95,90 @@ Variablen durch ganze Terme zu ersetzen ist trivial und kann ignoriert werden.
&A \times B\text{: Paare aus Elementen } &\{0,1\}\times \{0,1\} &= \{0,1\}\\
&A + B\text{: disjunkte Vereinigung } &\{0,1\} + \{0,1\} &= \{0,0,1,1\}
\end{align*}
+\pagebreak
+\section*{Minimierung von DFA}
+\begin{enumerate}
+ \item vom Startzustand aus unerreichbare Knoten streichen
+ \item bei allen Paare, die aus Endzustand und Nicht-Endzustand bestehen, \textbf{0} eintragen
+ \item für jedes Paar einen Übergang mit jeder Eingabe durchführen; wenn beim Ergebnis-Paar ein Wert $i$ steht, beim aktuellen $i+1$ eintragen
+ \item Punkt 3 so lange wiederholen, bis sich nichts mehr ändert
+ \item Paare, bei denen kein Wert steht, zusammenfassen
+\end{enumerate}
+
+\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm,
+semithick]
+\node[initial,state] (a) {$a$};
+\node[state] (e) [above of=a] {$e$};
+\node[state] (h) [right of=e] {$h$};
+\node[state,accepting] (c) [right of=h] {$c$};
+\node[state] (g) [right of=a] {$g$};
+\node[state] (f) [right of=g] {$f$};
+\node[state] (d) [below of=g] {$d$};
+\node[state] (b) [above of=h] {$b$};
+
+\path (a) edge [bend left] node {0} (e)
+edge [bend right] node {1} (h)
+(b) edge node {0,1} (c)
+(c) edge node {0,1} (h)
+(d) edge node {0} (f)
+edge node {1} (a)
+(e) edge node {0} (b)
+edge [bend left] node {1} (a)
+(f) edge node {0,1} (c)
+(g) edge node {0} (f)
+edge node {1} (a)
+(h) edge node {0} (g)
+edge node {1} (e);
+\end{tikzpicture}
+
+\begin{tikzpicture}
+\matrix(M)[matrix of math nodes,row sep=-\pgflinewidth,column sep=-\pgflinewidth,
+nodes={draw,minimum width=2em,minimum height=2em,font=\strut}]
+{
+ 3 & 1 & 0 & \times & 2 & 1 & 2\\
+ 2 & 1 & 0 & \times & & 1 \\
+ 1 & & 0 & \times & 1 \\
+ 2 & 1 & 0 & \times \\
+ \times & \times & \times \\
+ 0 & 0 \\
+ 1 \\
+};
+\foreach[count=\j] \i in {h,...,b}\node[left=0pt of M-\j-1]{\i};
+\foreach[count=\j] \i in {a,...,g}\node[above=0pt of M-1-\j]{$\i$};
+\draw[line width=.5mm] (M-1-4.north) -- (M-4-4.south);
+\draw[line width=.5mm] (M-5-1.west) -- (M-5-3.east);
+\end{tikzpicture}
+\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm,
+semithick]
+\node[initial,state] (a) {$a$};
+\node[state] (e) [above of=a] {$e,g$};
+\node[state] (h) [right of=e] {$h$};
+\node[state,accepting] (c) [right of=h] {$c$};
+\node[state] (b) [above of=h] {$b,f$};
+
+\path (a) edge [bend left] node {0} (e)
+edge [bend right] node {1} (h)
+(b) edge node {0,1} (c)
+(c) edge node {0,1} (h)
+(e) edge node {0} (b)
+edge [bend left] node {1} (a)
+(h) edge node {0,1} (e);
+\end{tikzpicture}
\pagebreak
+\section*{Typisierungsregeln}
+\begin{align*}
+(\text{axiom})&\frac{}{\Gamma,x:\alpha\vdash x:\alpha}\\&\\
+(\rightarrow_i)&\frac{\Gamma,x:\alpha\vdash t:\beta}{\Gamma\vdash\lambda x.t:\alpha\rightarrow\beta}\\&\\
+(\rightarrow_e)&\frac{\Gamma\vdash t:\alpha\rightarrow\beta \qquad\Gamma\vdash t:\alpha}{\Gamma\vdash ts : \beta}\\&\\
+(\forall_i)&\frac{\Gamma\vdash t:\alpha\qquad\text{a} \notin \text{FV}(\Gamma)}{\Gamma\vdash t : \forall \text{a}.\alpha}\\&\\
+(\forall_e)&\frac{\Gamma\vdash t :\forall \text{a}.\alpha}{\Gamma\vdash t:(\alpha[\text{a}:=\beta])}\qquad\text{bzw.}\\&\\
+(\forall_e)&\frac{}{\Gamma\vdash x:\alpha \left[a_1 \mapsto\beta_1,\ldots,a_k\mapsto\beta_k\right]}(x:\forall a_1 \ldots\forall a_k . \alpha)\in \Gamma\\&\\
+(\text{let})&\frac{\Gamma\vdash t:\alpha\qquad\Gamma,x:Cl(\Gamma, \alpha)\vdash s:\beta}{\Gamma\vdash\text{let }x=t\text{ in }s:\beta}
+\end{align*}
+
+%\pagebreak
+
\section*{Listen}
\begin{align*}
Nil&:List~a\\
@@ -96,18 +203,6 @@ maximum~Nil &= 0 \\
maximum~(Cons~x~xs) &= max~x~(maximum~xs)
\end{align*}
-\pagebreak
-\section*{Typisierungsregeln}
-\begin{align*}
-(\text{axiom})&\frac{}{\Gamma,x:\alpha\vdash x:\alpha}\\&\\
-(\rightarrow_i)&\frac{\Gamma,x:\alpha\vdash t:\beta}{\Gamma\vdash\lambda x.t:\alpha\rightarrow\beta}\\&\\
-(\rightarrow_e)&\frac{\Gamma\vdash t:\alpha\rightarrow\beta \qquad\Gamma\vdash t:\alpha}{\Gamma\vdash ts : \beta}\\&\\
-(\forall_i)&\frac{\Gamma\vdash t:\alpha\qquad\text{a} \notin \text{FV}(\Gamma)}{\Gamma\vdash t : \forall \text{a}.\alpha}\\&\\
-(\forall_e)&\frac{\Gamma\vdash t :\forall \text{a}.\alpha}{\Gamma\vdash t:(\alpha[\text{a}:=\beta])}\qquad\text{bzw.}\\&\\
-(\forall_e)&\frac{}{\Gamma\vdash x:\alpha \left[a_1 \mapsto\beta_1,\ldots,a_k\mapsto\beta_k\right]}(x:\forall a_1 \ldots\forall a_k . \alpha)\in \Gamma\\&\\
-(\text{let})&\frac{\Gamma\vdash t:\alpha\qquad\Gamma,x:Cl(\Gamma, \alpha)\vdash s:\beta}{\Gamma\vdash\text{let }x=t\text{ in }s:\beta}
-\end{align*}
-
\newpage
\section*{Funktionen}
\begin{align*}
@@ -153,74 +248,4 @@ lt~~n~m &= iszero~(sub~m~(succ~n))
\lceil n\rceil &= \lambda fa.\underbrace{f(f(f(\ldots f}_{n} a)))
\end{align*}
-\pagebreak
-\section*{Minimierung von DFA}
-\begin{enumerate}
- \item vom Startzustand aus unerreichbare Knoten streichen
- \item bei allen Paare, die aus Endzustand und Nicht-Endzustand bestehen, \textbf{0} eintragen
- \item für jedes Paar einen Übergang mit jeder Eingabe durchführen; wenn beim Ergebnis-Paar ein Wert $i$ steht, beim aktuellen $i+1$ eintragen
- \item Punkt 3 so lange wiederholen, bis sich nichts mehr ändert
- \item Paare, bei denen kein Wert steht, zusammenfassen
-\end{enumerate}
-
-\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm,
-semithick]
-\node[initial,state] (a) {$a$};
-\node[state] (e) [above of=a] {$e$};
-\node[state] (h) [right of=e] {$h$};
-\node[state,accepting] (c) [right of=h] {$c$};
-\node[state] (g) [right of=a] {$g$};
-\node[state] (f) [right of=g] {$f$};
-\node[state] (d) [below of=g] {$d$};
-\node[state] (b) [above of=h] {$b$};
-
-\path (a) edge [bend left] node {0} (e)
- edge [bend right] node {1} (h)
- (b) edge node {0,1} (c)
- (c) edge node {0,1} (h)
- (d) edge node {0} (f)
- edge node {1} (a)
- (e) edge node {0} (b)
- edge [bend left] node {1} (a)
- (f) edge node {0,1} (c)
- (g) edge node {0} (f)
- edge node {1} (a)
- (h) edge node {0} (g)
- edge node {1} (e);
-\end{tikzpicture}
-
-\begin{tikzpicture}
-\matrix(M)[matrix of math nodes,row sep=-\pgflinewidth,column sep=-\pgflinewidth,
-nodes={draw,minimum width=2em,minimum height=2em,font=\strut}]
-{
- 3 & 1 & 0 & \times & 2 & 1 & 2\\
- 2 & 1 & 0 & \times & & 1 \\
- 1 & & 0 & \times & 1 \\
- 2 & 1 & 0 & \times \\
- \times & \times & \times \\
- 0 & 0 \\
- 1 \\
-};
-\foreach[count=\j] \i in {h,...,b}\node[left=0pt of M-\j-1]{\i};
-\foreach[count=\j] \i in {a,...,g}\node[above=0pt of M-1-\j]{$\i$};
-\draw[line width=.5mm] (M-1-4.north) -- (M-4-4.south);
-\draw[line width=.5mm] (M-5-1.west) -- (M-5-3.east);
-\end{tikzpicture}
-\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm,
-semithick]
-\node[initial,state] (a) {$a$};
-\node[state] (e) [above of=a] {$e,g$};
-\node[state] (h) [right of=e] {$h$};
-\node[state,accepting] (c) [right of=h] {$c$};
-\node[state] (b) [above of=h] {$b,f$};
-
-\path (a) edge [bend left] node {0} (e)
- edge [bend right] node {1} (h)
- (b) edge node {0,1} (c)
- (c) edge node {0,1} (h)
- (e) edge node {0} (b)
- edge [bend left] node {1} (a)
- (h) edge node {0,1} (e);
-\end{tikzpicture}
-
\end{document}