add guardians to algorithmic type system

new_system3.tex

@@ -148,6 +148,8 @@ TODO: Theorems and proof: no need for rule Inter, etc.
 \\
 \Infer[ProjDom]
 {\Gamma(x) = t\\
+t\land(\pair{\Any}{\Any})\neq\Empty\\
+t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
 \Gamma\subst{x}{t\land(\pair{\Any}{\Any})}\vdash_e e: \{(u_i,\Gamma_i)\}_{i\in I}\\
 \Gamma\subst{x}{t\land\neg(\pair{\Any}{\Any})}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J}
 }
@@ -181,8 +183,8 @@ TODO: Theorems and proof: no need for rule Inter, etc.
 \Infer[AppRDom]
 {
   \Gamma(x_1)\equiv \textstyle\bigwedge_{i\in I}\arrow {s_i}{t_i}\\
-  \Gamma(x_2)=s\\
   s_\circ=\textstyle\bigvee_{i\in I}s_i\\
+  \Gamma(x_2)=s\\s\land s_\circ\neq\Empty\\s\land \neg s_\circ\neq\Empty\\
   \Gamma\subst{x_2}{s\land s_\circ}\vdash_e e: \{(u_i,\Gamma_i)\}_{i\in I}\\
   \Gamma\subst{x_2}{s\land \neg s_\circ}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J}
 }
@@ -190,20 +192,22 @@ TODO: Theorems and proof: no need for rule Inter, etc.
 { }
 \\
 \Infer[AppL*]
-{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}\arrow{s_i}{t_i}\\
-\forall i\in I.\ \Gamma\subst{x_1}{\arrow{s_i}{t_i}}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J_i}
+{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}t_i\leq\arrow{\Empty}{\Any}\\
+\forall i\in I.\ \Gamma\subst{x_1}{t_i}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J_i}
 }
 {\Gamma \vdash_e {x_1}{x_2}: \bt\{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}}
 { }
 \\
 \Infer[AppLDom]
-{\Gamma(x_1) = t\\
+{\Gamma(x_1) = t\\t\land (\arrow{\Empty}{\Any})\neq\Empty\\t\land \neg (\arrow{\Empty}{\Any})\neq\Empty\\
 \Gamma\subst{x_1}{t\land(\arrow{\Empty}{\Any})}\vdash_e e: \{(u_i,\Gamma_i)\}_{i\in I}\\
 \Gamma\subst{x_1}{t\land\neg(\arrow{\Empty}{\Any})}\vdash_e e: \{(u_j,\Gamma_j)\}_{j\in J}
 }
 {\Gamma \vdash_e {x_1}{x_2}: \bt\{(u_i,\Gamma_i)\}_{i\in I}\cup\{(u_j,\Gamma_j)\}_{j\in J}}
 { }
-\\
+\end{mathpar}
+
+\begin{mathpar}
 \Infer[CaseThen]
 {
 \Gamma(x)=t_\circ\\t_\circ\leq t\\