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

fix

parent 1a5361ee
......@@ -353,7 +353,7 @@ 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 = \{x_1:\textstyle\bigwedge_{j\in J_i}\arrow {s_j}{t_j}\}\\
\forall i\in I.\ \Gamma_2^i = \{x_2:s_i'}
\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\}
......@@ -402,8 +402,8 @@ NOTE: The declarative rule for the application is as follows:
\Infer[App]
{\Gamma(x_1)\equiv\textstyle\bigvee_{i\in I}u_i \\
\forall i\in I.\ u_i\leq \arrow{\neg s_i}{t_i} \text{ with } t_i\land t = \varnothing \\
\forall i\in I.\ \Gamma_1^i = \subst{x_1}{u_i}\\
\forall i\in I.\ \Gamma_2^i = \subst{x_2}{s_i}
\forall i\in I.\ \Gamma_1^i = \{x_1:u_i\}\\
\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\}
......
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