\section{Context Schemata}
\label{sec:runtime}
\renewcommand{\emp}{\cdot;\top}

In this Section we address the properties of contexts\footnote{This
  section is inspired by Sch\"{u}rmann's treatment of similar material
  in his  dissertation \cite{Schurmann00phd}.}. %  We
% restrict to third-order programs, namely to programs which make
% only Horn assumptions; this is enough to achieve satisfaction of
% boolean axioms for the algebra of clause complementation.
%(Section \ref{ssec:ccalgebra}).
Hereditary Harrop formulae differ from Horn clauses in that they may
dynamically extend the current signature and program; this is
reflected in the provability (and denial) relation which is
parameterized by a run-time context $\ga$. As we have argued before
(Section \ref{sec:lamrelated}) we cannot obtain closure under clause
complementation for the full logic of HHF, but we have to restrict
ourselves to
a smaller (but significant) fragment. This in turn entails that we
have to make sure that during execution whenever an assumption is
made, the latter stays in the fragment we have isolated.  Technically,
we proceed as follows:
\begin{itemize}
\item We extract from the static definition of a predicate the general
  `template' of a legal assumption.
\item We require dynamic assumptions to conform to this template.
\end{itemize}
 
We thus introduce the notion of \emph{schema satisfaction}, for which we will
need the following data structure: a \emph{schema context} abstracts
over all possible instantiation of a run-time context. To account for
that, we introduce a quantifier-like operator, say $\some{\Phi} \cD$,
which takes a clause and existentially bounds its free variables, \ie
the global parameters occurring in $\cD$. % : we denote this restriction
% of $\Phi$ to $\cD$ with $\Phi_{\cD}$, defined as $\Phi_{\cD}=\Phi\cap
% FV(\cD)$.
%$\Phi=FV(\cD)$. As usual,
%we implicitly annotate those variables with their types.
 We use the following reification of schemata: do not confuse
`$\mbar$', which is used to represent schema alternatives in the object
language with `$\bnfalt$' which does the same in our informal
meta-language.

\[ \begin{array}{rrcl}
\mbox{\textit{ Contexts Schemata}}& \cS & \bnfas &
\ecs\bnfalt\cS\mbar(\GG;\some{\Phi} \cD)
\end{array}\]

\begin{Example} The schema context grammar induced by the
  \texttt{linear} predicate (Example \ref{ex:linear}) is as follows:
\beq
\cS_{linear} & = &  \ecs\mbar x\oftp exp;linear(x)\mbar x\oftp exp;\top_{linx}  
%\cS_{linear} & = & \ecs\bnfalt\cS_{linear}\mbar x\oftp
%exp;linear(x)\bnfalt\cS_{linear}\mbar x\oftp exp;\top_{linx}  
\eneq
while a possible run-time context is
$$y_1\oftp exp,y_2\oftp exp,y_3\oftp exp;\top_{linx}\And
\top_{linx}\And linear(y_3)$$
Since every possible assumption is
closed, there are no existential bindings. Consider instead the clauses
for type-checking in the simply typed calculus:
\beq
ofapp & : & \PI{E_1,E_2}{exp}\PI{T_1,T_2,T}{tp}\\
&& of\ (app\ E_1\ E_2) \ T_2\\
&&\qquad \If of\ E_1\ (arrow\ T_1\ T_2)\\
&&\qquad \If of\ E_2\ T_1.\\
oflam &:&  \PI{E}{exp\Imp exp}\PI{T_1,T_2}{tp}\\
&& of\ lam(E) \  (arrow\ T_1\ T_2)\\
& & \qquad\If( \PI{x}{exp} of\ x\ T_1 \Imp  of\ (E\ x) \ T_2).
\eneq
Then the schema context is:
\beq
\cS_{of} & = &  \ecs\mbar x\oftp exp;\some{u\hastype tp}
of\ x\ u 
%%\cS_{of} & = & \ecs\bnfalt\cS_{of}\mbar x\oftp exp;\some{u\hastype tp}
%of\ x\ u 
\eneq
where `$u$' is a global parameter.
\end{Example}

We will also need to disambiguate \emph{blocks} in run-time contexts;
overlapping may indeed happen when the alternatives in a context
schema are not disjoint.  For example, suppose we are given the
following schema and partial run-time context:
\beq
\cS & = &  \ecs\mbar x\oftp exp;p(x)\mbar x\oftp exp;p(x)\And q(x) 
%%\cS & = & \ecs\bnfalt\cS\mbar x\oftp exp;p(x)\bnfalt\cS\mbar x\oftp
%%exp;p(x)\And q(x) 
\eneq
$$y_1\oftp exp,y_2\oftp exp;p(y_1)\And p(y_2)$$

It is not uniquely determined whether, say, $p(y_2)$ is an instance of the
first alternative or a prefix of the second one.  To determine that,
we simply modify the provability and denial rules $\vd\atm$ and
$\nvd\atm$ by `packaging' run-time contexts into blocks with a bracket
operator $\block{ \cdot }$.  Intuitively, a block is complete when an
atomic conclusion is reached during the deduction.  It is therefore
bracketed when the run-time context is passed to the immediate
implication judgment.
\beq 
\ibnc{D\inn\cP\And\cD}{\block{\GG};\block{\cD}\sp D\imm Q}{\ga\sp Q}{\vd\atm}
\qquad
\ibnc{\mbox{for every }D\inn\cP\And\cD}{\block{\GG};\block{\cD}\fp D \nimm Q}{\ga\fp Q}{\nprv\atm}
\eneq
Still, we need to `flatten' blocks, so that re-bracketing during
execution will be immaterial on already delimited blocks;
we thus require the bracket operator to satisfy the following
absorption-distribution law:
\beq
\block{\block{\GG},\GG'} & = & \block{ \GG},\block{ \GG'}\\
\block{ \block{ \cD} \And\cD'} & = & \block{ \cD} \And\block{ \cD'} 
\eneq

\smallskip We are now ready to introduce schema satisfaction; this is
accomplished by the following judgments:
% depicted in Figure~\ref{fig:schemaG}:
\begin{itemize}
\item $\dsat D$: clause $D$ satisfies schema $\cS$.
\item $\ga\sla G\inss$:  (partial) run-time context
  $\ga$ together with goal $G$ satisfies schema $\cS$.
\item $\ga\inss$: (completed) run-time context $\ga$  satisfies schema $\cS$.
\item $\GG\vd\gap\in\cS$: block $\gap$ in context $\GG$ occurs in schema $\cS$.
\end{itemize}
 First, we say that a completed block
