@@ -598,7 +598,7 @@ In the example with \code{\(t=(\Int \to \Int)\) \(\wedge\) \((\Bool \to \Bool)\)

The first two operators belongs to the theory of semantic subtyping while the last one is new and we described it in Section~\ref{sec:ideas}

We need similar operators for projections since the type $t$ of $e$ in $\pi_i e$ may not be a single product type but, say, a union of products: all we know is that $t$ must be a subtype of $\pair\Any\Any$. So let $t$ be a type such that $t\leq\pair\Any\Any$) then we define:

We need similar operators for projections since the type $t$ of $e$ in $\pi_i e$ may not be a single product type but, say, a union of products: all we know is that $t$ must be a subtype of $\pair\Any\Any$. So let $t$ be a type such that $t\leq\pair\Any\Any$, then we define:

\begin{eqnarray}

\bpl t & = &\min\{ u \alt t\leq\pair u\Any\}\\

\bpr t & = &\min\{ u \alt t\leq\pair\Any u\}

...

...

@@ -609,7 +609,7 @@ All the operators above but $\worra{}{}$ are already present in the theory of se

\worra t s = \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P\subset P_i\alt s\leq\bigvee_{p \in P}\neg t_p\}}\left(\bigvee_{p \in P}\neg s_p\right) \right)

\end{equation}

\beppe{Explain the formula?}

The proof that this type satisfies \eqref{worra} is given in the Appendix~ref{}.

The proof that this type satisfies \eqref{worra} is given in the Appendix~\ref{}.