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{amssymb}
 \usepackage{graphicx}
 \usepackage{xcolor}

+\usepackage{proof}

 
 \graphicspath{{./img/}}
 
 
 \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.\\ 
 
 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$$\\
 \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.\\
 
 $$\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