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