exec ipv tweede compositie regel

1 files 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}
 $$