\begin{center}
\begin{sideways}
\small\infertrue
$
%logical consequence
\La{{{
\CA F {\WHILE\ a \neq b \ \DO\ \ASS a{a+1}; \ASS b{b-1}\ \OD\ }{G}}}}
%LC-Unterm Strich
{F \Rightarrow {\INV\ }}
%LC-Übern Strich 1. Ausdruck
{\WHt{{
\CA\INV{\WHILE\ a \neq b \ \DO\ \ASS a{a+1}; \ASS b{b-1}\ \OD\ }
{\INV\land\lnot e}}}
%Wht-Unterm Strich
   {\SC
{\CA
{\INV\land a \neq b \land t = t_0}%CA - 1.
{\ASS a{a+1}; \ASS b{b-1}\ }%CA - 2.
{\INV\land 0 \leq t \leq t_0}}%CA - 3.
%Sequence-unterm Strich
{\La{\CA{\INV\land a \neq b \land t = t_0}{\ASS a{a+1};\ }{B}}{{\INV\land  a \neq b \land t = t_0} => C}{\CA{C}{\ASS a{a+1}}{B}}
}
%Sequence-überm Strich 1. Ausdruck
{\CA{B}{\ASS b{b-1}\ }{\INV\land 0 \leq t \leq t_0}}}
%Sequence-überm Strich 2. Ausdruck
%Wht-Übern Strich 1. Ausdruck
{}
%Wht-Übern Strich 2. Ausdruck  (Wird nciht gebraucht da wir wht''  verwenden)
}%LC-Übern Strich 2. Ausdruck
{\INV\land \neg e \Rightarrow G
}
%LC-Übern Strich 3. Ausdruck
$
\end{sideways}
\end{center}