fix

new_system3.tex

@@ -332,8 +332,8 @@ rules, because one branch is already unreachable and retyping only occurs with s
 \\
   \Infer[Pair]
   {
-   \forall i\in I.\ \Gamma_1^i = \subst{x_1}{t_i}\\
-   \forall i\in I.\ \Gamma_2^i = \subst{x_2}{s_i}
+   \forall i\in I.\ \Gamma_1^i = \{x_1:t_i\}\\
+   \forall i\in I.\ \Gamma_2^i = \{x_2:s_i\}
   }
   {\Gamma\bvdash {(x_1,x_2)} {\bigcup_{i\in I}(t_i,s_i)} \textstyle\bigcup_{i\in I}\{\Gamma_1^i\land\Gamma_2^i\}}
   { }
@@ -352,8 +352,8 @@ rules, because one branch is already unreachable and retyping only occurs with s
   {
   \Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}\textstyle\bigwedge_{j\in J_i}\arrow {s_j}{t_j}\\  
   \forall i\in I.\ \worra{(\textstyle\bigwedge_{j\in J_i}\arrow {s_j}{t_j})}t = s_i' \\
-  \forall i\in I.\ \Gamma_1^i = \subst{x_1}{\textstyle\bigwedge_{j\in J_i}\arrow {s_j}{t_j}}\\
-  \forall i\in I.\ \Gamma_2^i = \subst{x_2}{s_i'}
+  \forall i\in I.\ \Gamma_1^i = \{x_1:\textstyle\bigwedge_{j\in J_i}\arrow {s_j}{t_j}\}\\
+  \forall i\in I.\ \Gamma_2^i = \{x_2:s_i'}
   }
   {
     \Gamma\bvdash {(x_1\ x_2)} {t} \textstyle\bigcup_{i\in I}\{\Gamma_{1}^i\land\Gamma_{2}^i\}
@@ -440,8 +440,8 @@ $x$ is supposed to be included into $t_x$ or $\neg t_x$.
 \\
   \Infer[Pair]
   {
-   \forall i\in I.\ \Gamma_1^i = \subst{x_1}{t_i}\\
-   \forall i\in I.\ \Gamma_2^i = \subst{x_2}{s_i}
+   \forall i\in I.\ \Gamma_1^i = \{x_1:t_i\}\\
+   \forall i\in I.\ \Gamma_2^i = \{x_2:s_i\}
   }
   {\Gamma\fvdash {(x_1,x_2)} {\bigcup_{i\in I}(t_i,s_i)} \textstyle\bigcup_{i\in I}\{\Gamma_1^i\land\Gamma_2^i\}}
   { }
@@ -458,12 +458,13 @@ $x$ is supposed to be included into $t_x$ or $\neg t_x$.
 \\
   \Infer[App]
   {
-  \Gamma(x_1) \btr t = s \\
-  \Gamma_1 = \subst{x_1}{\Gamma(x_1)}\\
-  \Gamma_2 = \subst{x_2}{s}
+  \Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}\textstyle\bigwedge_{j\in J_i}\arrow {s_j}{t_j}\\  
+  \forall i\in I.\ (\textstyle\bigwedge_{j\in J_i}\arrow {s_j}{t_j})\btr t = s_i' \\
+  \forall i\in I.\ \Gamma_1^i = \{x_1:\textstyle\bigwedge_{j\in J_i}\arrow {s_j}{t_j}\}\\
+  \forall i\in I.\ \Gamma_2^i = \{x_2:s_i'\}
   }
   {
-    \Gamma\fvdash {(x_1\ x_2)} {t} \{\Gamma_{1}\land\Gamma_{2}\}
+    \Gamma\bvdash {(x_1\ x_2)} {t} \textstyle\bigcup_{i\in I}\{\Gamma_{1}^i\land\Gamma_{2}^i\}
   }
   { }
 \\