\emph{occurs} in a schema when 
%there is a well typed substitution $\q$ such that 
the  block is an alphabetic variant of some 
instantiation of one of the alternatives of the schema:
%we recall that the
%domain of a well-typed substitution is $FV(D)\sla\dom(\GG)$.
% , \ie the pool of global parameters
% % introduced by the $\dsat\Pi$ and $\sla\exists$ rules
% , while the domain is $\GG$.
\beq
\ibnc{\GG\vd\q\hastype\Phi}{(\GG';\cD')\equiv_{\alpha}(\GG'';[\q]\cD)}
{\GG\vd(\GG';\cD')\in \cS\mbar
(\GG'';\some{\Phi} \cD)}{\in_1} \qquad 
\ianc{\GG\vd(\GG';\cD')\in\cS}{\GG\vd(\GG';\cD')\in \cS\mbar(\GG'';\cD)}{\in_2}
\eneq

The judgment $\GG\vd \theta\hastype\Phi$ formalizes that $\theta$ is a
valid well-typed substitution \wrt $\GG$.
% where $par(t)$ denotes the set of parameters occurring in $t$:
\beq
\ianc{}{\GG\vd\epsilon\hastype\cdot}{\epsilon\cdot}\qquad
%\ianc{}{\GG\vd\epsilon}{\epsilon}\qquad
\ibnc{\GG\vd t\hastype A}{\GG\vd\theta\hastype\Phi}
{\GG\vd\theta,t/x\hastype(\Phi,x\hastype A)} {\theta\Phi}
%\ibnc{par(t)\subseteq\GG}{\GG\vd\theta}{\GG\vd\theta,t/x}{\theta}
\eneq

Let us now analyze the rules in Figure \ref{fig:schemaG}.  The empty
run-time context is an instance of every schema. Moreover if $\GG'$
and $\cD'$ are completed blocks which occur in $\cS$, as denoted by
the block notation, then $(\GG,\block{\GG'});(\cD\And\block{\cD'})$ is
an instance of $ \cS$, provided that $\cD'$ is a valid clause.  Thus
we need to define the instance relation simultaneously to clause (and
in turn to goal) satisfaction.  The judgment $\dsat D$ is merely
auxiliary to the $\ga\sla G\inss$ one: here we mimic the construction
on the run-time schema until, in the base case, we check whether the
resulting context is an instance of the given schema.


