cleaned up code

diff --git a/project.tex b/project.tex
index 20c24e4..a1fed4e 100644 (file)
--- a/project.tex
+++ b/project.tex
@@ -6,6 +6,7 @@
 \usepackage{amssymb}
 \usepackage{graphicx}
 \usepackage{xcolor}
+\usepackage{proof}
 
 \graphicspath{{./img/}}
 

diff --git a/semantics.tex b/semantics.tex
index e977049..fb4c747 100644 (file)
--- a/semantics.tex
+++ b/semantics.tex
@@ -16,8 +16,6 @@ $\langle S, s_i, s_o, s\rangle\Rightarrow\langle s_i', s_o', s'\rangle$\\
 Waarbij de laatste transitie duidt op een terminerende transitie en de eerste
 op een niet terminerende transitie.\\ 
 
-
-
 \subsection{Semantiek beschrijving}
 Om het eerste element van een stack weg te kunnen gooien gebruiken we de volgende functie:\\
 $$\mathcal{D} : s \rightarrow s$$\\
@@ -27,28 +25,99 @@ Om een stack uit te kunnen breiden met een element gebruiken we de volgende func
 $$\mathcal{E} : s, \mathbb{Z} \rightarrow s$$\\
 Deze functie neemt een stack en een integer en voegt de integer toe bovenop de stack.\\
 
-$[delete_{sos} ] \; <delete, s_i, s_o, s> \Rightarrow <s_i, s_o,\mathcal{D}[s]>$\\
-
-$[extend_{sos} ] \; <extend \: z, s_i, s_o, s> \Rightarrow <s_i, s_o,\mathcal{E}[s, z]>$\\
-
-$[pop_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>}{<pop, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>}$\\
-
-$[add_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\: x+y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<add \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
-
-$[subtract_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\:  x-y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<subtract \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
-
-$[multiply_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\:  x*y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<multiply \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
-
-$[divide_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\: x/y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<divide \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
-
-$[mod_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\:  x \: mod \: y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<mod \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
-
-$[duplicate_{sos} ] \; \frac{<extend\: x, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>}{<duplicate \: x, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>}$\\
-
-$[not^0_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <extend\: 1, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''>}{<not \: x, s_i, s_o, s> \Rightarrow <s_i, s_o, s''>}$ if x = 0\\
-
-$[not^*_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <extend\: 0, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''>}{<not \: x, s_i, s_o, s> \Rightarrow <s_i, s_o, s''>}$ if x $\neq$ 0\\
-
-$[greater^<_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\:,1, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<greater \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$ if x$<$y\\
-
-$[greater^>_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\: 0, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<greater \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$ if x$>$y\\
\ No newline at end of file
+\footnotesize
+$\infer        [{[}delete_{sos}{]}]
+               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i,s_o,\mathcal{D}[s]\rangle}{}\\
+\infer [{[}extend_{sos}{]}]
+               {       \langle extend \: z, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o,\mathcal{E}[s, z]\rangle}{}\\
+\infer [{[}pop_{sos} {]}]
+               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'\rangle}
+               {       \langle pop, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'\rangle}\\
+\infer [{[}add_{sos} {]}]
+               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'\rangle \quad
+                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
+                               \langle s_i, s_o, s''\rangle \quad
+                       \langle extend\: x+y, s_i, s_o, s''\rangle \Rightarrow
+                               \langle s_i, s_o, s'''\rangle}
+               {       \langle add \: x,y, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'''\rangle}\\
+\infer [{[}subtract_{sos} {]}]
+               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'\rangle \quad
+                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
+                               \langle s_i, s_o, s''\rangle \quad
+                       \langle extend\: x-y, s_i, s_o, s''\rangle \Rightarrow
+                               \langle s_i, s_o, s'''\rangle}
+               {       \langle subtract \: x,y, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'''\rangle}\\
+\infer [{[}multiply_{sos} {]}]
+               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'\rangle \quad
+                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
+                               \langle s_i, s_o, s''\rangle \quad
+                       \langle extend\: x*y, s_i, s_o, s''\rangle \Rightarrow
+                               \langle s_i, s_o, s'''\rangle}
+               {       \langle multiply \: x,y, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'''\rangle}\\
+\infer [{[}divide_{sos} {]}]
+               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'\rangle \quad
+                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
+                               \langle s_i, s_o, s''\rangle \quad
+                       \langle extend\: x/y, s_i, s_o, s''\rangle \Rightarrow
+                               \langle s_i, s_o, s'''\rangle}
+               {       \langle divide \: x,y, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'''\rangle}\\
+\infer [{[}mod_{sos} {]}]
+               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'\rangle \quad
+                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
+                               \langle s_i, s_o, s''\rangle \quad
+                       \langle extend\: x \: mod \: y, s_i, s_o, s''\rangle \Rightarrow
+                               \langle s_i, s_o, s'''\rangle}
+               {       \langle mod \: x,y, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'''\rangle}\\
+\infer [{[}duplicate_{sos} {]}]
+               {       \langle extend\: x, s_i, s_o, s\rangle \Rightarrow
+                       \langle s_i, s_o, s'\rangle}
+               {       \langle duplicate \: x, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'\rangle}\\
+\infer [{[}not^0_{sos} {]}]
+               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'\rangle \quad
+                       \langle extend\: 1, s_i, s_o, s'\rangle \Rightarrow
+                               \langle s_i, s_o, s''\rangle}
+               {       \langle not \: x, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s''\rangle}$ if $x = 0\\
+\infer [{[}not^*_{sos} {]}]
+               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'\rangle \quad 
+                       \langle extend\: 0, s_i, s_o, s'\rangle \Rightarrow
+                               \langle s_i, s_o, s''\rangle}
+               {       \langle not \: x, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s''\rangle}$ if $x\neq 0\\
+\infer [{[}greater^<_{sos} {]}]
+               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'\rangle \quad 
+                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
+                               \langle s_i, s_o, s''\rangle \quad 
+                       \langle extend\:,1, s_i, s_o, s''\rangle \Rightarrow 
+                               \langle s_i, s_o, s'''\rangle}
+               {       \langle greater \: x,y, s_i, s_o, s\rangle \Rightarrow
+                       \langle s_i, s_o, s'''\rangle}$ if $x>y\\
+\infer [{[}greater^>_{sos} {]}]
+               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
+                               \langle s_i, s_o, s'\rangle \quad 
+                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
+                               \langle s_i, s_o, s''\rangle \quad 
+                       \langle extend\: 0, s_i, s_o, s''\rangle \Rightarrow 
+                               \langle s_i, s_o, s'''\rangle}
+               {       \langle greater \: x,y, s_i, s_o, s\rangle \Rightarrow 
+                               \langle s_i, s_o, s'''\rangle}$ if $x<y
+$
+\normalsize