example for reductions

proofs.tex

@@ -141,7 +141,7 @@
     
     \newpage
 
-    \subsection{Full parallel semantics}\label{app:parallel}
+    \subsection{Parallel semantics}\label{app:parallel}
 
     \[
       \begin{array}{lrcl}
@@ -205,6 +205,29 @@
       \\
       \end{mathpar}
 
+      Here is an example of reduction using the parallel semantics:
+
+      \begin{mathpar}
+        \Infer[TestCtx]
+        {
+          \Infer[Ctx]
+          {\Infer[App] { } {(\lambda x.\ x+1)\ 1\idleadsto 2} {}}
+          {((\lambda x.\ x+1)\ 1, \true)\xleadsto{(\lambda x.\ x+1)1\ \mapsto\ 2} (2, \true)}
+          {}
+        }
+        {\ite {((\lambda x.\ x+1)\ 1, \true)} {\pair \Int \Bool} {(\lambda x.\ x+1)\ 1} {0} \idleadsto \ite {(2, \true)} {\pair \Int \Bool} {2} {0}}
+        {}
+      \end{mathpar}
+
+      and
+
+      \begin{mathpar}
+        \Infer[Case]
+        {(2, \true) \in \valsemantic {\pair \Int \Bool}}
+        {\ite {(2, \true)} {\pair \Int \Bool} {2} {0} \idleadsto 2}
+        {}
+      \end{mathpar}\\
+
       All the proofs below will use the parallel semantics instead of the standard semantics (\ref{sec:opsem}).
       However, the safety of the type system for the standard semantics can be deduced from the safety of the type system for the parallel semantics,
       using the following lemma: