From cdb22510a8640a4a12a4e797dcb9d880226c3157 Mon Sep 17 00:00:00 2001
From: Evi
Date: Fri, 10 Jun 2016 10:26:53 +0200
Subject: exec ipv tweede compositie regel

---
 sosexamp.tex | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/sosexamp.tex b/sosexamp.tex
index 0fe065a..e3926e8 100644
--- a/sosexamp.tex
+++ b/sosexamp.tex
@@ -22,34 +22,34 @@ en lezen we als
 
  Je kunt de structurele operationele semantiek zoals bij de natuurlijke semantiek definiëren aan de hand van de  $\lambda$-regel maar om juist het verschil aan te geven met als je gebruik maakt van compositieregels, hebben wij ervoor gekozen om de structurele operationele semantiek te definiëren gebruik makende van compositieregels. 
 
-De twee compositieregels zijn als volgt:
+De compositieregel is dan als volgt:
 
 $$
 \begin{prooftree}
-	\sostrans
+	\sostranseind
 		{\stm}{\ip}{\op}{(\stk, \str)}
-		{\pgm'}{\ip'}{\op'}{(\stk', \str')}
+		{\ip'}{\op'}{(\stk', \str')}
 	\justifies
 	\sostrans
 		{\stm:\pgm}{\ip}{\op}{(\stk,\str)}
-		{\pgm'}{\ip'}{\op'}{(\stk',\str')}
+		{\pgm}{\ip'}{\op'}{(\stk',\str')}
 	\using{\rcompeensos}
 	\qquad
 \end{prooftree}
 $$
 
-\medskip
+\bigskip
+
+De regel voor $\StmExec$ zou in de structurele operationele semantiek als volgt zijn: 
 $$
 \begin{prooftree}
-	\sostranseind
-		{\stm}{\ip}{\op}{(\stk, \str)}
-		{\ip'}{\op'}{(\stk', \str')}
-	\justifies
+\axjustifies
 	\sostrans
-		{\stm:\pgm}{\ip}{\op}{(\stk,\str)}
-		{\pgm}{\ip'}{\op'}{(\stk',\str')}
-	\using{\rcomptweesos}
+		{\StmExec:\pgm}{\ip}{\op}{(\stk,\str)}
+		{\pgm'}{\ip'}{\op'}{(\stk',\str')}
+	\using{\rexecsos}
 	\qquad
+		\text{met $\pop{\stk} = ( \pgm', \stk'')$.}
 \end{prooftree}
 $$
 
-- 
cgit v1.2.3