\begin{figure}
  \[
\begin{array}{c}
\ibnc{X\in\{Q,\top,\perp\}\mbox{ or (dis)eq}}{\ga\inss}{\ga\sla
  X\inss}{\sla X}
%  \ianc{\ga\ins\cS}{\ga\sla Q\ins\cS}{\sla\atm}\qquad
%  \ianc{\ga\ins\cS}{\ga\sla\top\ins\cS}{\sla\top}\qquad
%  \ianc{\ga\ins\cS}{\ga\sla\perp\ins\cS}{\sla\perp}\vsk
% \ianc{\ga\ins\cS}{\ga\sla  (\vM \eqd \vN)\ins\cS}{{\sla\eqd}}\qquad
% \ianc{\ga\ins\cS}{\ga\sla  (\vM \neqd \vN)\ins\cS}{{\sla\neqd}}
\vsk
\ibnc{\ga\sla  G_1\ins\cS}{\ga\sla  G_{2}\ins\cS}{\ga\sla  G_{1}\And G_{2}\ins\cS}{{\sla}\And}
\vsk
\ibnc{\ga\sla  G_1\ins\cS}{\ga\sla  G_{2}\ins\cS}{\ga\sla  G_{1}\Or G_{2}\ins\cS}{{\sla}\Or}
\vsk
%\ianc{\ga\sla [u/x]G\ins\cS}{\ga\sla \exa G\ins\cS}{\sla\exists^u}
%\vsk
\ianc{(\GG,y\oftp A);\cD\sla [y/x]G\ins\cS}{\ga\sla  \PIXA
  G\ins\cS}{{\sla} \Pi^y}
\vsk
\ibnc{\dsat D}{\GG;(\cD\And D) \sla  G\ins\cS}{\ga\sla  D \Imp G\ins\cS}{{\sla} \Imp}
\vsk\vsk
%start |=D
\ianc{X\in\{Q,\top\perp\}}{\dsat X}{\dsat X}
% \ianc{}{\dsat Q}{\dsat\atm}\qquad
%  \ianc{}{\dsat\top}{\dsat\top}\qquad
%  \ianc{}{\dsat\perp}{\dsat\perp}
\vsk
\ibnc{\dsat  D_1}{\dsat  D_{2}}{\dsat  D_{1}\And D_{2}}{\dsat\And}
\vsk
\ibnc{\dsat  D_1}{\dsat  D_{2}}
{\dsat  D_{1}\tensor D_{2}}{\dsat\tensor}
\vsk
\ianc{\dsat [u/x] D}{\dsat \PIXA D}{\dsat\Pi^u}
\vsk
\ibnc{\dsat D}{\cdot;\top\sla  G\inss}{\dsat  G \Imp D}{\dsat \Imp}
\vsk\vsk
%start <
\ianc{}{\cdot;\top\ins \cS}{\ins_1}\qquad
\ianc{\GG\vd(\GG';\cD')\in\cS\quad \dsat\cD'\quad(\GG;\cD)\ins \cS}
{(\GG,\block{\GG'});(\cD\And\block{\cD'})\ins\cS}{\ins_2}
\end{array}
\]
  \caption{Judgments $\GG;\cD\sla G\ins \cS$, $\dsat D$ and $\ga\inss$}
  \label{fig:schemaG}
\end{figure}

\smallskip

The following Lemma ensures that when an assumption $D$ is pulled from a
legal run-time context, \ie which satisfies a given schema,  so does $D$.

\begin{Lemma}
\label{le:ins}
If $\ga\inss$ and $D\inn\cD$, then $\dsat D$.
\end{Lemma}
\begin{proof}
By induction on the structure of the derivation of $\pi::\ga\inss$.
\bit
\itc
$$\pi=\ianc{}{\cdot;\top\ins \cS}{\ins_1}$$
Then $D=\top$ and immediately $$\pi'=\ianc{}{\cdot;\top\dsat\top}{\dsat\top}$$
\itc
$$\pi=\ianc{\GG''\vd(\GG';\cD')\in
\cS\quad \dsat\cD'\quad(\GG'';\cD'')\ins \cS}{(\GG'',\block{\GG'});(\cD''\And\block{\cD'})\ins
\cS}{\ins_2}$$
\bit
\item[\subcase]
\btab
$D\equiv\cD'$\\
$\dsat \cD'$\bh
\etab
\item[\subcase]
\btab
$D\inn\cD''$\\
$\GG'';\cD''\inss$\bs
$\dsat D$\bi\\
\etab
\enit
\enit
\end{proof}

We can also show that schema satisfaction is closed under substitution:

\begin{Lemma}
\label{le:schematheta}
Let $\ga\inss$ and $\GG\vd \q\hastype\Phi$.
\ben
\item If $\dsat D$, then $\dsat [\q]D$.
\item If $\ga\sla G\inss$, then $\GG;[\q]\cD\sla [\q]G\inss$.
\item If $\ga\ins\cS$ then $\GG;[\q]\cD\inss$.  \enen
\end{Lemma}
\begin{proof}
  By a straightforward mutual induction on the structure of $\pi::\ 
  \dsat D$, $\gamma ::\ga\sla G\inss$ and $\sigma::\ga\ins\cS$.
\end{proof}


\subsection{Schema Extraction}
\label{ssec:schemaextract}

Roughly, we extract a context schema by collecting all negative
occurrences in a goal. In fact, those will be dynamically added to the
static program under evaluation. This is achieved by the judgment
$\ga\vd_{\!\Phi} G\yg\cS$. The latter is mutually recursive to the
judgment $ \vd_{\!\Phi}D\yd\cS$ which collects schemata for each
clause in the given program, as depicted in Figure \ref{fig:schema}.
When an atomic goal is reached, the current list of parameters and
assumptions is returned, with the correct existential binding inferred
from the context of global variables. With the notation $\Phi_{\cD}$ we mean
the restriction of context $\Phi$ to the free variables of $\cD$, \ie
$\{u\oftp A\mid u\in\dom(\Phi),u\in FV(\cD)\}$.  
%To avoid notational clutter, we will suppress mention of $\Phi$ when possible.
We make the convention to absorb schema alternatives which are
$\alpha$-variants. Moreover the empty 
%%% run-time 
context behaves as a left and right zero element for $\mbar$, \ie:
\beq (\ga\mbar\cdot;\top)=(\cdot;\top\mbar\ga)=\ga \eneq Finally
$\mbar$ is commutative.

\begin{figure}
\renewcommand{\vd}{\vdash_{\!\Phi}}
\[
\begin{array}{c}
  \ianc{X\in\{Q,\top,\perp\}\mbox{ or
  (dis)eq}}%{\Phi_{\cD}=FV(\cD)\cap\Phi)}
{\ga\vd 
  X\yg\GG;\some{\Phi_{\cD}} \cD}{\yg X}  \vsk 
\ibnc{ \GG;(\cD\And D)\vd G\yg \cS_1}{D\yd \cS_2}{ \ga \vd
  D\Imp G\yg \cS_1\mbar \cS_2}{ \yg\Imp}\vsk
\ianc{(\GG,y\oftp A);\cD\vd[y/x] G\yg  \cS}{ \ga\vd\PIXA G\yg \cS}{ \yg\Pi^y}\vsk 
%\ianc{\GG;\cD\vdash_{\!\Phi,u\oftp A} [u/x] G\yg \cS}{ \ga\vd\exa G\yg
%  \cS}{ \yg\exists^u}\vsk  
\ibnc{ \ga \vd G_1 \yg  \cS_1}{\ga\vd G_2\yg \cS_2} { \ga\vd G_{1}\And
  G_{2} \yg \cS_1\mbar \cS_2}{ \yg\And}\vsk 
\ibnc{ \ga \vd G_1 \yg \cS_1}{\ga\vd G_2\yg \cS_2} { \ga\vd
  G_{1}\Or G_{2} \yg \cS_1\mbar \cS_2}{ \yg\Or}\vsk \vsk

% \ianc{}{\top\yd \cdot;\top}{\yd \top} \qquad
 % \ianc{}{\perp\yd \cdot;\top}{\yd \perp} \vsk
\ianc{X\in\{Q,\top,\perp\} }{\vd X\yd \cdot;\top}{\yd X} \vsk
%  \ianc{\cdot;\top\vd G\yg \cS} {(G\Imp Q)\yd \cS}{ \yd\Imp} Q\If G syntax
  \ibnc{\cdot;\top\vd G\yg \cS_1}{\vd D\yd \cS_2} {\vd (G\Imp  D)\yd \cS_1\mbar \cS_2}{ \yd\Imp}\vsk
  \ianc{ \vdash_{\!\Phi,u\oftp A}[u/x]D\yd \cS}{\vd \PIXA D\yd \cS}{ \yd\Pi^u}\vsk 
\ibnc{ \vd D_1 \yd \cS_1}{\vd D_2\yd \cS_2} { \vd D_{1} \And D_{2} \yd \cS_1\mbar \cS_2}{ \yd\And}\vsk
 \ibnc{ \vd D_1 \yd \cS_1}{\vd D_2\yd \cS_2} { \vd D_{1} \tensor D_{2} \yd \cS_1\mbar
 \cS_2}{ \yd\tensor}
 \end{array}
\]
  \caption{Extracting  contexts schemata}
  \label{fig:schema}
\end{figure}



\begin{Example} If $\cP$ is the program in Example~\ref{ex:linear}, 
$\cP\yd x\oftp exp;linear(x)\mbar x\oftp
  exp;\top_{linx} $.
% \beq
% \cS_{linear} & = & \ecs\bnfalt\cS_{linear}\mbar x\oftp exp;linear(x)\bnfalt\cS_{linear}\mbar 
% x\oftp exp;\top_{linx} 
% \eneq
\end{Example}


\smallskip
We aim to show that if a schema context is extracted by a program, the
latter satisfies the former. First, we need to establish two
weakening lemmata \wrt schema alternatives:

% \begin{Lemma}
% \label{le:gagap}
% If $\ga\inss$ and $\gap\inss$, then $\ggdd\inss$.
% %$\GG,\block{\GG'};\cD\And\block{\cD'}\inss$.
% \end{Lemma}
% \begin{proof}
% By induction on the structure of the first derivation. 
% \end{proof}

% \begin{Lemma} [$\ins$-Weakening]
% \label{le:dsatweak}
% Let $\gap\inss$.
% \ben
% \item If $\dsat D$ and then $(\GG,\GG');(\cD\And\cD')\dsat D$.
% \item If $\ga\sla G\inss$ and  then $(\GG,\GG');(\cD\And\cD')\sla G\inss$.
% \enen
% \end{Lemma}
% \begin{proof}
% By mutual induction on the structure of the given derivations, using
% Lemma \ref{le:gagap} in the $\sla X$ case.
% \end{proof}


\begin{Lemma}
\label{le:w1}
If $\GG\vd\GG';\cD'\in\cS$ then $\gapp\in S'\mbar S$.
\end{Lemma}
\begin{proof}
By a straightforward induction on the structure of $\pi::\ga\in\cS$.
\end{proof}

Note also that
%, following our convention concerning the commutativity of $\mbar$, 
$\gapp\in S'\mbar S$ iff $\gapp\in S\mbar S'$.


