From fcc62f10bc11948534a4571a052ee87e0627d4f4 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Tue, 16 Feb 2016 10:28:20 +0100
Subject: Fix task 2

---
 task2.tex | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'task2.tex')

diff --git a/task2.tex b/task2.tex
index a85aa89..9a2c87f 100644
--- a/task2.tex
+++ b/task2.tex
@@ -24,7 +24,7 @@ Zie Figuur \ref{fig:boom}.
 Hier geldt:
 
 \begin{align*}
-    s_0 &= [x\mapsto17, y\mapsto5]\\ %todo
+    s_0 &= s[x\mapsto17, y\mapsto5]\\ %todo
     s_1 &= s_0[z\mapsto0]\\
     s_2 &= s_1[z\mapsto1]\\
     s_3 &= s_2[x\mapsto12]\\
@@ -68,20 +68,19 @@ Hier geldt:
 
 \section*{Het \texttt{do} statement}
 \subsection*{Syntax}
-We voegen een regel $S ::= \sdowhile{S}{b}$ toe.
+$S ::= \ldots \mid \sdowhile{S}{b}$.
 
 \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}
+\trans{S}{s}{s'} \quad \trans{\swhile{b}{S}}{s'}{s''}
+\justifies \trans{\sdowhile{S}{b}}{s}{s''}
 \end{prooftree}$$
 
 \section*{Opdracht 2.4}
 \begin{itemize}
-    \item Termineert als $x\ge1$, anders niet.
+    \item Termineert op toestanden $s$ waarvoor $s(x)\ge1$. Loopt op alle andere toestanden.
     \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).
+    \item Loopt op alle toestanden. $\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}
-- 
cgit v1.2.3

