Commit 4c763865 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

trying some new rules... (wip)

parent 15f67411
......@@ -351,6 +351,11 @@ TODO: Algorithmic rules
{\Gamma\vdash e:t' \\ \Gamma\bvdash e {t\wedge t'} \{(t_i, \Gamma_i)\}_{i\in I}}
{\Gamma\bvdash e t \{(t_i, \Gamma_i)\}_{i\in I}}
{ }
% \qquad
% \Infer[Inter2]
% {\Gamma\bvdash e t \{(t_i, \Gamma_i)\}_{i\in I}\\\forall i\in I.\ \Gamma_i\vdash e:t_i}
% {\Gamma\bvdash e t \{(t_i\land t_i', \Gamma_i)\}_{i\in I}}
% { }
\\
\Infer[EFQ]
{ }
......@@ -363,11 +368,11 @@ TODO: Algorithmic rules
{ }
\\
\Infer[App]
{\Gamma\vdash e_1:\bigvee_{i\in I}u_i \\ \Gamma\vdash e_2:t_2\\
\forall i\in I.\ u_i\leq \arrow{(\neg t_i \land t_2)}{s_i'} \text{ with } s_i'\land t = \varnothing \\
\forall i\in I.\ u_i\leq \arrow{t_i}{s_i}\\
\forall i\in I.\ \Gamma\bvdash{e_1}{u_i}\{(\_, \Gamma_{1,i}^j)\}_{j\in J_i} \\ \forall i\in I.\ \Gamma\bvdash{e_2}{t_i}\{(\_, \Gamma_{2,i}^k)\}_{k\in K_i}}
{\Gamma\bvdash {(e_1\ e_2)} {t} \bigcup_{i\in I}\{(s_i, \Gamma_{1,i}^j\land\Gamma_{2,i}^k)\ |\ j\in J_i, k\in K_i\}}
{\Gamma\vdash e_1:\bigvee_{i\in I}u_i \\
\forall i\in I.\ u_i\leq \arrow{\neg t_i}{s_i} \text{ with } s_i\land t = \varnothing \\
\forall i\in I.\ \Gamma\bvdash{e_1}{u_i}\{(u_i^j, \Gamma_{1,i}^j)\}_{j\in J_i} \\ \forall i\in I.\ \Gamma\bvdash{e_2}{t_i}\{(t_i^k, \Gamma_{2,i}^k)\}_{k\in K_i}\\
\forall i\in I.\ \forall j\in J_i.\ \forall k\in K_i.\ u_i^j\leq\arrow{t_i^k}{s_i^{j,k}}}
{\Gamma\bvdash {(e_1\ e_2)} {t} \bigcup_{i\in I}\{(s_i^{j,k}, \Gamma_{1,i}^j\land\Gamma_{2,i}^k)\ |\ j\in J_i, k\in K_i\}}
{ }
\\
\Infer[Case]
......
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