\begin{Lemma}[Schema Weakening]
\label{le:w}
Let $\ga\inss$. Then
\ben
\item If $\dsat D$, then $\dsats D$.
\item If $\ga\sla G\inss$, then $\ga\sla G\insss$.
\item If $\ga\ins\cS$ then $\ga\ins \cS\mbar \cS'$.
\enen
\end{Lemma}
\begin{proof}
By mutual induction on the structure of $\pi::\  \dsat D$, $\gamma
::\ga\sla G\inss$ and  $\sigma::\ga\ins\cS$. We show the crucial cases:
\bit
\itc $$\pi=\ianc{X\in\{Q,\top,\perp\}}{\dsat X}{\dsat X}$$
Trivially $$\pi'=\ianc{X\in\ \{Q,\top,\perp\}}{\dsats Q}{\dsat X}$$

\itc$$\pi=\ibnc{\dsat D}{\emp\sla G\inss}{\dsat G\Imp  D}{\dsat\Imp}$$
\btab
%$\ga\inss$\bh
$\dsat D$\bs
$\dsats D$\bi $1$\\
$\emp\sla G\inss$\bs
$\emp\sla G\insss$\bi $2$\\
$\dsats G\Imp D$\br $\dsat\Imp$
\etab
\itc $$\gamma=\ibnc{X\in\{Q,\top,\perp\}\mbox{ or (dis)eq}}{\ga\inss}{\ga\sla X\inss}{\sla X}$$
\btab
$\ga\inss$\bs
$\ga\insss$\bi $3$\\
$\ga\sla X\insss$\br $\sla X$
\etab
\itc$$\gamma=\ibnc{\dsat D}{\GG;\cD\And D\sla G\inss}{\ga\sla D\Imp
  G\inss}{\sla\Imp}$$
\btab
$\dsat D$\bs
$\dsats D$\bi $1$\\
$\GG;\cD\And D\sla G\inss$\bs
$\GG;(\cD\And D)\sla G\insss$\bi $2$\\
$\ga\sla D\Imp G\insss$\br $\sla\Imp$
\etab
\itc $$\sigma=\ianc{}{\cdot;\top\ins \cS}{\ins_1}$$
Then immediately:
 $$\sigma'=\ianc{}{\cdot;\top\ins \cS\mbar\cS'}{\ins_1}$$
