\section{Context Schemata}
\label{sec:runtime}
\renewcommand{\bar}{\|}

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 forthcoming dissertation \cite{}.}.  We restrict to second-order
programs, specifically 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 form 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 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}; 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 $\Phi=FV(\cD)$. As usual,
we implicitly annotate those variables with their types.  This is
achieved by the following reification of schemata. Do not confuse
`$\bar$', 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\bar(\GG;\some{\Phi} \cD)
\end{array}\]

We will also need to disambiguate blocks in run-time contexts;
overlapping may indeed happen when the alternatives in a context
schema are not disjoint. To achieve 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{ \_ \ 
  }$.  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 
\ianc{\block{\GG};\block{\cD}\sp \defp(Q,\cP\And\cD) \imm Q}
{\ga\sp Q}{\vd\atm}
\vsk 
\ianc{\block{\GG};\block{\cD}\fp  \defp(Q,\cP\And\cD) \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

We are now ready to define when a run-time context is an
\emph{instance} of a schema. 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 restrain
from giving rules for substitutions; we simply mention that the
codomain is $\Phi$, \ie the global parameters introduced by the
$\dsat\Pi$ and $\sla\exists$ rules, while the domain is $\GG$.
\beq
\ianc{(\GG';\cD')\equiv_{\alpha}(\GG;\q\cD)}{(\GG';\cD')\in \cS\bar
(\GG;\some{\Phi} \cD)}{\in_1} \qquad 
\ianc{(\GG';\cD')\in\cS}{(\GG';\cD')\in \cS\bar(\GG;\cD)}{\in_2}
% \vsk KEEP!! Well typed substitutions
%
% \ianc{}{\GG\vd\epsilon\hastype\cdot}{\epsilon\cdot}\qquad
% \ibnc{\GG\vd t\hastype A}{\GG\vd\q\hastype\Phi}{\GG\vd[t/Z]\cdot\q\hastype(\Phi,Z\hastype
%   A)}
% {\q\Phi}
\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}[htbp]
  \[
\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';\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}


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

Roughly, we extract a context schema by collecting all negative occurrences in
a goal: this is achieved by the judgment $\ga\vd G\yg\cS$. The latter
is mutually recursive to the judgment $ 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
parameter and assumption is returned, with the correct existential binding.  We
make the convention to absorb schema alternatives which are
$\alpha$-variants. Moreover the empty run-time context behave as a
left and right zero element for $\bar$, \ie
\beq
(\ga\bar\cdot;\top)=(\cdot;\top\bar)\ga=\ga 
\eneq
Finally $\bar$ is commutative.

\begin{figure}[htbp]

\[
\begin{array}{c}
  \ibnc{X\in\{Q,\top,\perp\}\mbox{ or (dis)eq}}{FV(\cD)=\Phi}{\ga\vd
  X\yg\GG;\some{\Phi} \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\bar \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\vd[u/x] G\yg \cS}{ \ga\vd\exa G\yg \cS}{ \yg\exists^y}\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\bar \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\bar \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\} }{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}{D\yd \cS_2} {(G\Imp  D)\yd \cS_1\bar \cS_2}{ \yd\Imp}\vsk
  \ianc{ [u/x]D\yd \cS}{ \PIXA D\yd \cS}{ \yd\Pi^y}\vsk 
\ibnc{ D_1 \yd \cS_1}{D_2\yd \cS_2} { D_{1} \And D_{2} \yd \cS_1\bar \cS_2}{ \yd\And}\vsk
 \ibnc{ D_1 \yd \cS_1}{D_2\yd \cS_2} { D_{1} \tensor D_{2} \yd \cS_1\bar
 \cS_2}{ \yd\tensor}
 \end{array}
\]
  \caption{Extracting  Contexts Schemata}
  \label{fig:schema}
\end{figure}
\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 $\ga\in\cS$ then $\ga\in S'\bar 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 $\bar$, 
$\ga\in S'\bar S$ iff $\ga\in S\bar 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\bar \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\bar\cS'}{\ins_1}$$
\itc$$\sigma=\ianc{(\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$\\
$\gap\in\cS$\bs
$\gap\in\cS\bar\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\bar\cS_2}}
\renewcommand{\insss}{\ins\cS_1\bar\cS_2}

% \begin{Lemma}
% \label{le:auxsplit}
% If $\ga\in \cS_1\bar\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\bar\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}
\mbox{} Let $\GG\vd \q$, where dom$(\q)=FV(\cD')\cup FV(D)$:
\ben
\item If $D\yd \cS$,  then $\dsat[ \q] D$.
\item If $\gap\vd G\yg \cS$, $\dsat[\q]\cD'$  and  $\ga\ins\cS$,
 then $(\GG,\GG');(\cD\And [\q]) \cD'\sla [ \q] G\inss$.
\enen
\end{Theorem}
\begin{proof}
By mutual induction on the structure of $\pi:: D\yd \cS$ and $\gamma::\gap \vd
G\yg \cS$.
\renewcommand{\q}{[\theta]}
\bit
\itc $$\pi=\ianc{X\in\{Q,\top,\perp\}}  {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{ D_1 \yd \cS_1}{D_2\yd \cS_2} { D_{1} \And D_{2}
  \yd \cS_1\bar \cS_2}{ \yd\And}$$
\btab
$ D_1 \yd \cS_1$\bs
$ 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}{D\yd \cS_2} {(G\Imp  D)\yd
  \cS_1\bar \cS_2}{ \yd\Imp}$$
\btab
$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\bar\cS_2$\bl{le:w}
$\dsats \q G\Imp\q D$\br $\dsat\Imp$
\etab
\itc $$\gamma= \ibnc{X\in\{Q,\top,\perp\}\mbox{ or (dis)eq}}{FV(\cD')=\Phi}
{\gap\vd  X\yg\GG';\some{\Phi} \cD'}{\yg X} $$
\btab
$\GG';\q\cD'\equiv_{\alpha}\GG';\q\cD'$\bh
$\GG';\q\cD'\in\GG';\some{\Phi} \cD'$\br $\in_1$\\
$\ga\ins\GG';\some{\Phi} \cD'$\bh
$\models_{\GG';\some{\Phi}\cD'} \q\cD'$\bh
$\gaex\ins\GG';\some{\Phi} \cD'$\br $\ins_2$\\
$\gaex\sla \q X\ins\GG';\some{\Phi} \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}{D\yd \cS_2}{  \gap\vd
  D\Imp G\yg \cS_1\bar \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}
$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\bar\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\bar \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\bar\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\bar\cS_2$\bl{le:w}
%$\GG_1;\cD_1\ins\cS_1\bar\cS_2$ and $\GG_2;\cD_2\ins S_1\bar\cS_2$\bl{le:w2}
%$\GG_1,\GG_2;\cD_1\And \cD_2\sla \q
%G_1\ins\cS_1\bar\cS_2$\bl{le:dsatweak}
%$\GG_1,\GG_2;\cD_1\And \cD_2\sla \q G_2\ins\cS_1\bar\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 the extracted schema; that
is,  that every
subgoal which arises in any given successful or failed (immediate and
non-immediate sub-derivation) satisfies the 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$.

\begin{Theorem}[Context Preservation \wrt Provability]
\label{thm:poscntpres}
Let $\dsat\cP$ and $D\in \defp(Q,\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 mutual induction on the structure of $\pi::\ga\sp G$ and $\iota::\ga\sp D\imm Q$. 
\bit
\itc $\pi$ ends in $\ga\sp \top$: trivial.
\itc $\pi$ ends in $\ga\sp D\Imp G$:
\btab
$\GG;\cD\And D\sp G$\bs
$\ga\sla D\Imp G\ins \cS$\bh
$\GG;\cD\And D\sla G\ins \cS$\bv
for any $\iota'::\gap\sp D'\imm Q$ and   $\dsat D'$ and \\
for any $\pi'::\GG';(\cD'\And D')\sp G'$ and  $\GG';(\cD'\And D')\sla G'\ins\cS$\bi  \\
for any $\pi'::\gap\sp D'\Imp G'$ and  $\gap\sla D\Imp G'\ins\cS$\br
\etab
\itc $\pi$ ends in $\ga\sp\PIXA G$:
\btab
$(\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
for any $\iota'::\gap\sp D'\imm Q$ and   $\dsat D'$ and\\
for any $\pi'::(\GG',y\oftp A);\cD'\sp[y/x] G'$ and  $(\GG',y\oftp
A);\cD'\sla[y/x] G'\ins\cS$ \bi \\
for any $\pi''::\gap\sp \PIXA G'$ and  $\gap\sla \PIXA G'\ins\cS$\br
\etab
\itc $\pi$ ends in $\vd\And,\vd\Or_1,\vd\Or_2,\vd\exists$: similarly by IH.
\itc $\pi$ ends in $\ga\sp Q$:
\bit
\item[Subcase]
\btab
$\iota::\ga\sp D\imm Q$, for $D\in \defp(Q,\cP$)\bs
%$\ga\sla Q\inss$\ba
%$\ga\inss$\bv
$\dsat D$\bh
for any $\pi'::\gap\sp G'$ and  $\gap\sla G'\ins\cS$ and \\
for any $\iota'::\gap\sp D'\imm Q$ and   $\dsat D'$\bi
\etab
\item[Subcase]
\btab
$\iota::\ga\sp D\imm Q$, for $D\in \defp(Q,\cD$)\bs
%$\ga\sla Q\inss$\bh
%$\ga\inss$\bv
$\dsat D$\` By Lemma \ref{le:ins}\\
for any $\pi'::\gap\sp G'$ and  $\gap\sla G'\ins\cS$ and \\
for any $\iota'::\gap\sp D'\imm Q$ and   $\dsat D'$\bi
\etab
\enit
\itc $\iota::\ga\sp\perp\imm Q$: trivial.
\itc $\iota::\ga\sp D_1\And D_2\imm Q$:
\btab
$\dsat D_1\And D_2$\bh
$\dsat D_1$ and $\dsat D_2$\` By inversion
\etab
\bit
\item[Subcase]
\btab
$\ga\sp D_1\imm Q$\bs
for any $\pi'::\gap\sp G'$ and  $\gap\sla G'\ins\cS$ and \\
for any $\iota'::\gap\sp D_1'\imm Q$ and   $\dsat D_1'$ \bi\\
for any $\iota''::\gap\sp D_1'\And D_2'\imm Q$ and   $\dsat
D_1'\And D_2'$ \br
\etab
\item[Subcase]
\btab
$\ga\sp D_2\imm Q$\` Symmetrical
\etab
\enit %ends subcase
\itc 
$\iota::\ga\sp\PIXA D\imm Q$
\btab
$\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\\
for any $\pi'::\gap\sp G'$ and  $\gap\sla G'\ins\cS$ and \\
for any $\iota'::\gap\sp[t/x] D'\imm Q$ and   $\dsat [t/x]D'$\bi\\
for any $\iota''::\gap\sp \PIXA D'\imm Q$ and   $\dsat \PIXA D'$\br
\etab
\itc
$\iota::\ga\sp G\Imp D\imm Q$:
\btab
$\ga\sp D\imm Q$ and $\ga\sp G$\bs
$\dsat G\Imp D$\bh
$\ga\sla G\inss$ and $\dsat D$\bv
for any $\pi'::\gap\sp G'$ and  $\gap\sla G'\ins\cS$ and \\
for any $\iota'::\gap\sp D'\imm Q$ and   $\dsat D'$\bi\\
for any $\iota''::\gap\sp G'\Imp D'\imm Q$ and   $\dsat G'\Imp D'$\br
\etab
\itc $\iota$ ends in $\imm\tensor, \imm\Pi$: similarly by IH.
\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}{[ \theta']} 
\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\in \defp(Q,\cP\And\cD$);
 \renewcommand{\q}{[ \theta]} 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}{[ \theta]}
\renewcommand{\foq}{\mbox{\textrm{for all }$\theta$  }}
By mutual induction on the structure of $\pi::\ga\fp\q G$ and
$\iota::\ga\fp\q D\imm\q Q$, as above. We show only some cases:
\bit
\itc
$$\pi=\ibnc{\mbox{\rm for all $n,\theta$ }\GG\vd n\hastype A}{\ga\fp[\theta,n/x] G}
{\foq\ga\fp\q\exa G}{\nvd\exists}$$
\btab
$\foq, n\ \ga\fp[\theta,n/x] G$\bs
$\foq\ga\sla\q\exa G\inss$\bh
$\foq\ga\sla[\theta,u/x]  G\inss$\bv
$\foq, n\  \ga\sla[\theta,n/u,u/x]  G$\` By substitution\\
for any $\iota'::\gap\fp\qp  D'\imm\qp  Q$ and   $\dsat \qp D'$
and \\
for any $\pi'::\gap\fp [\theta',n/x]G'$ and   $\gap\sla [\theta',n/x]  G'\ins\cS$ \bi
\\
for any $\pi''::\gap\fp \qp \exa G'$ and   $\gap\sla \qp  \exa G'\ins\cS$ \br
\etab
\itc
$$\pi= \ianc{\foq\GG;(\q\cD\And \q D )\fp \q G}{\ga\fp \q D \Imp\q
  G}{{\nprv} \Imp}$$
\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
for any $\iota'::\gap\fp\qp  D'\imm\qp  Q$ and   $\dsat \qp D'$ and\\
for any $\pi'::\GG;(\qp\cD'\And \qp D')\fp \qp G'$ and   $\GG;(\qp\cD'\And \qp D')\sla \qp  G'\ins\cS$ \bi \\
for any $\pi''::\gap\fp \qp (D'\Imp G')$ and   $\gap\sla \qp (D'\Imp
G')\ins\cS$ \br 
\etab
\itc
$$\iota=\ianc{\foq\ga\fp\q G}{\foq\ga\fp \q D\If\q G \nimm \q
  Q}{\notimm{\Imp_1}}$$
\btab
$\foq\ga\fp\q G$\bs
$\foq\dsat\q G\Imp \q D$\bh
$\foq\ga\sla\q G\inss$ and $\dsat\q D$\bv
for any $\pi'::\gap\fp G'$ and   $\gap\sla G'\ins\cS$ and \\
for any $\iota'::\gap\fp \qp D'\imm\qp Q$ and     $\dsat \qp D'$\bi\\
for any $\iota''::\gap\fp\qp  (D'\If G')\imm\qp  Q$ and    $\dsat
\qp (D'\If G')$\br
\etab
\itc 
$$\iota=\ianc{\foq\ga\fp\q D\imm \q Q} {\foq\ga\fp  \q D
  \If \q G \nimm \q Q}{\notimm{\Imp_2}}$$
\btab
$\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
for any $\pi'::\gap\fp \qp G'$ and   $\gap\sla \qp  G'\ins\cS$ and \\
for any $\iota'::\gap\fp\qp  D'\imm\qp  Q$ and    $\dsat \qp D'$\bi\\
for any $\iota''::\gap\fp\qp  (D'\If G')\imm\qp  Q$ and    $\dsat
\qp (D'\If G')$\br
\etab
\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^-}



