1 files changed, 39 insertions, 0 deletions

diff --git a/ws2015/eip/blaetter/03/H3-1.md b/ws2015/eip/blaetter/03/H3-1.md
new file mode 100644
index 0000000..bb3d2ca
--- /dev/null
+++ b/ws2015/eip/blaetter/03/H3-1.md
@@ -0,0 +1,39 @@
+---
+header-includes:
+        - \usepackage{bussproofs}
+        - \renewcommand{\implies}{\rightarrow}
+        - \EnableBpAbbreviations
+---
+# Hoare-Tripel II
+
+d)
+
+\begin{prooftree}
+\AXC{$\forall \phi \ldotp \phi \implies \phi$}
+\UIC{$(0 < n + 1 \land n < m) \implies (0 < n + 1 \land n < m)$}
+\RightLabel{Umformung}
+\UIC{$(0 < n + 1 \land n < m) \implies (0 < n + 1 \land n \leq m - 1)$}
+\RightLabel{Umformung}
+\UIC{$(0 < n + 1 \land n < m) \implies (0 < n + 1 \land n + 1 \leq m)$}
+\RightLabel{Zuweisung}
+\UIC{$ \{ 0 < n + 1 \land n < m \} $ \texttt{n = n + 1} $ \{ 0 < n \land n \leq m \} $}
+\end{prooftree}
+
+e) Nimm als Gegenbeispiel:
+
+~~~
+a = -1
+b = 0
+~~~
+
+f) Seit $\phi$ die Nachfolgerfunktion auf $\mathbb{N}$.
+
+\begin{prooftree}
+\AXC{$\forall n \in \mathbb{N} \ldotp \phi(n) > n$}
+\UIC{$1 > 0$}
+\UIC{$((x + 1) + y > x + y)$}
+\UIC{$(z = x + y) \implies ((x + 1) + y > z)$}
+\UIC{$ \{ z = x + y \} $ \texttt{ x = x + 1} $ \{ x + y > z \} $}
+\UIC{$ \{ z = x + y \land z \equiv 0 \mod 2 \} $ \texttt{x = x + 1} $ \{ x + y > z \} $ \quad $ \{ z = x + y \land z \equiv 1 \mod 2 \} $ \texttt{x = x + 1} $ \{ x + y > z \} $}
+\UIC{$ \{ z = x + y \} $ \texttt{if (z \% 2 == 0) x = x + 1; else y = y + 1;} $ \{ x + y > z \} $}
+\end{prooftree}