\subsection{Schema Extraction}

Roughly, we extract schemata 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 schema
alternatives for each clause in the given program. When an atomic goal
is reached, the current list of parameter and assumption is returned,
with the correct binding. We formalize this in
Figure~\ref{fig:schema}.  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, \ie 
\beq
\ga\bar\cdot;\top=\cdot;\top\bar\ga=\ga 
\eneq
Finally $\bar$ is commutative.

\begin{figure}[htbp]
  \label{fig:schema}
\[
\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^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\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^u}\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 Schema Contexts}
\end{figure}

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

\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 $\ga\in S'\bar S$ iff $\ga\in S\bar S'$.
\begin{Lemma}
\label{le:w2}
If $\ga\ins\cS$, then $\ga\ins \cS\bar \cS'$.
\end{Lemma}
\begin{proof}
By induction on the structure of $\pi::\ga\ins\cS$
\bit
\itc $$\pi=\ianc{}{\cdot;\top\ins \cS}{\ins_1}$$
Then immediately:
 $$\pi'=\ianc{}{\cdot;\top\ins \cS\bar\cS'}{\ins_1}$$
\itc$$\pi=\ianc{(\GG';\cD')\in
\cS\quad \GG';\top\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\\
$\gap\in\cS$\bs
$\gap\in\cS\bar\cS'$\` By Lemma \ref{le:w1}\\
$(\GG,\block{\GG'});(\cD\And\block{\cD'})\insss$\br $\ins_2$
\etab
\enit
\end{proof}


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

\itc$$\pi=\ibnc{\ga\dsat D}{\ga\sla G\inss}{\ga\dsat G\Imp  D}{\dsat\Imp}$$
\btab
%$\ga\inss$\bh
$\ga\dsat D$\bs
$\ga\dsats D$\bi $1$\\
$\ga\sla G\inss$\bs
$\ga\sla G\insss$\bi $2$\\
$\ga\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$\bl{le:w2}
$\ga\sla X\insss$\br $\sla X$
\etab
\itc$$\gamma=\ibnc{\ga\dsat D}{\GG;\cD\And D\sla G\inss}{\ga\sla D\Imp
  G\inss}{\sla\Imp}$$
\btab
$\ga\dsat D$\bs
$\ga\dsats D$\bi $1$\\
$\GG;\cD\And D\sla G\inss$\bs
$\GG;(\cD\And D)\sla G\insss$\bi $2$\\
$\ga\sla G\Imp D\insss$\br
\etab
\enit
\end{proof}

\renewcommand{\dsats}{\models_{\!\cS_1\bar\cS_2}}
\begin{Theorem}[Extracted Schema Satisfaction]
\label{thm:yieldsat}
\mbox{}
\ben
\item If $D\yd \cS$ and $\ga\inss$,  then $\ga\dsat D$.
\item If $\gap\vd G\yg \cS$ and $\ga\inss$, then $\ga\sla 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$.
\bit
\itc $$\pi=\ianc{X\in\{Q,\top,\perp\}}  {X\yd \cdot;\top}{\yd X}$$
\btab
$\cdot;\top\dsat X$\br $\yd X$\\
$\ga\inss$\bh
$\ga\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
$ \ga\dsato D_1$\bi $1$\\
$\ga\dsatt D_2$\bi $1$\\
$\ga\dsats D_1$\bl{le:w}
$\ga\dsats D_2$\bl{le:w}
$\ga\dsats D_1\And D_2$\br $\dsat\And$
\etab
\itc $\pi$ ends in $\yd\tensor$: analogously to the above.
\itc $\pi$ ends in $\yd\Pi^u$: 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
$\ga\models_{\!\cS_2} D$\bi $1$\\
$\ga\dsats D_1$\bl{le:w}
$\cdot;\top\vd G\yg \cS_1$\bs
$\ga\ins\cS_1$\bh
$\cdot;\top\sla G\ins\cS_1$\bi $2$\\
$\ga\sla G\ins\cS_1$\bl{le:dsatweak}
$\ga\sla G\ins\cS_1\bar\cS_2$\bl{le:w}
$\ga\dsats G\Imp D$\br $\dsat\Imp$
\etab
\itc $$\gamma= \ibnc{X\in\{Q,\top,\perp\}\mbox{ or (dis)eq}}{FV(\cD')=\Phi}{\ga[\vd
  X\yg\GG';\some{\Phi} \cD'}{\yg X} $$
\bmeta Need $\q$\emeta
\btab
$\ga\ins\gap$\bh
$\ga\sla X\ins\gap$\br $\ins X$
\etab
\itc
$$\gamma=\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}$$
\btab
$\GG;(\cD\And D)\vd G\yg \cS_1$\bs
$\GG;(\cD\And D)\sla G\ins\cS_1$\bi $2$\\
$\GG;(\cD\And D)\sla G\ins\cS_1\bar\cS_2$\bl{le:w}
$D\yd\cS_2$\bs
$\ga\dsatt D$\bi $1$\\
$\ga\dsats D$\bl{le:w}
$\ga\sla D\Imp G\ins\cS_1\bar\cS_2$\br $\sla\Imp$
\etab
\itc $\gamma$ ends in $\yg\And,\yg\Or$: by  IH $2$ and Lemma
\ref{le:w} as above.
\itc $\gamma$ ends in $\yg\Pi^y,\yg\exists^u$: by an immediate appeal
to IH $2$.
\enit
\end{proof}