\itc$$\sigma=\ianc{\GG\vd(\GG';\cD')\in
\cS\quad \dsat\cD'\quad(\GG;\cD)\ins \cS}{(\GG,\block{\GG'});(\cD\And\block{\cD'})\ins
\cS}{\ins_2}$$
\btab
$\ga\inss$\bs
$\ga\insss$\bi $3$\\
$\gapp\in\cS$\bs
$\gapp\in\cS\mbar\cS'$\` By Lemma \ref{le:w1}\\
$\dsat\cD'$\bs
$\dsats D$\bi $1$\\
$(\GG,\block{\GG'});(\cD\And\block{\cD'})\insss$\br $\ins_2$
\etab
\enit
\end{proof}

\renewcommand{\dsats}{\models_{\!\cS_1\mbar\cS_2}}
\renewcommand{\insss}{\ins\cS_1\mbar\cS_2}

% \begin{Lemma}
% \label{le:auxsplit}
% If $\ga\in \cS_1\mbar\cS_2$, then $\ga\in\cS_1$ or $\ga\in\cS_2$.
% \end{Lemma}
% \begin{proof}
% By induction on the structure of $\ga\in \cS_1\mbar\cS_2$.
% \end{proof}

% \begin{Lemma}
% \label{le:splitrun}
% If $\ga\insss$, then $\GG_1;\cD_1\ins \cS_1$ and $\GG_2;\cD_2\ins
% \cS_2$, for $\GG=\GG_1,\GG_2$, $\cD=\cD_1\And\cD_2$.
% \end{Lemma}
% \begin{proof}
% By induction on the structure of $\ga\insss$, using Lemma \ref{le:auxsplit}.
% \end{proof}

%\begin{Lemma}
%\label{le:weakD}
%If $\GG_1;\cD_1\sla G\inss$ and $\GG_2;\cD_2\dsat D$ and
%$\GG_2;\cD_2\in\cS$, then $\GG_1,\GG_2;\cD_1\And\cD_2\sla G\inss$.
%\end{Lemma}
%\begin{proof}
%By induction on the structure of $\GG_1;\cD_1\sla G\inss$.
%\end{proof}


\smallskip 

We are now ready to show that if a program yields a schema, then every
instance of a clause used at run-rime will comply with the schema. We
need to generalize this statement to take into account instances of
goals as well; in the latter case, we need to synchronize the schema
accumulator in $\gap\vd G\yg \cS$ with the possibly incomplete
run-time context $\ga$. 
%It is also convenient to strengthen the
%induction hypothesis to consider arbitrary schema alternatives. 
A fortiori the result holds for compile-time contexts as well, by
taking $\ga$ as $\emp$.
%In the following we abridge $\cdot;\top\dsat D$ in $\dsat D$.

\newcommand{\gaex}{(\GG,\GG');(\cD\And \q \cD')}
\begin{Theorem}[Extracted Schema Satisfaction]
\label{thm:yieldsat}
\renewcommand{\vd}{\vdash_{\!\Phi}}
Let $\GG\vdash \q\hastype\Phi$.
% that is  dom$(\q)=(FV(\cD')\cup FV(D)\cup FV(G))\sla\dom(\GG))\sla$
\ben
\item If $\vd D\yd \cS$,  then $\dsat[ \q] D$.
\item If $\gap\vd G\yg \cS$, $\dsat\cD'$ 
 and  $\ga\ins\cS$,  then $(\GG,\GG');(\cD\And [\q] \cD')\sla [ \q] G\inss$.
\enen
\end{Theorem}
\begin{proof}
\renewcommand{\q}{[\theta]}
\renewcommand{\vd}{\vdash_{\!\Phi}}
By mutual induction on the structure of $\pi:: D\yd \cS$ and $\gamma::\gap \vd
G\yg \cS$.
\bit
\itc $$\pi=\ianc{X\in\{Q,\top,\perp\}}  {\vd X\yd \cdot;\top}{\yd X}$$
\btab
$\models_{\! \cdot;\top} X$\br $\dsat X$\\
% $\ga\inss$\bh
%$\dsat X$\bl{le:dsatweak}
\etab \itc $$\pi = \ibnc{ \vd D_1 \yd \cS_1}{\vd D_2\yd \cS_2} { \vd
  D_{1} \And D_{2} \yd \cS_1\mbar \cS_2}{ \yd\And}$$
\btab $ \vd D_1
\yd \cS_1$\bs $ \vd D_2 \yd \cS_2$\bs
$\dsato \q D_1$\bi $1$\\
$\dsatt\q D_2$\bi $1$\\
$\dsats\q D_1$\bl{le:w} $\dsats\q D_2$\bl{le:w}
$\dsats\q D_1\And \q D_2$\br $\dsat\And$\\
$\dsats\q (D_1\And D_2)$\bsu \etab \itc $\pi$ ends in $\yd\tensor$:
analogously to the above.  \itc $\pi$ ends in $\yd\Pi^y$: by an
immediate appeal to IH $1$.  \itc $$\pi= \ibnc{\cdot;\top\vd G\yg
  \cS_1}{\vd D\yd \cS_2} {\vd(G\Imp D)\yd \cS_1\mbar \cS_2}{ \yd\Imp}$$
\btab $\vd D\yd \cS_2$\bs
$\models_{\!\cS_2} \q D$\bi $1$\\
$\dsats\q D$\bl{le:w} $\cdot;\top\vd G\yg \cS_1$\bs
$\cdot;\top\ins\cS_1$\br $\ins_1$\\
$\cdot;\top\sla \q G\ins\cS_1$\bi $2$\\
$\cdot;\top\sla \q G\ins\cS_1\mbar\cS_2$\bl{le:w} $\dsats \q G\Imp\q
D$\br $\dsat\Imp$ \etab 
\itc $$\gamma=
\ianc{X\in\{Q,\top,\perp\}\mbox{ or
    (dis)eq}}%{\Phi_{\cD'}=FV(\cD')\cap\Phi } 
{\gap\vd
  X\yg\GG';\some{\Phi_{\cD'}} \cD'}{\yg X} $$
\btab
$\GG';\q\cD'\equiv_{\alpha}\GG';\q\cD'$\bh
$\GG\vdash\GG';\q\cD'\in\GG';\some{\Phi_{\cD'}} \cD'$\br $\in_1$\\
$\ga\ins\GG';\some{\Phi_{\cD'}}\cD'$\bh
$\models_{\GG';(\some{\Phi_{\cD'}}\cD')} \cD'$\bh
$\models_{\GG';(\some{\Phi_{\cD'}}\cD')} \q\cD'$\` By Lemma \ref{le:schematheta}\\
$(\GG,\block{\GG'});(\cD\And \block{\q\cD'})\ins\GG';\some{\Phi_{\cD'}} \cD'$\br $\ins_2$\\
$(\GG,\GG');(\cD\And \q\cD')\sla \q X\ins\GG';\some{\Phi_{\cD'}}
\cD'$\br $\sla X$ 
\etab
\itc %% PI
$$\gamma = \ianc{(\GG',y\oftp A);\cD'\vd[y/x] G\yg  \cS}
{ \gap\vd\PIXA G\yg \cS}{ \yg\Pi^y}$$
\btab
$(\GG',y\oftp A);\cD'\vd[y/x] G\yg\cS$\bs
$(\GG,\GG',y\oftp A);(\cD\And\q\cD')\sla\q\cdot [y/x] G\inss$\bi $2$\\
$(\GG,\GG');(\cD\And\q\cD')\sla\q\PIXA G\inss$\br $\sla\Pi^y$\\
\etab
\itc % D Imp G
$$\gamma=\ibnc{ \GG';(\cD'\And D)\vd G\yg \cS_1}{\vd D\yd \cS_2}{  \gap\vd
  D\Imp G\yg \cS_1\mbar \cS_2}{ \yg\Imp}$$
\btab
%$\GG_1;\cD_1\ins\cS_1$\bl{le:splitrun}
%$\GG_2;\cD_2\ins\cS_2$\bl{le:splitrun}
$\vd D\yd\cS_2$\bs
$\dsatt \q D$\bi $1$\\
$\dsats \q D$\bl{le:w}
$\ga\ins\cS_1$\bh
$\GG';(\cD'\And D)\vd G\yg \cS_1$\bs
$(\GG,\GG');(\cD\And\q\cD'\And\q D)\sla\q G\ins\cS_1$\bi $2$\\
$(\GG,\GG');(\cD\And\q\cD'\And\q D)\sla\q G\ins\cS_1\mbar\cS_2$\bl{le:w}
$\gaex\sla \q D\Imp \q G\insss$\br $\sla\Imp$\\
\etab
%%% AND
\itc $$\gamma=\ibnc{ \gap \vd G_1 \yg  \cS_1}{\gap\vd G_2\yg \cS_2} { \gap\vd G_{1}\And
  G_{2} \yg \cS_1\mbar \cS_2}{ \yg\And}$$
\btab
$\gap \vd G_1 \yg  \cS_1$\bs
$\ga\ins\cS_1$\bh
%$\GG_1;\cD_1\ins\cS_1$ and $\GG_2;\cD_2\ins\cS_2$\bl{le:splitrun}
$\gaex\sla \q G_1\ins\cS_1$\bi $2$\\
$\gaex\sla \q G_1\ins\cS_1\mbar\cS_2$\bl{le:w}
$\gap \vd G_2 \yg  \cS_2$\bs
$\ga\ins\cS_2$\bh
$\gaex\sla \q G_2\ins\cS_2$\bi $2$\\
$\gaex\sla \q G_2\ins\cS_1\mbar\cS_2$\bl{le:w}
%$\GG_1;\cD_1\ins\cS_1\mbar\cS_2$ and $\GG_2;\cD_2\ins S_1\mbar\cS_2$\bl{le:w2}
%$\GG_1,\GG_2;\cD_1\And \cD_2\sla \q
%G_1\ins\cS_1\mbar\cS_2$\bl{le:dsatweak}
%$\GG_1,\GG_2;\cD_1\And \cD_2\sla \q G_2\ins\cS_1\mbar \cS_2$\bl{le:dsatweak}
$\gaex\sla\q G_1\And\q G_2\insss$\br $\sla\And$
\etab
\itc $\gamma$ ends in $\yg\Or$: similarly to the above.
%\itc $\gamma$ ends in $\yg\exists^y$: by an immediate appeal
to IH $2$.
\enit
\end{proof}

\subsection{Context Preservation}
\label{ssec:contextpreserv}

We aim to prove that execution preserves contexts, provided that the
program itself and the input goal satisfy a schema; that
is,  that every
subgoal which arises in any given successful or failed (immediate and
non-immediate sub-derivation) satisfies the same context schema. 

%As expected, first 
% we need to establish  weakening  for run-time schema
% satisfaction: this is possible for any valid block $\gap$. 
%For the sake of brevity we omit the block notation.

% \newcommand{\ggdd}{(\GG,\block{\GG'});(\cD\And\block{\cD'})}

% \begin{Lemma}[Run-time Context Weakening]
% \label{le:indsat}
% Let $\gap\in\cS$ and $\ga\inss$. Then
% \ben
% \item If $\dsat D$, then $\ggdd\dsat D$.
% \item If $\ga\sla G\inss$, then $\ggdd\sla G\inss$.
% \enen
% \end{Lemma}
% \begin{proof}
% By mutual induction on the structure of $\pi::\dsat D$ and
% $\gamma::\ga\sla G\inss$. We show some  crucial cases:
% \bit
% \itc $$\pi=\ianc{X\in\{Q,\top\perp\}}{\dsat Q}{\dsat X}$$
% Trivially:
%  $$\pi'=\ianc{X\in\{Q,\top\perp\}}{\ggdd\dsat Q}{\dsat X}$$

% \itc$$\pi=\ibnc{\dsat D}{\ga\sla G\inss}{\dsat G\Imp  D}{\dsat\Imp}$$
% \btab
% %$\gap\in\cS$\bh
% %$\ga\inss$\bh
% $\dsat D$\bs
% $\ggdd\dsat D$\bi $1$\\
% $\ga\sla G\inss$\bs
% $\ggdd\sla G\inss$\bi $2$\\
% $\ggdd\dsat G\Imp D$\br $\dsat\Imp$
% \etab
% \itc $$\gamma=\ibnc{X\in\{Q,\top,\perp\}\mbox{ or (dis)eq}}{\ga\inss}{\ga\sla X\inss}{\sla\atm}$$
% \btab
% $\ga\inss$\bs
% $\gap\in\cS$\bh
% $\ggdd\inss$\br $<_2$\\
% $\ggdd\sla X\inss$\br $\sla X$
% \etab
% \itc$$\gamma=\ibnc{\dsat D}{\GG;\cD\And D\sla G\inss}{\ga\sla D\Imp
%   G\inss}{\sla\Imp}$$
% \btab
% %$\gap\in\cS$\bh
% %$\ga\inss$\bh
% $\dsat D$\bs
% $\ggdd\dsat D$\bi $1$\\
% $\GG;(\cD\And D)\sla G\inss$\bs
% $(\GG;\block{\GG'});(\cD\And\block{\cD'}\And D)\sla G\inss$\bi $2$\\
% $\ggdd\sla G\Imp D\inss$\br $\sla\Imp$
% \etab
% \enit
% \end{proof}


% % \begin{Lemma}
% \label{le:gagap}
% If $\ga\inss$ and $\gap\inss$, then $\ggdd\inss$.
% %$\GG,\block{\GG'};\cD\And\block{\cD'}\inss$.
% \end{Lemma}
% \begin{proof}
% By induction on the structure of the first derivation. 
% \end{proof}

% \begin{Lemma} [$\ins$-Weakening]
% \label{le:dsatweak}
% Let $\gap\inss$.
% \ben
% \item If $\dsat D$ and then $(\GG,\GG');(\cD\And\cD')\dsat D$.
% \item If $\ga\sla G\inss$ and  then $(\GG,\GG');(\cD\And\cD')\sla G\inss$.
% \enen
% \end{Lemma}
% \begin{proof}
% By mutual induction on the structure of the given derivations, using
% Lemma \ref{le:gagap} in the base case.
% \end{proof}

% The following Lemma ensures that when an assumption $D$ is pulled from a
% legal run-time context, \ie which satisfies a given schema,  so does $D$.

% \begin{Lemma}
% \label{le:ins}
% If $\ga\inss$ and $D\in\cD$, then $\dsat D$.
% \end{Lemma}
% \begin{proof}
% By induction on the structure of the derivation of $\pi::\ga\inss$.
% \bit
% \itc
% $$\pi=\ianc{}{\cdot;\top\ins \cS}{\ins_1}$$
% Then $D=\top$ and immediately $$\pi'=\ianc{}{\cdot;\top\dsat\top}{\dsat\top}$$
% \itc
% $$\pi=\ianc{(\GG';\cD')\in
% \cS\quad \dsat\cD'\quad(\GG'';\cD'')\ins \cS}{(\GG'',\block{\GG'});(\cD''\And\block{\cD'})\ins
% \cS}{\ins_2}$$
% \bit
% \item[Subcase]
% \btab
% $D\equiv\cD'$\\
% $\dsat \cD'$\bh
% \etab
% \item[Subcase]
% \btab
% $D\in\cD''$\\
% $\GG'';\cD''\inss$\bs
% $\dsat D$\bi\\
% \etab
% \enit
% \enit
% \end{proof}


%Finally, the proof of context preservation; 
Note that we have already
established schema extraction (Theorem \ref{thm:yieldsat}), that is we
assume that $\cP\yd \cS$. We write $\pi'< \pi$ to say that $\pi'$ is a
strict subproof of $\pi$, \ie $\pi'\leq\pi$ if $\pi'< \pi$ or $\pi'=\pi$.

\begin{Theorem}[Context Preservation \wrt Provability]
\label{thm:poscntpres}
Let $\dsat\cP$ and $D\inn (\cP\And\cD$). For any
 $\ga\inss$,  if ($\pi::\ga\sp G$ and $\ga\sla G\ins\cS$) or 
($\iota::\ga\sp D\imm Q$ and $\dsat D$), then: 
\ben
\item for every subproof $\pi'::\gap\sp G'$ and $\gap\sla G'\ins\cS$.
\item 
for every subproof  $\iota'::\gap\sp D'\imm Q$ and  $\dsat D'$.
\enen
\end{Theorem}
\begin{proof}
By\fixed mutual induction on the structure of $\pi::\ga\sp G$ and $\iota::\ga\sp D\imm Q$. 
\bit %main bit
\itc $\pi=\ga\sp \top$: trivial.
\itc $$\pi=\ianc{\arv{\pi_1}{ \GG;\cD\And D\sp G}}{\ga\sp D\Imp
  G}{\vd\Imp}$$
\bit
\item[\subcase] $\pi'=\pi$: trivial.
\item[\subcase] $\pi' <\pi$: then $\pi' \leq\pi_1$.
\btab
$\pi_1::\GG;\cD\And D\sp G$\bs
$\ga\sla D\Imp G\ins \cS$\bh
$\GG;\cD\And D\sla G\ins \cS$\bv
 $\iota'::\gap\sp D'\imm Q$ and   $\dsat D'$ and \\
 $\pi_1'::\GG';(\cD'\And D')\sp G'$ and  $\GG';(\cD'\And D')\sla G'\ins\cS$\bi  \\
 $\pi'::\gap\sp D'\Imp G'$ and  $\gap\sla D'\Imp G'\ins\cS$\br
\etab
\enit
\itc $$\pi\ianc{\arv{\pi_1}{(\GG,y\oftp A);\cD\sp [y/x]G}}{\ga\sp\PIXA G}{\vd\Pi^y}$$
\bit
\item[\subcase] $\pi'=\pi$: trivial.
\item[\subcase] $\pi' <\pi$: then $\pi' \leq\pi_1$.
\btab
$\pi_1::(\GG,y\oftp A);\cD\sp [y/x]G$\bs
$\ga\sla \PIXA G\ins \cS$\bh
$(\GG,y\oftp A);\cD\sla [y/x]G\inss$\bv
 $\iota'::\gap\sp D'\imm Q$ and   $\dsat D'$ and\\
 $\pi_1'::(\GG',y\oftp A);\cD'\sp[y/x] G'$ and  $(\GG',y\oftp
A);\cD'\sla[y/x] G'\ins\cS$ \bi \\
 $\pi'::\gap\sp \PIXA G'$ and  $\gap\sla \PIXA G'\ins\cS$\br
\etab
\enit
\itc $\pi$ ends in $\vd\And,\vd\Or_1,\vd\Or_2$: similarly.
\itc $$\pi=\ianc{\arv{\iota}{\ga\sp D\imm Q}}{\ga\sp Q}{\vd\atm}$$
\bit
\item[\subcase] $\pi'=\pi$: trivial.
\item[\subcase] $\pi' <\pi$: then $\pi' \leq\iota$.
\bit
\item[\subcase]
\btab
$\iota_1::\ga\sp D\imm Q$, for $D\inn \cP$\bs
%$\ga\sla Q\inss$\ba
%$\ga\inss$\bv
$\dsat D$\bh
 $\pi'::\gap\sp G'$ and  $\gap\sla G'\ins\cS$ and\\
 $\iota_1'::\gap\sp D'\imm Q$ and   $\dsat D'$ \bi\\
$\gap\sp Q'$  and $\gap\sla Q'\ins\cS$\br
\etab
\item[\subcase]
\btab
$\iota_1::\ga\sp D\imm Q$, for $D\inn \cD$\bs
%$\ga\sla Q\inss$\bh
%$\ga\inss$\bv
$\dsat D$\` By Lemma \ref{le:ins}\\
 $\pi'::\gap\sp G'$ and  $\gap\sla G'\ins\cS$ and \\
 $\iota_1'::\gap\sp D'\imm Q$ and   $\dsat D'$\bi\\
$\gap\sp Q'$  and $\gap\sla Q'\ins\cS$\br
\etab
\enit
\enit
\itc $\iota::\ga\sp\perp\imm Q$: trivial.
\itc $$\iota=\ianc{\arv{\iota_1}{\ga\sp D_1\imm Q}}{\ga\sp D_1\And
 D_2\imm Q}{\imm\And_1}$$ 
\bit
\item[\subcase] $\iota'=\iota$: trivial.
\item[\subcase] $ \iota'<\iota$: then $\iota' \leq\iota_1$:
\btab
$\dsat D_1\And D_2$\bh
$\dsat D_1$ and $\dsat D_2$\` By inversion\\
$\iota_1::\ga\sp D_1\imm Q$\bs
 $\pi'::\gap\sp G'$ and  $\gap\sla G'\ins\cS$ and \\
 $\iota_1'::\gap\sp D_1'\imm Q$ and   $\dsat D_1'$ \bi\\
 $\iota'::\gap\sp D_1'\And D_2'\imm Q$ and   $\dsat D_1'\And D_2'$ \br
\etab
\enit %ends subcase
\itc $\iota$ ends in $\imm\And_2$. Symmetrical.
\itc 
$$\iota=\ianc{\arv{\iota_1}{\ga\sp [t/x] D\imm Q}}{\ga\sp\PIXA D\imm
  Q}{\imm\Pi}$$ 
\bit
\item[\subcase] $\iota'=\iota$: trivial.
\item[\subcase] $\iota'<\iota$: then $\iota' \leq\iota_1$.
\btab
$\iota_1::\ga\sp [t/x] D\imm Q$\bs
$\dsat \PIXA D$\bh
$\dsat [u/x] D$\bv
$\dsat [t/u,u/x] D$\` By substitution\\
 $\pi'::\gap\sp G'$ and  $\gap\sla G'\ins\cS$ and \\
 $\iota_1'::\gap\sp[t/x] D'\imm Q$ and   $\dsat [t/x]D'$\bi\\
 $\iota'::\gap\sp \PIXA D'\imm Q$ and   $\dsat \PIXA D'$\br
\etab
\enit
\itc
$$\iota=\ibnc{\arv{\iota_1}{\ga\sp D\imm Q}}{\arv{\pi_1}{\ga\sp G}}{\ga\sp G\Imp
  D\imm Q}{\imm\Imp} $$
\bit

\item[\subcase] $\iota'=\iota$: trivial.
\item[\subcase] $\iota'<\iota$: 
\bit
\item[\subcase] $\iota' \leq\iota_1$
\btab
$\iota_1::\ga\sp D\imm Q$ and $\pi_1::\ga\sp G$\bs
$\dsat G\Imp D$\bh
$\ga\sla G\inss$ and $\dsat D$\bv
 $\pi'::\gap\sp G'$ and  $\gap\sla G'\ins\cS$ and \\
 $\iota_1'::\gap\sp D'\imm Q$ and   $\dsat D'$\bi\\
 $\iota'::\gap\sp G'\Imp D'\imm Q$ and   $\dsat G'\Imp D'$\br
\etab
\item[\subcase] $\iota'  \leq\pi_1$: analogously.
\enit
\enit
\itc $\iota$ ends in $\imm\tensor, \imm\Pi$: similarly.
\enit
\end{proof}

We establish an analogous result \wrt denial. % We recall that the
% statement must be generalized to account for the meta-level
% extensional quantification brought in by the $\notimm\Pi,\nvd\exists$
% rules; at the same time those substitution terms should be disjoint
% with the global parameters which are instantiated while satisfying the
% schema: formally, for our implicit pool of global parameters $\Phi$,
% we require $\dom(\q)\cap\Phi=\eset$.

%Notice that the definition of allowed program implies that $\cD$ is
%closed, thus unaffected by substitutions.

\newcommand{\qp}{}
%\newcommand{\qp}{[ \theta']} 
\renewcommand{\ga}{ \Gamma;\cD }
\renewcommand{\gap}{ \Gamma';\cD' }
% \renewcommand{\ga}{ \Gamma;[\theta]\cD }
% \renewcommand{\gap}{ \Gamma';[\theta']\cD' }
\begin{Theorem}[Context Preservation \wrt Denial]
\label{thm:negcntpres}
%Let $\q$ be a well-typed substitution such that $\GG\vd\q$.  
Let $\dsat\cP$ and $D\inn (\cP\And\cD$):%and $\GG\vd\q hastype\Phi$:
 \renewcommand{\q}{} for any
$\ga\inss$, if ( $\pi::\ga\fp \q G$ and $\ga\sla \q G\ins\cS$ ) or (
$\iota::\ga\fp \q D\imm\q Q$ and $\dsat\q D$), then:
% for all $\theta'$:
\ben
\item for every subproof $\pi'::\gap\fp \qp G'$ and $\gap\sla \qp
  G'\ins\cS$.
\item for every subproof $\iota'::\gap\fp\qp D'\imm\qp Q$ and $\dsat
  \qp D'$.  
\enen
\end{Theorem}

\begin{proof}
\renewcommand{\q}{}
\renewcommand{\foq}{}
% \renewcommand{\q}{[ \theta]}
% \renewcommand{\foq}{\mbox{\textrm{for all }$\theta$  }}
 %\renewcommand{\foq}{\mbox{\textrm{for all } $n$  }}
By mutual induction on the structure of $\pi::\ga\fp\q G$ and
$\iota::\ga\fp\q D\imm\q Q$, similarly to the case of provability.
 We show only some cases:
\bit
% \itc
% %$$\pi=\ibnc{\mbox{\rm for all $n$ }\GG\vd n\hastype A}{\ga\fp[n/x] G}
% {\foq\ga\fp\q\exa G}{\nvd\exists}$$
% \btab
% for all $n$ $ \ga\fp[n/x] G$\bs
% $\foq\ga\sla\q\exa G\inss$\bh
% $\foq\ga\sla[u/x]  G\inss$\bv
% for all $ n\  \ga\sla[n/u,u/x]  G$\` By substitution\\
%  $\iota'::\gap\fp\qp  D'\imm\qp  Q$ and   $\dsat \qp D'$
% and \\
%  $\pi'::\gap\fp [\theta',n/x]G'$ and   $\gap\sla [\theta',n/x]  G'\ins\cS$ \bi
% \\
%  $\pi''::\gap\fp \qp \exa G'$ and   $\gap\sla \qp  \exa G'\ins\cS$ \br
% \etab
\itc
$$\pi= \ianc{\arv{\pi_1}{\foq\GG;(\q\cD\And \q D )\fp \q G}}{\ga\fp \q D \Imp\q
  G}{{\nprv} \Imp}$$
\bit
\item[\subcase] $\pi'=\pi$: trivial.
\item[\subcase] $ \pi'<\pi$: then $\pi' \leq\pi_1$:
\btab
$\foq\GG;(\q\cD\And \q D) \fp\q G$\bs
$\foq\ga\sla\q D\Imp\q G\ins \cS$\bh
$\foq\GG;\q\cD\And\q D\sla\q G\ins \cS$\bv
 $\iota'::\gap\fp\qp  D'\imm\qp  Q$ and   $\dsat \qp D'$ and\\
 $\pi'::\GG;(\qp\cD'\And \qp D')\fp \qp G'$ and   $\GG;(\qp\cD'\And \qp D')\sla \qp  G'\ins\cS$ \bi \\
 $\pi''::\gap\fp \qp (D'\Imp G')$ and   $\gap\sla \qp (D'\Imp
G')\ins\cS$ \br 
\etab
\enit
\itc
$$\iota=\ianc{\arv{\iota_1}{\foq\ga\fp\q G}}{\foq\ga\fp \q D\If\q G \nimm \q
  Q}{\notimm{\Imp_1}}$$
\bit
\item[\subcase] $\iota'=\iota$: trivial.
\item[\subcase] $ \iota'<\iota$: then $\iota' \leq\iota_1$:
\btab
$\foq\iota_1::\ga\fp\q G$\bs
$\foq\dsat\q G\Imp \q D$\bh
$\foq\ga\sla\q G\inss$ and $\dsat\q D$\bv
 $\pi'::\gap\fp G'$ and   $\gap\sla G'\ins\cS$ and \\
 $\iota'::\gap\fp \qp D'\imm\qp Q$ and     $\dsat \qp D'$\bi\\
 $\iota''::\gap\fp\qp  (D'\If G')\imm\qp  Q$ and    $\dsat
\qp (D'\If G')$\br
\etab
\enit
\itc 
$$\iota=\ianc{\arv{\iota_1}{\foq\ga\fp\q D\imm \q Q}} {\foq\ga\fp  \q D
  \If \q G \nimm \q Q}{\notimm{\Imp_2}}$$
\bit
\item[\subcase] $\iota'=\iota$: trivial.
\item[\subcase] $ \iota'<\iota$: then $\iota' \leq\iota_1$:
\btab
$\iota_1::\foq\ga\fp\q D\imm\q Q$ \bs
$\foq\dsat\q G\Imp\q D$\bh
$\foq\ga\sla\q G\inss$ and $\dsat\q D$\bv
 $\pi'::\gap\fp \qp G'$ and   $\gap\sla \qp  G'\ins\cS$ and \\
 $\iota'::\gap\fp\qp  D'\imm\qp  Q$ and    $\dsat \qp D'$\bi\\
 $\iota''::\gap\fp\qp  (D'\If G')\imm\qp  Q$ and    $\dsat
\qp (D'\If G')$\br
\etab
\enit
\itc 
$$\iota=\ianc{\arv{\iota_1}{\mbox{for all $n$ }\ga\fp [n/x] D\imm Q}}{\ga\fp\PIXA D\imm
  Q}{\imm\Pi}$$ 
\bit
\item[\subcase] $\iota'=\iota$: trivial.
\item[\subcase] $\iota'<\iota$: then $\iota' \leq\iota_1$.
\btab
$\dsat \PIXA D$\bh
$\dsat [u/x] D$\bv
For all  $\iota_1::\ga\fp [n/x] D\imm Q$\bs
For all $\dsat [n/u,u/x] D$\` By substitution\\
 $\pi'::\gap\fp G'$ and  $\gap\sla G'\ins\cS$ and \\
For all  $\iota_1'::\gap\fp[n/x] D'\imm Q$ and   $\dsat [n/x]D'$\bi\\
 $\iota'::\gap\fp \PIXA D'\imm Q$ and   $\dsat \PIXA D'$\br
\etab
\enit
\enit 
\end{proof}


% RESET \ga to remove \q
\renewcommand{\ga}{ \Gamma;\cD }
\renewcommand{\gap}{ \Gamma';\cD' }

\renewcommand{\SP}{{\cal S}^+}
\renewcommand{\SM}{{\cal S}^-}
\renewcommand{\IP}{{\cal I}^+}
\renewcommand{\IM}{{\cal I}^-}
%\newcommand{\PP}{\cP^+}
%\newcommand{\PM}{\cP^-}



