Task 2

4 files changed, 554 insertions, 1 deletions

diff --git a/prooftree.sty b/prooftree.sty
new file mode 100644
index 0000000..b611d67
--- /dev/null
+++ b/prooftree.sty
@@ -0,0 +1,374 @@
+\message{<Paul Taylor's Proof Trees, 2 August 1996>}
+%% Build proof tree for Natural Deduction, Sequent Calculus, etc.
+%% WITH SHORTENING OF PROOF RULES!
+%% Paul Taylor, begun 10 Oct 1989
+%% *** THIS IS ONLY A PRELIMINARY VERSION AND THINGS MAY CHANGE! ***
+%%
+%% 2 Aug 1996: fixed \mscount and \proofdotnumber
+%%
+%%      \prooftree
+%%              hyp1            produces:
+%%              hyp2
+%%              hyp3            hyp1    hyp2    hyp3
+%%      \justifies              -------------------- rulename
+%%              concl                   concl
+%%      \thickness=0.08em
+%%      \shiftright 2em
+%%      \using
+%%              rulename
+%%      \endprooftree
+%%
+%% where the hypotheses may be similar structures or just formulae.
+%%
+%% To get a vertical string of dots instead of the proof rule, do
+%%
+%%      \prooftree                      which produces:
+%%              [hyp]
+%%      \using                                  [hyp]
+%%              name                              .
+%%      \proofdotseparation=1.2ex                 .name
+%%      \proofdotnumber=4                         .
+%%      \leadsto                                  .
+%%              concl                           concl
+%%      \endprooftree
+%%
+%% Within a prooftree, \[ and \] may be used instead of \prooftree and
+%% \endprooftree; this is not permitted at the outer level because it
+%% conflicts with LaTeX. Also,
+%%      \Justifies
+%% produces a double line. In LaTeX you can use \begin{prooftree} and
+%% \end{prootree} at the outer level (however this will not work for the inner
+%% levels, but in any case why would you want to be so verbose?).
+%%
+%% All of of the keywords except \prooftree and \endprooftree are optional
+%% and may appear in any order. They may also be combined in \newcommand's
+%% eg "\def\Cut{\using\sf cut\thickness.08em\justifies}" with the abbreviation
+%% "\prooftree hyp1 hyp2 \Cut \concl \endprooftree". This is recommended and
+%% some standard abbreviations will be found at the end of this file.
+%%
+%% \thickness specifies the breadth of the rule in any units, although
+%% font-relative units such as "ex" or "em" are preferable.
+%% It may optionally be followed by "=".
+%% \proofrulebreadth=.08em or \setlength\proofrulebreadth{.08em} may also be
+%% used either in place of \thickness or globally; the default is 0.04em.
+%% \proofdotseparation and \proofdotnumber control the size of the
+%% string of dots
+%%
+%% If proof trees and formulae are mixed, some explicit spacing is needed,
+%% but don't put anything to the left of the left-most (or the right of
+%% the right-most) hypothesis, or put it in braces, because this will cause
+%% the indentation to be lost.
+%%
+%% By default the conclusion is centered wrt the left-most and right-most
+%% immediate hypotheses (not their proofs); \shiftright or \shiftleft moves
+%% it relative to this position. (Not sure about this specification or how
+%% it should affect spreading of proof tree.)
+%
+% global assignments to dimensions seem to have the effect of stretching
+% diagrams horizontally.
+%
+%%==========================================================================
+
+\def\introrule{{\cal I}}\def\elimrule{{\cal E}}%%
+\def\andintro{\using{\land}\introrule\justifies}%%
+\def\impelim{\using{\Rightarrow}\elimrule\justifies}%%
+\def\allintro{\using{\forall}\introrule\justifies}%%
+\def\allelim{\using{\forall}\elimrule\justifies}%%
+\def\falseelim{\using{\bot}\elimrule\justifies}%%
+\def\existsintro{\using{\exists}\introrule\justifies}%%
+
+%% #1 is meant to be 1 or 2 for the first or second formula
+\def\andelim#1{\using{\land}#1\elimrule\justifies}%%
+\def\orintro#1{\using{\lor}#1\introrule\justifies}%%
+
+%% #1 is meant to be a label corresponding to the discharged hypothesis/es
+\def\impintro#1{\using{\Rightarrow}\introrule_{#1}\justifies}%%
+\def\orelim#1{\using{\lor}\elimrule_{#1}\justifies}%%
+\def\existselim#1{\using{\exists}\elimrule_{#1}\justifies}
+
+%%==========================================================================
+
+\newdimen\proofrulebreadth \proofrulebreadth=.05em
+\newdimen\proofdotseparation \proofdotseparation=1.25ex
+\newdimen\proofrulebaseline \proofrulebaseline=2ex
+\newcount\proofdotnumber \proofdotnumber=3
+\let\then\relax
+\def\hfi{\hskip0pt plus.0001fil}
+\mathchardef\squigto="3A3B
+%
+% flag where we are
+\newif\ifinsideprooftree\insideprooftreefalse
+\newif\ifonleftofproofrule\onleftofproofrulefalse
+\newif\ifproofdots\proofdotsfalse
+\newif\ifdoubleproof\doubleprooffalse
+\let\wereinproofbit\relax
+%
+% dimensions and boxes of bits
+\newdimen\shortenproofleft
+\newdimen\shortenproofright
+\newdimen\proofbelowshift
+\newbox\proofabove
+\newbox\proofbelow
+\newbox\proofrulename
+%
+% miscellaneous commands for setting values
+\def\shiftproofbelow{\let\next\relax\afterassignment\setshiftproofbelow\dimen0 }
+\def\shiftproofbelowneg{\def\next{\multiply\dimen0 by-1 }%
+\afterassignment\setshiftproofbelow\dimen0 }
+\def\setshiftproofbelow{\next\proofbelowshift=\dimen0 }
+\def\setproofrulebreadth{\proofrulebreadth}
+
+%=============================================================================
+\def\prooftree{% NESTED ZERO (\ifonleftofproofrule)
+%
+% first find out whether we're at the left-hand end of a proof rule
+\ifnum  \lastpenalty=1
+\then   \unpenalty
+\else   \onleftofproofrulefalse
+\fi
+%
+% some space on left (except if we're on left, and no infinity for outermost)
+\ifonleftofproofrule
+\else   \ifinsideprooftree
+        \then   \hskip.5em plus1fil
+        \fi
+\fi
+%
+% begin our proof tree environment
+\bgroup% NESTED ONE (\proofbelow, \proofrulename, \proofabove,
+%               \shortenproofleft, \shortenproofright, \proofrulebreadth)
+\setbox\proofbelow=\hbox{}\setbox\proofrulename=\hbox{}%
+\let\justifies\proofover\let\leadsto\proofoverdots\let\Justifies\proofoverdbl
+\let\using\proofusing\let\[\prooftree
+\ifinsideprooftree\let\]\endprooftree\fi
+\proofdotsfalse\doubleprooffalse
+\let\thickness\setproofrulebreadth
+\let\shiftright\shiftproofbelow \let\shift\shiftproofbelow
+\let\shiftleft\shiftproofbelowneg
+\let\ifwasinsideprooftree\ifinsideprooftree
+\insideprooftreetrue
+%
+% now begin to set the top of the rule (definitions local to it)
+\setbox\proofabove=\hbox\bgroup$\displaystyle % NESTED TWO
+\let\wereinproofbit\prooftree
+%
+% these local variables will be copied out:
+\shortenproofleft=0pt \shortenproofright=0pt \proofbelowshift=0pt
+%
+% flags to enable inner proof tree to detect if on left:
+\onleftofproofruletrue\penalty1
+}
+
+%=============================================================================
+% end whatever box and copy crucial values out of it
+\def\eproofbit{% NESTED TWO
+%
+% various hacks applicable to hypothesis list 
+\ifx    \wereinproofbit\prooftree
+\then   \ifcase \lastpenalty
+        \then   \shortenproofright=0pt  % 0: some other object, no indentation
+        \or     \unpenalty\hfil         % 1: empty hypotheses, just glue
+        \or     \unpenalty\unskip       % 2: just had a tree, remove glue
+        \else   \shortenproofright=0pt  % eh?
+        \fi
+\fi
+%
+% pass out crucial values from scope
+\global\dimen0=\shortenproofleft
+\global\dimen1=\shortenproofright
+\global\dimen2=\proofrulebreadth
+\global\dimen3=\proofbelowshift
+\global\dimen4=\proofdotseparation
+\global\count255=\proofdotnumber
+%
+% end the box
+$\egroup  % NESTED ONE
+%
+% restore the values
+\shortenproofleft=\dimen0
+\shortenproofright=\dimen1
+\proofrulebreadth=\dimen2
+\proofbelowshift=\dimen3
+\proofdotseparation=\dimen4
+\proofdotnumber=\count255
+}
+
+%=============================================================================
+\def\proofover{% NESTED TWO
+\eproofbit % NESTED ONE
+\setbox\proofbelow=\hbox\bgroup % NESTED TWO
+\let\wereinproofbit\proofover
+$\displaystyle
+}%
+%
+%=============================================================================
+\def\proofoverdbl{% NESTED TWO
+\eproofbit % NESTED ONE
+\doubleprooftrue
+\setbox\proofbelow=\hbox\bgroup % NESTED TWO
+\let\wereinproofbit\proofoverdbl
+$\displaystyle
+}%
+%
+%=============================================================================
+\def\proofoverdots{% NESTED TWO
+\eproofbit % NESTED ONE
+\proofdotstrue
+\setbox\proofbelow=\hbox\bgroup % NESTED TWO
+\let\wereinproofbit\proofoverdots
+$\displaystyle
+}%
+%
+%=============================================================================
+\def\proofusing{% NESTED TWO
+\eproofbit % NESTED ONE
+\setbox\proofrulename=\hbox\bgroup % NESTED TWO
+\let\wereinproofbit\proofusing
+\kern0.3em$
+}
+
+%=============================================================================
+\def\endprooftree{% NESTED TWO
+\eproofbit % NESTED ONE
+% \dimen0 =     length of proof rule
+% \dimen1 =     indentation of conclusion wrt rule
+% \dimen2 =     new \shortenproofleft, ie indentation of conclusion
+% \dimen3 =     new \shortenproofright, ie
+%                space on right of conclusion to end of tree
+% \dimen4 =     space on right of conclusion below rule
+  \dimen5 =0pt% spread of hypotheses
+% \dimen6, \dimen7 = height & depth of rule
+%
+% length of rule needed by proof above
+\dimen0=\wd\proofabove \advance\dimen0-\shortenproofleft
+\advance\dimen0-\shortenproofright
+%
+% amount of spare space below
+\dimen1=.5\dimen0 \advance\dimen1-.5\wd\proofbelow
+\dimen4=\dimen1
+\advance\dimen1\proofbelowshift \advance\dimen4-\proofbelowshift
+%
+% conclusion sticks out to left of immediate hypotheses
+\ifdim  \dimen1<0pt
+\then   \advance\shortenproofleft\dimen1
+        \advance\dimen0-\dimen1
+        \dimen1=0pt
+%       now it sticks out to left of tree!
+        \ifdim  \shortenproofleft<0pt
+        \then   \setbox\proofabove=\hbox{%
+                        \kern-\shortenproofleft\unhbox\proofabove}%
+                \shortenproofleft=0pt
+        \fi
+\fi
+%
+% and to the right
+\ifdim  \dimen4<0pt
+\then   \advance\shortenproofright\dimen4
+        \advance\dimen0-\dimen4
+        \dimen4=0pt
+\fi
+%
+% make sure enough space for label
+\ifdim  \shortenproofright<\wd\proofrulename
+\then   \shortenproofright=\wd\proofrulename
+\fi
+%
+% calculate new indentations
+\dimen2=\shortenproofleft \advance\dimen2 by\dimen1
+\dimen3=\shortenproofright\advance\dimen3 by\dimen4
+%
+% make the rule or dots, with name attached
+\ifproofdots
+\then
+        \dimen6=\shortenproofleft \advance\dimen6 .5\dimen0
+        \setbox1=\vbox to\proofdotseparation{\vss\hbox{$\cdot$}\vss}%
+        \setbox0=\hbox{%
+                \advance\dimen6-.5\wd1
+                \kern\dimen6
+                $\vcenter to\proofdotnumber\proofdotseparation
+                        {\leaders\box1\vfill}$%
+                \unhbox\proofrulename}%
+\else   \dimen6=\fontdimen22\the\textfont2 % height of maths axis
+        \dimen7=\dimen6
+        \advance\dimen6by.5\proofrulebreadth
+        \advance\dimen7by-.5\proofrulebreadth
+        \setbox0=\hbox{%
+                \kern\shortenproofleft
+                \ifdoubleproof
+                \then   \hbox to\dimen0{%
+                        $\mathsurround0pt\mathord=\mkern-6mu%
+                        \cleaders\hbox{$\mkern-2mu=\mkern-2mu$}\hfill
+                        \mkern-6mu\mathord=$}%
+                \else   \vrule height\dimen6 depth-\dimen7 width\dimen0
+                \fi
+                \unhbox\proofrulename}%
+        \ht0=\dimen6 \dp0=-\dimen7
+\fi
+%
+% set up to centre outermost tree only
+\let\doll\relax
+\ifwasinsideprooftree
+\then   \let\VBOX\vbox
+\else   \ifmmode\else$\let\doll=$\fi
+        \let\VBOX\vcenter
+\fi
+% this \vbox or \vcenter is the actual output:
+\VBOX   {\baselineskip\proofrulebaseline \lineskip.2ex
+        \expandafter\lineskiplimit\ifproofdots0ex\else-0.6ex\fi
+        \hbox   spread\dimen5   {\hfi\unhbox\proofabove\hfi}%
+        \hbox{\box0}%
+        \hbox   {\kern\dimen2 \box\proofbelow}}\doll%
+%
+% pass new indentations out of scope
+\global\dimen2=\dimen2
+\global\dimen3=\dimen3
+\egroup % NESTED ZERO
+\ifonleftofproofrule
+\then   \shortenproofleft=\dimen2
+\fi
+\shortenproofright=\dimen3
+%
+% some space on right and flag we've just made a tree
+\onleftofproofrulefalse
+\ifinsideprooftree
+\then   \hskip.5em plus 1fil \penalty2
+\fi
+}
+
+\endinput
+
+%==========================================================================
+% IDEAS
+% 1.    Specification of \shiftright and how to spread trees.
+% 2.    Spacing command \m which causes 1em+1fil spacing, over-riding
+%       exisiting space on sides of trees and not affecting the
+%       detection of being on the left or right.
+% 3.    Hack using \@currenvir to detect LaTeX environment; have to
+%       use \aftergroup to pass \shortenproofleft/right out.
+% 4.    (Pie in the sky) detect how much trees can be "tucked in"
+% 5.    Discharged hypotheses (diagonal lines).
+
+Date: Tue, 19 May 1998 16:45:32 +0100
+From: Simon Gay <simon@dcs.rhbnc.ac.uk>
+
+I've got another problem when combining
+your packages with elsart.cls. The code
+
+\documentclass{elsart}
+\input{prooftree}
+\input{diagrams}
+\begin{document}
+
+\[
+\begin{prooftree}
+A \rTo^{f} B
+\justifies
+p \rTo^{(a,c)} q
+\end{prooftree}
+\]
+
+\end{document}
+
+doesn't leave enough space below the line in the proof tree, so that
+the (a,c) label on the lower arrow runs into the line. It's fine with
+article.cls. 
diff --git a/senc.sty b/senc.sty
index f08edb0..9a6af38 100644
--- a/senc.sty
+++ b/senc.sty
@@ -1,4 +1,4 @@
-\RequirePackage{amssymb,amsmath,stmaryrd}
+\RequirePackage{amssymb,amsmath,stmaryrd,alltt,color}
 
 \def\A#1{\mathcal{A}\left\llbracket#1\right\rrbracket}
 \def\B#1{\mathcal{B}\left\llbracket#1\right\rrbracket}
@@ -13,3 +13,15 @@
 \def\AND{\mathtt{\;\&\&\;}}
 \def\OR{\mathtt{\;||\;}}
 
+\newcommand{\sdowhile}[2]{\mbox{\texttt{do~}}#1\mbox{\texttt{~while~}}#2}
+\def\ruleif#1{\using{\enspace\text{if }#1}}
+\def\axif#1{\enspace\text{if }#1}
+
+% Engelbert Hubbers, Annotated Programs
+\input{sl1defs}
+\newcommand{\pass}[2]{\left[#1\mapsto\calA{#2}\right]}
+\newcommand{\smaller}[1]{{\small\textcolor{red}{#1}}}
+\renewcommand{\allttsup}[1]{\begin{math}^{\textcolor{red}{#1}}\end{math}}
+%\renewcommand{\allttsub}[1]{\begin{math}_{\textcolor{red}{#1}}\end{math}}
+\renewcommand{\psqan}[5]{\{#1\}^{\textcolor{red}{#4}}\espace #2 \espace \{#3\}^{\textcolor{red}{#5}}}
+
diff --git a/sl1defs.tex b/sl1defs.tex
new file mode 100644
index 0000000..36355d2
--- /dev/null
+++ b/sl1defs.tex
@@ -0,0 +1,79 @@
+\newcommand{\calA}[1]{{\cal A}\llbracket #1 \rrbracket}
+\newcommand{\calB}[1]{{\cal B}\llbracket #1 \rrbracket}
+\newcommand{\CC}{{\mathbb C}}
+\newcommand{\desda}{\leftrightarrow}
+\newcommand{\Desda}{\Leftrightarrow}
+\newcommand{\dimpl}{\Rightarrow}
+\newcommand{\espace}{\hspace*{0.2cm}}
+\newcommand{\impl}{\rightarrow}
+\newcommand{\mgeq}{\begin{math}\geq\end{math}}
+\newcommand{\mggd}{\mbox{ggd}}
+\newcommand{\mgcd}{\mbox{gcd}}
+\newcommand{\minv}{\mbox{INV}}
+\newcommand{\mneg}{\begin{math}\neg\end{math}}
+\newcommand{\mneq}{\begin{math}\neq\end{math}}
+\newcommand{\mwedge}{\begin{math}\wedge\end{math}}
+\newcommand{\NN}{{\mathbb N}}
+\newcommand{\postboven}{}
+\newcommand{\postonder}{}
+\newcommand{\preboven}{}
+\newcommand{\preonder}{}
+\newcommand{\punten}[1]{\marginpar{\fbox{#1}}}
+\newcommand{\QQ}{{\mathbb Q}}
+\newcommand{\RR}{{\mathbb R}}
+\newcommand{\psq}[3]{\{#1\}\espace #2 \espace \{#3\}}
+\newcommand{\psqsr}[5]{\{#1\}\espace #2 \espace \{#3\} \espace #4 \espace \{#5\}}
+\newcommand{\psqsrst}[7]{\{#1\}\espace #2 \espace \{#3\} \espace #4 \espace \{#5\} \espace #6 \espace \{#7\}}
+\newcommand{\psqan}[5]{\{#1\}^{#4}\espace #2 \espace \{#3\}^{#5}}
+\newcommand{\allttmath}[1]{\begin{math}#1\end{math}}
+\newcommand{\allttsup}[1]{\begin{math}^{#1}\end{math}}
+\newcommand{\allttsub}[1]{\begin{math}_{#1}\end{math}}
+
+\newcommand{\sblock}[2]{\mbox{\texttt{begin~}}#1\espace#2\mbox{\texttt{~end}}}
+\newcommand{\svar}[2]{\mbox{\texttt{var~}}#1:=#2;}
+\newcommand{\sass}[2]{#1:=#2}
+\newcommand{\scomp}[2]{#1;#2}
+\newcommand{\sifthenelse}[3]{\mbox{\texttt{if~}}#1\mbox{\texttt{~then~}}#2\mbox{\texttt{~else~}}#3}
+\newcommand{\sor}[2]{#1\mbox{\texttt{~or~}}#2}
+\newcommand{\srepeatuntil}[2]{\mbox{\texttt{repeat~}}#1\mbox{\texttt{~until~}}#2}
+\newcommand{\sskip}{\mbox{\texttt{skip}}}
+\newcommand{\swhile}[2]{\mbox{\texttt{while~}}#1\mbox{\texttt{~do~}}#2}
+\newcommand{\swhileuntil}[3]{\mbox{\texttt{while~}}#1\mbox{\texttt{~do~}}#2\mbox{\texttt{~until~}}#3}
+\newcommand{\trans}[3]{\langle #1, #2\rangle \impl #3}
+\newcommand{\ZZ}{{\mathbb Z}}
+\newenvironment{sol}{\expandafter\ifsols\par{\bf{Oplossing:}\\}}{\par\expandafter\fi}
+\newcommand{\mtt}{\mbox{tt}}
+\newcommand{\mff}{\mbox{ff}}
+\newcommand{\mwhile}{\mbox{while}}
+\newcommand{\mif}{\mbox{if}}
+\newcommand{\mthen}{\mbox{then}}
+\newcommand{\melse}{\mbox{else}}
+\newcommand{\mdo}{\mbox{do}}
+\newcommand{\mmskip}{\mbox{skip}}
+\newcommand{\mtrue}{\mbox{true}}
+\newcommand{\mfalse}{\mbox{false}}
+\newcommand{\rskipp}{[\mbox{skip}_{\mbox{p}}]}
+\newcommand{\rassp}{[\mbox{ass}_{\mbox{p}}]}
+\newcommand{\rcompp}{[\mbox{comp}_{\mbox{p}}]}
+\newcommand{\rifp}{[\mbox{if}_{\mbox{p}}]}
+\newcommand{\rwhilep}{[\mbox{while}_{\mbox{p}}]}
+\newcommand{\rconsp}{[\mbox{cons}_{\mbox{p}}]}
+\newcommand{\rvar}{[\mbox{var}_{\mbox{ns}}]}
+\newcommand{\rnone}{[\mbox{none}_{\mbox{ns}}]}
+\newcommand{\rass}{[\mbox{ass}_{\mbox{ns}}]}
+\newcommand{\rskip}{[\mbox{skip}_{\mbox{ns}}]}
+\newcommand{\rcomp}{[\mbox{comp}_{\mbox{ns}}]}
+\newcommand{\riftt}{[\mbox{if}_{\mbox{ns}}^{\mbox{tt}}]}
+\newcommand{\rifff}{[\mbox{if}_{\mbox{ns}}^{\mbox{ff}}]}
+\newcommand{\rwhilett}{[\mbox{while}_{\mbox{ns}}^{\mbox{tt}}]}
+\newcommand{\rwhileff}{[\mbox{while}_{\mbox{ns}}^{\mbox{ff}}]}
+\newcommand{\rwhileuntilttff}{[\mbox{while-until}_{\mbox{ns}}^{\mbox{ttff}}]}
+\newcommand{\rwhileuntiltttt}{[\mbox{while-until}_{\mbox{ns}}^{\mbox{tttt}}]}
+\newcommand{\rwhileuntilff}{[\mbox{while-until}_{\mbox{ns}}^{\mbox{ff}}]}
+\newcommand{\rcall}{[\mbox{call}_{\mbox{ns}}]}
+\newcommand{\rcallrec}{[\mbox{call}_{\mbox{ns}}^{\mbox{rec}}]}
+\newcommand{\strans}[4]{{#1} \vdash \langle {#2}, {#3} \rangle \rightarrow {#4}}
+\newcommand{\dtrans}[3]{\langle {#1}, {#2} \rangle \rightarrow_{D} {#3}}
+
+\newcommand{\axjustifies}{\thickness0em\justifies}
+\endinput
diff --git a/task2.tex b/task2.tex
new file mode 100644
index 0000000..a85aa89
--- /dev/null
+++ b/task2.tex
@@ -0,0 +1,88 @@
+\documentclass[a4paper,9pt]{article}
+
+\usepackage[dutch]{babel}
+\usepackage{geometry}
+
+\author{Camil Staps}
+\title{Semantiek \& Correctheid\\\Large{Leertaak 2}}
+
+\usepackage{senc}
+\usepackage{prooftree} 
+\usepackage{alltt}
+\usepackage{stmaryrd}
+\usepackage[figuresleft]{rotating}
+\usepackage{mathdots}
+
+%\renewcommand{\trans}[3]{#1} 
+
+\begin{document}
+
+\maketitle
+
+\section*{Opdracht 2.3}
+Zie Figuur \ref{fig:boom}.
+Hier geldt:
+
+\begin{align*}
+    s_0 &= [x\mapsto17, y\mapsto5]\\ %todo
+    s_1 &= s_0[z\mapsto0]\\
+    s_2 &= s_1[z\mapsto1]\\
+    s_3 &= s_2[x\mapsto12]\\
+    s_{13} &= s_3[z\mapsto6,x\mapsto-13].
+\end{align*}
+
+\begin{sidewaysfigure}
+  \scriptsize
+  $$
+  \begin{prooftree}
+      \[
+        \axjustifies \trans{\sass{z}{0}}{s_0}{s_1} \using{\rassp}
+      \]\quad
+      \[
+        \[
+          \[\axjustifies \trans{\sass{z}{z+1}}{s_1}{s_2} \using{\rassp}\]\quad
+          \[\axjustifies \trans{\sass{x}{x-y}}{s_2}{s_3} \using{\rassp}\]
+          \justifies \trans{\scomp{\sass{z}{z+1}}{\sass{x}{x-y}}}{s_1}{s_3} \using{\rcomp}
+        \]\quad
+        \[\vdots\quad
+          \[
+            \[
+              \axjustifies \trans{\swhile{y\le x}{(\scomp{\sass{z}{z+1}}{\sass{x}{x-y}})}}{s_{13}}{s_{13}}%todo
+              \using{\rwhileff}
+            \]
+            \justifies \iddots \using{\rwhilett}
+          \]
+          \axjustifies
+          \trans{\swhile{y\le x}{(\scomp{\sass{z}{z+1}}{\sass{x}{x-y}})}}{s_3}{s_{13}}
+        \]
+        \justifies \trans{\swhile{y\le x}{(\scomp{\sass{z}{z+1}}{\sass{x}{x-y}})}}{s_1}{s_{13}}
+        \using{\rwhilett}
+      \]
+      \justifies \trans{\scomp{\sass{z}{0}}{\swhile{y\le x}{(\scomp{\sass{z}{z+1}}{\sass{x}{x-y}})}}}{s_0}{s_{13}}
+      \using{\rcomp}
+  \end{prooftree}
+  $$
+  \caption{Afleidingsboom voor opgave 2.3}
+  \label{fig:boom}
+\end{sidewaysfigure}
+
+\section*{Het \texttt{do} statement}
+\subsection*{Syntax}
+We voegen een regel $S ::= \sdowhile{S}{b}$ toe.
+
+\subsection*{Semantiek}
+$$\trans{\sdowhile{S}{b}}{s}{s} \axif{\B{b}s=\ff}$$
+$$\begin{prooftree}
+\trans{S}{s}{s'} \quad \trans{\sdowhile{S}{b}}{s'}{s''}
+\justifies \trans{\sdowhile{S}{b}}{s}{s''} \ruleif{\B{b}s=\tt}
+\end{prooftree}$$
+
+\section*{Opdracht 2.4}
+\begin{itemize}
+    \item Termineert als $x\ge1$, anders niet.
+    \item Idem.
+    \item Termineert niet. $\B{\mtrue}=\tt$, dus we gebruiken $\rwhilett$. Aangezien {\sskip} de toestand niet verandert kunnen we dus $\swhile{\mtrue}{\sskip}$ afleiden, waarna we weer hetzelfde kunnen doen (en blijven doen).
+\end{itemize}
+
+\end{document}
+