---
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}