Commit f2848b7a authored by Mickael Laurent's avatar Mickael Laurent
Browse files

simplification

parent 41bc21f7
......@@ -366,13 +366,11 @@ TODO: Algorithmic rules
\\
\Infer[Pair]
{%\forall i\in I.\ \Gamma\bvdash{x_1}{t_i}\{(t_i^j,\Gamma_{1,i}^j)\}_{j\in J_i}\\
\Gamma\vdash x_1:t_\circ\\
\Gamma\vdash x_2:s_\circ\\
\forall i\in I.\ \Gamma_1^i = \Gamma\subst{x_1}{t_\circ\land t_i}\\
\forall i\in I.\ \Gamma_1^i = \Gamma\subst{x_1}{t_i}\\
%\forall i\in I.\ \Gamma\bvdash{x_2}{s_i}\{(s_i^k,\Gamma_{2,i}^k)\}_{k\in K_i}
\forall i\in I.\ \Gamma_2^i = \Gamma\subst{x_2}{s_\circ\land s_i}\\
\forall i\in I.\ \Gamma_2^i = \Gamma\subst{x_2}{s_i}\\
}
{\Gamma\bvdash {(x_1,x_2)} {\bigcup_{i\in I}(t_i,s_i)} \bigcup_{i\in I}\{(\pair{(t_\circ\land t_i)}{(s_\circ\land s_i)}, \Gamma_1^i\land\Gamma_2^i)\}}
{\Gamma\bvdash {(x_1,x_2)} {\bigcup_{i\in I}(t_i,s_i)} \bigcup_{i\in I}\{(\pair{t_i}{s_i}, \Gamma_1^i\land\Gamma_2^i)\}}
{ }
\\
\Infer[Proj]
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment