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

triangle operator

parent 27997821
......@@ -118,6 +118,7 @@ TODO: Theorems and proof: no need for rule Inter, etc.
\apply t s & = & \bigvee_{i\in I}\left(\bigvee_{\{Q\subsetneq P_i\alt s\not\leq\bigvee_{q\in Q}s_q\}}\left(\bigwedge_{p\in P_i\setminus Q}t_p\right)\right)\hspace*{1cm}\makebox[0cm][l]{(for $s\leq\dom{t}$)}\\[4mm]
\worra t s & = & \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\[4mm]
%\worra t s & = & \left\{\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n'),\ \dom t \wedge\bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\ |\ i\in I\right\}
t \btr s & = & \bigwedge_{i\in I}\left(\bigvee_{\{P \subseteq P_i\alt \bigwedge_{p \in P} t_p \leq s\}} \left(\bigwedge_{p \in P} s_p \right)\right)
\end{eqnarray*}
The elements of $\Gamma\avdash\Gammap\ct e:S$ mean:
......
......@@ -306,6 +306,7 @@
\newcommand{\tree}[0]{\mathcal{T}}
\newcommand{\ttype}[0]{\texttt{type}}
\newcommand{\tleaves}[0]{\texttt{leaves}}
\newcommand{\btr}[0]{\blacktriangleright}
\makeatletter % allow us to mention @-commands
\def\arcr{\@arraycr}
......
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