trying some new rules... (wip)

new_system2.tex

@@ -137,43 +137,10 @@ TODO: Simplify pairs (only with variables) + simplify grammar accordingly (no ne
   { }
 \end{mathpar}
 
-% \begin{mathpar}
-% \Infer[ProjC]
-% {\Gamma \vdash x:\textstyle\bigcup_{j\in J}\pair{t_1^j}{t_2^j}}
-% {\Gamma \cvdash \pi_i x: \{(t_i^j, \Gamma\subst{x}{\pair{t_1^j}{t_2^j}})\ \alt\ j\in J\}}
-% { }
-% \\
-% \Infer[AppC]
-% {
-%   \Gamma \vdash x: \textstyle\bigcup_{i\in I}t_i\quad
-%   \forall i\in I.\ t_i\leq \arrow{t}{s_i}\quad
-%   \Gamma \vdash y: t
-% }
-% { \Gamma \cvdash {x}{y}: \{(s_i, \Gamma\subst{x}{t_i})\ \alt\ i\in I\} }
-% { }
-% \\
-% \Infer[CaseC]
-% {
-% \Gamma_1 = \Gamma\subst{x}{\Gamma(x)\land t}\\
-% \Gamma_2 = \Gamma\subst{x}{\Gamma(x)\land \neg t}\\
-% \Gamma_1 \vdash e_1:t_1\\
-% \Gamma_2 \vdash e_2:t_2}
-% {\Gamma\cvdash \tcase {x} t {e_1}{e_2}: \{(t_1, \Gamma_1), (t_2, \Gamma_2)\}}
-% { }
-% \\
-% \Infer[AtomicC]
-% {\Gamma \vdash a:t}
-% {\Gamma \cvdash a: \{(t, \Gamma)\}}
-% { }
-% \end{mathpar}
-
 TODO: Inter rule needed?
 
 TODO: Algorithmic rules
 
-% TODO: AppC rule: what about the argument? We could loose precision there...
-% In the end, these rules look quite similar to the candidate generation rules.
-
 \subsection{Candidates generation rules}
 
 \begin{mathpar}
@@ -186,7 +153,7 @@ TODO: Algorithmic rules
   \Infer[Var*]
   {
   }
-  { \Gamma \vdash y \triangleright_x \{\} }
+  { \Gamma \vdash x \triangleright_x \{\} }
   {}
 \hfill
   \Infer[Const]
@@ -233,11 +200,11 @@ TODO: Algorithmic rules
    \Infer[Proj]
           { }
           {\Gamma \vdash \pi_i y\triangleright_x\{\}}
-          {y\neq x}
+          {}
   \hfill
   \Infer[Proj*]
-    {\Gamma \vdash x:\textstyle{\bigvee_{i \in I}t_i}}
-    {\Gamma \vdash \pi_i x\triangleright_x\textstyle{\bigcup_{i\in I} \{t_i\}}}
+    { }
+    {\Gamma \vdash \pi_i x\triangleright_x\{\}}
     {}
   \\
   \Infer[CaseTest*]