\subsection{Faculteit}
Als we de analyse op een compleet programma toepassen komt er een \textit{Piet}
programma uit dat behoorlijk fors is maar netjes zijn werk doet. Dit programma
berekent de faculteit van $x$ en stopt dat uiteindelijk in $y$.
\begin{lstlisting}[title=Faculteit in \textit{While}]
x:=5;
y:=1;
while $\neg$(x=1)
do (
    y:=y*x;
    x:=x-1
)
\end{lstlisting}

In \textit{Piet} ziet dit er als volgt uit...
\begin{lstlisting}[title=Faculteit in \textit{Piet'}]
push 10     // x:=5
push 1      // y:=1

MARKERING A:
            // Un(2)
            // $\neg$(x=1) $\equiv$ \neg(x-1)>0)


            // x-1
            // Un(2)
push 2      //
push 1      //
roll        //
dup         //
push 3      //
push 1      //
roll        //
push 1      //
sub         //
not         // $\neg(x-1)$

push 1      // zet $0$ op de stack
push 1
sub

gre         // $\neg(x-1)>0$ oftewel x=1

pointer     // als x=0 dan draait de DP niet en gaat het programma naar pad B
            // als x$\neq$ dan draait de DP en gaat het programma naar pad A

PAD A:
skip        // een oneindig aantal witte blokken, y is nu x!
            // evt een outchar om $y$ naar standardout te printen

PAD B:
            // y:=y*x
            // Bin(1, 2)
dup         // Un(1)
push 3      // Un(2+1)
push 2      //
roll        //
dup         //
push 4      //
push 1      //
roll        //
mul         // x*y
push 2      // Ass(1)
push 1
roll
pop

            // x:=x-1
push 2      // Un(2)
push 1
roll
dup
push 3
push 1
roll


push 1      // 
sub         // x-1
push 3      // Ass(2)
push 2
roll 
pop
push 2
push 1
roll
            // nu gaat het programma weer via een wit pad naar markering A
\end{lstlisting}

Wat in piet er uit zit als in \ref{fig:img3}
\begin{figure}[H]
	\caption{Factulteit vanuit \textit{While} naar \textit{Piet}}
	\label{fig:img3}
	\centering
	\fbox{\includegraphics[natheight=320px, natwidth=256px, height=320px,
	width=256px]{img3.png}}
\end{figure}

\begin{landscape}
De afleidingsrij voor 1! ziet er als volgt uit:\\
$
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2;push \: 1;push \: 1, [\:], [\:], [\:]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2;push \: 1, [\:], [\:], [1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2, [\:], [\:], [1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1, [\:], [\:], [2,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll, [\:], [\:], [1,2,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup, [\:], [\:], [1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1, [\:], [\:], [3,1,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll, [\:], [\:], [1,3,1,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;, [\:], [\:], [1,1,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1;not, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1, [\:], [\:], [1,1,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract, [\:], [\:], [1,1,1,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater, [\:], [\:], [0,1,1,1]\rangle \Rightarrow\\
\langle pointer; not, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
\langle pointer [\:], [\:], [0,1,1]\rangle \Rightarrow\\
\langle [\:], [\:], [1,1]\rangle\\
\\
$
Eerst worden x en y op de stack gestopt zodat de stack [y,x] = [1,1]. 
Deze stack is gelijk aan de stack in de termineerende configuratie: 1 = 1! dus y = x!.
Als bewijs dat de wiskundige operaties op de stack goed zijn uitgevoerd staat in 
de appendix onder het kopje voorbeelden een stukje code.  In het programma 
eenfaculteit worden alle wiskundige operaties die bij de commando's horen 
achter elkaar uitgevoerd op de stack, waarbij het resultaat [1,1] is.\\
Bij de voorbeelden staan ook nog de programma's tweefaculteit en 
vijffaculteit die respectievelijk 2! en 5! uitrekenen.
\end{landscape}