-\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
+Om het bovenste element van een stack te dupliceren gebruiken we de
+volgende functie:\\
+$$\mathcal{DUP} : Stack \rightarrow Stack$$
+$$\mathcal{DUP} [\:] = [\:]$$
+$$\mathcal{DUP} [a:rest] = [a:a:rest] $$\\
+
+Om de bovenste twee elementen van een stack op te tellen gebruiken we de
+volgende functie:\\
+$$\mathcal{NOT} : Stack \rightarrow Stack$$
+$$\mathcal{NOT} [\:] = [\:]$$
+$$\mathcal{NOT} [a:rest] = [0:rest] \: \text{if} \: a \neq 0$$
+$$\mathcal{NOT} [a:rest] = [1:rest] \: \text{if} \: a = 0$$\\
+
+Om de bovenste twee elementen van een stack op te tellen gebruiken we de
+volgende functie:\\
+$$\mathcal{GRE} : Stack \rightarrow Stack$$
+$$\mathcal{GRE} [\:] = [\:]$$
+$$\mathcal{GRE} [a] = [a] $$
+$$\mathcal{GRE} [a:b:rest] = [0:rest] \: \text{if} \: a \geq b$$
+$$\mathcal{GRE} [a:b:rest] = [1:rest] \: \text{if} \: a < b$$\\
+
+Met behulp van deze gedefineerde functies kunnen we nu de volgende semantiekregels opstellen:\\
+
+$
+{[pop_{sos}]}\qquad
+\langle pop, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o,\mathcal{D}(s)\rangle\\
+{[add_{sos}]}\qquad
+\langle add, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{ADD}(s)\rangle\\
+{[subtract_{sos} ]}\qquad
+\langle subtract, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{SUB}(s)\rangle\\
+{[multiply_{sos}]}\qquad
+\langle multiply, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{MUL}(s)\rangle\\
+{[divide_{sos}]} \qquad
+\langle divide, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{DIV}(s)\rangle\\
+{[mod_{sos}]} \qquad\qquad
+\langle mod, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{MOD}(s)\rangle\\
+{[duplicate_{sos}]} \qquad
+\langle duplicate, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{DUP}(s)\rangle\\
+{[not_{sos}]}\qquad\qquad
+\langle not, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{NOT}(s)\rangle\\
+{[greater_{sos}]} \qquad
+\langle greater, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{GRE}(s)\rangle \qquad \\