% \newcommand{\mnot}{{\rm Not\ }}
\newcommand{\mnots}{{\rm Not^* }}
\newcommand{\mnotd}{{\rm Not_{$D$} }}
\newcommand{\mnotg}{{\rm Not_{$G$} }}
\newcommand{\PP}{\cP^{+}}
\newcommand{\PM}{\cP^{-}}
\newcommand{\spp}{\prv_{\PP}}
\newcommand{\fpp}{\not\prv_{\PP}}
\newcommand{\snp}{\prv_{\PM}\mnot}
\newcommand{\fnp}{\not\prv_{\PM}\mnot}
\newcommand{\fn}{\not\prv_{\PM}}
\renewcommand{\sn}{\vdash_{\PM}}
\renewcommand{\sp}{\vdash_{\cP}}
\newcommand{\fp}{\not\vdash_{\cP}}
\newcommand{\cA}{{\cal A}}
\newcommand{\ga}{\GG;\cA}
\newcommand{\gna}{\GG;\mnots\cA}
\newcommand{\vN}{\vec{N}}
\newcommand{\vM}{\vec{M}}
\newcommand{\al}{\alpha}

\bedef[Complementable]
\label{de:complem}

A program $\cP$ over a signature $\Sigma$ is \emph{complementable} if 
every crucial predicate is well-founded.  A predicate 
is \emph{crucial} if  it occurs in the program both positively and 
negatively. Such a predicate $q$ is \emph{well-founded} if it satisfies 
the following:
\[
\all n\in Neg_{q}(\cP), \all p\in Pos_{q}(\cP), head(n) <_{lex} p
\]
where $<_{lex} $ is the lexicographical extension of the \ho 
subterm ordering and $Neg[Pos]$\footnote{fill in} are the sets of 
negative[positive] occurrences of $q$
\enef
For example $(of\ !x\ T_{1}) <_{lex} (of\ (E\ x) \ T_{2})$ hence the 
program is complementable. On the contrary
\beq
impI & : & pf\ (A \supset B) \If (pf\ A \Imp pf\ B)
\eneq
is not, as $ (pf\ A) \not< (pf\ B)$.
The condition can be made less stringent by requiring that $ head(n) <_{lex} 
p$ only for those $n,p$ which are connected in the calling graph.


\smallskip
Some programs which are complementable require \emph{augmentation} to 
become `assumption-complete':
\bedef A program $\cP$ is \emph{assumption-complete} if for every 
parameter
\ben
\item either $\al(\PP)$ or $\al(\PM)$
\item it is not the case that both either $\al(\PP)$ and $\al(\PM)$
\enen
\enef
For example \texttt{open} requires an addition to its lambda case:
\beq
 oplam &: & open\ (lam\ E)  \If \Pi x : exp.\ open\ (E\ x)\\
 aug(openlam) & : & open\ (lam\ E) \If \Pi x : exp.\ \neg open\ x 
\Imp open\ (E\ x) \eneq

We assume for now this phase completed\footnote{as I do not 
understand it fully}.


\section{Assumptions}

Assumptions are contexts which contains all negative occurrences of a 
goal: at the moment we collect together clause assumptions and 
parameter assumptions (to avoid context within context) a' la 
\emph{Elf}.  Logical variables are declared in a pool and left here
implicit.
\[
\alpha \bnfas \cdot\mid\al,x : A,\mid\al,D
\]
$\alpha(G)$ is defined as:
\beq
\al(P) & = & \cdot\\
\al(\Pi x:A.G) & = & x:A,\al(G)\\
\al(D\Imp G) & = & D,\al(G)
\eneq

Let $m_i : P_{i} \If G_{i}$ and $def(P) = \bigcup_{i=1}^{n} m_{i}$: 

\beq
\al(m_{i}) & = & \al(G_{i})\\
 \al(def(P)) & = &  \bigcup_{i=1}^{n} \al(m_{i})\\
\al(\cP) & = & \bigcup_{P\in\Sigma_\cP} \al(def(P)) \eneq
For example, 
$\al(cplam) = x:exp,y:exp, copy\ x\ y$. 

% Assumptions may need to be 
%left-linearized: $$\al(sublam) = z:exp, \Pi M_{1},M_{2} : exp.\ sub\ 
%(\lx z) \ M_{1} \ M_{2}\If eq_{exp}\ M_{2} \ z$$ where $M_{2}$ is a fresh 
%variable. 
 Note that for second-order complementable programs, assumptions 
are \fo and thus we can think the equality theory as already 
computed\footnote{explain better and add pointer to operational semantics 
of parameters disequations}.


Negation of a context\footnote{I know this is not quite right}:
\[
\mnots \alpha \bnfas \cdot\mid \mnots \al,x : A,\mid \mnots\al,\mnots D
\]
where
\beq
\mnots x: A, q\ x & = & x: A, \neg q\ x\\
\mnots x: A, q\ x\ \vM & = & x: A, \neg q\ x\ \vN \If  
neq_{\vec{B}} \ \vN\ \vM\\
\mnots (P\If G) & = & \mnot\ P \If \mnot\ G\\
\mnots (G\Imp G') & = & \mnots G \Imp \mnots G'
\eneq
For example:
\beq
\al(oflam) & = & x: exp,  of\ x\ T_{1}\\
\mnots \al(oflam) & = & x: exp, \neg of\ x\ T \If neq_{\tau} \ T\ T_{1}\\
\mnots \al(sublam) &= & z:exp, \Pi M_{1},M_{2} : exp.\ \neg sub\ 
(\lx z) \ M_{1} \ M_{2}\If neq_{exp}\ M_{2} \ z
\eneq

\beq
inall & : & inst\ (all\ A) \ B \If \Pi x : exp.\ term\ x \Imp copy\ x\ T 
\Imp inst\ (A\ x)  \ B\\
\al(inall) & = & x : exp. term\ x, copy\ x\ T\\
\mnots \al(inall) & = & x : exp. term\ x, \neg copy\ x\ T' \If 
neq_{exp} \ T\ T'
\eneq

Extended language: fix a signature
\beq
D & \bnfas & P \mid\top\mid P\If (\al(\cP)\Imp G)\mid \Pi x:A.D\mid 
\all x:A.D\mid D_1 \And D_2 \\
G &\bnfas & P \mid eq_A M\ N\mid neq_A M\ N\mid\top \mid G_1 \And G_2 
\mid G_1 \lor G_2 \mid \al(\cP)\Imp G\mid \Pi x:A.G
 % \mid\exists x:A.G
\eneq


Success and failure of complementable programs: $\cA$ is a set of assumptions, 
$\GG$ records parameters.  For this judgment, temporarily, we drop 
quantification from programs in favor of logical variables which are 
in two separate categories: the first instantiates only on closed 
terms, the other is unrestricted\footnote{This is ugly and not precise, 
but please bear with me; suggestions welcome, by the way}.  Goals are 
\emph{closed}, no existentials are allowed.

\[
\begin{array}{c}
\ianc{q\ \vN\in \cP\cup\cA\quad\GG\prv \vM\in\|\vN\|}{\ga\sp q\ 
\vM}{Sa1} 
\qquad
\ianc{\all (q\ \vN)\in \cP\cup\cA\quad\GG\prv 
\vM\not\in\|\vN\|}{\ga\fp q\ \vM}{Fa1} 
\vsk 
\ianc{q\ \vN\If G\in \cP\cup\cA,\GG\prv \vM\in\|\vN\|\quad \ga\sp G}
{\ga\sp q\ \vM}{Sa2} 
\qquad 
\ianc{\all(q\ \vN\If G)\in \cP\cup\cA,\GG\prv \vM\in\|\vN\|\quad 
\ga\fp G}
{\ga\fp q\ \vM}{Fa2} 
 \vsk 
\ianc{\ga\sp G_1\quad\ga\sp G_{2}}{\ga\sp G_{1}\And G_{2}}{S\And}
\qquad
\ianc{\ga\fp G_i}{\ga\fp G_{1}\And G_{2}}{F\And}
\vsk
\ianc{\ga\sp G_i}{\ga\sp G_{1}\Or G_{2}}{S\Or}
\qquad
\ianc{\ga\fp G_1\quad\ga\fp G_{2}}{\ga\fp G_{1}\Or G_{2}}{F\Or}
\vsk
\ianc{\GG;\cA,\al\sp G}{\ga\sp \al\Imp G}{S\Imp}
\qquad
\ianc{\GG;\cA,\al\fp G}{\ga\fp \al\Imp G}{F\Imp}
\vsk
\ianc{\GG,y:A;\cA\sp[y/x]G}{\ga\sp \Pi x:A.G}{S\Pi}
\qquad
\ianc{\GG,y:A;\cA\fp[y/x]G}{\ga\fp \Pi x:A.G}{F\Pi}
\end{array}
\]



\begin{Lemma}[Weakening]
Assume $\ga\sp G$; then
\ben
\item $\ga,\al\sp G$
\item $\GG,x:B; \cA\sp G$.
\enen
\end{Lemma}
\begin{proof}
\ben
\item by induction on $\sp$.
\item by induction on $\sp$, using Lemma \ref{le:weak}
\enen
\end{proof}
This lemma will be used tacitly.

\section{The algebra of clause complementation}

Source language:

\beq
G & \bnfas & P\mid G_{1}\And G_{2}\mid D\Imp G\mid \Pi x:A.G\\
D & \bnfas & P\mid \Pi x:A. D\mid P \If G \\
\cP & \bnfas & \cdot\mid D,\cP
\eneq

\bedef[Clause Complementation]
\label{def:palgebra}
\beq
\mnotd (\Pi x:A. D) & = & \mnotd (D)\\
\mnotd(P\If G) & = & \mnotd(P) \cup\{ \neg P \If \mnotg(G) \}\\
\mnotd( q\ \vM) & = & \{ \neg q\ \vN\mid \vN\in \mnot(\vM) \}
\eneq
where $\mnotg$ is defined on goals as follow:
\beq
\mnotg(P) & = & \neg P\\
\mnotg(G_{1}\And G_{2}) & = & \mnotg(G_{1}) \Or \mnotg(G_{2}) \\
% \mnotg(G_{1}\If G_{2}) & = & \mnotg(G_{1}) \Or \mnotg(G_{2}) \\
\mnotg(G_{1}\Or G_{2}) & = & \mnotg(G_{1}) \And  \mnotg(G_{2}) \\
\mnotg(D\Imp G) & = & D \Imp \mnotg(G) \\
\mnotg(\Pi x:A.G) & = & \Pi x:A. \mnotg(G) \\
\eneq
\enef

Given $m : P\If G$, we call $ \mnotd m$ the \emph{m-candidates}.  
Candidates represent the potential negative contribution of each 
clause: the `factual' part $\mnotd(P) $ motivates failure due to clash 
with the head of $m$; the remainder $\mnotg G$ expresses failure in the body.  
Candidates from each clause in the definition of a predicate need to 
be merged.  This is accomplished by the intersection operator 
$\otimes$.  The latter corresponds to the unification of the heads and 
the pairing of the bodies. In fact `factual' failure needs to be 
considered simultaneously: and this is achieved  by `anding' the 
complement of each head. In the disunification approach this is 
achieved by solving the equation and disequations collected in the 
completion formula.
In the \ho setting the intersection operator has less 
pleasant algebraic properties as its \fo counterpart \cite{MP90}, due 
to the possible lack of mgu's.  We therefore use complete sets of 
unifiers \cite{Hue75} (\emph{CSU}). .

\bedef[$\otimes$]
For $m1: P_{1}\If G_{1}$ and  $m2: P_{2}\If G_{2}$
\beq 
m1 \otimes m2 & = & \{ \vec{\Pi} \q(P_{1}\If G_1\And G_2)\mid \q\in CSU(P_{1},P_{2}) \} 
% \\ \cP_{1} \otimes \cP_{2} & = & \{ m1 \otimes m2\mid m1 \in \cP_{1}, 
% m2 \in \cP_{2} \} 
\eneq
where $\vec{\Pi} D$ denotes the universal closure of $D$.
\enef 

\bedef[Program complementation]
\label{def:palgebra}
Given $\cP$, let $m_i : q\ \vM_{i} \If G_{i}$ and $def(q) = 
\bigcup_{i=1}^{n} m_{i}$:
\beq
\mnotd(def(q)) & = & \bigotimes_{i=1}^{n} \mnotd(m_{i})\\
\mnotd(\cP) & = &  \bigcup_{q\in\Sigma_{\cP}} \mnotd def(q)
\eneq
\enef
We abbreviate  $\mnotd(def(q))$ in  $def(\neg q)$. If $\PP$ is the
source program, we use $\PM$ for $\mnotd \PP$.

\begin{Examplen}
\beq
cloz & : & closed\ z\\
clolam &: & \Pi E:exp.\ closed\ (lam\ E) \If \Pi x : exp.\ (closed\ x) 
\Imp closed\ (E\ x)\\
cloapp &: & \Pi E_{1}E_{2}:exp.\ closed\ (app\ E_{1} E_{2}) \If 
closed\ E_1 \And closed\ E_{2}\\
\eneq
Let $def(closed)= \{cloz,clolam,cloapp\}$

\beq
\mnotd cloz & = & \mnotd closed\ z \\
            & = & \{\neg closed\ N\mid N\in\mnot z\}\\
            & = & \{ closed\ lam\ F, closed\ app\ F_{1} \ F_{2}\}\\
\vsk
\mnotd clolam & = & \mnotd (closed\ lam\ E) \cup
\neg closed\ (lam\ E) \If \mnotg (\Pi x : exp.\ (closed\ x) \Imp closed\ 
(E\ x))\\
              & = & \{\neg closed\ N\mid N\in\mnot lam\ E\}\cup
\neg closed\ (lam\ E) \If \mnotg (\Pi x : exp.\ (closed\ x) \Imp closed\ 
(E\ x))\\
              & = & \{closed\ z, closed\ app\ F_{1} \ F_{2},  
\neg closed\ (lam\ E) \If \Pi x : exp.\ (closed\ x) \Imp \neg closed\ 
(E\ x))\\
\vsk
\mnotd cloapp & = & \mnotd closed\ (app\ E_{1} E_{2})\cup
\mnotg ( closed\ (app\ E_{1} E_{2}) \If closed\ E_1 \And closed\ 
E_{2})\}\\
              & = & \{\neg closed\ N\mid N\in\mnot closed\ (app\ E_{1} 
E_{2})\}\cup\mnotg (closed\ (app\ E_{1} E_{2}) \If closed\ E_1 \And 
closed\ E_{2})\\
              & = & \{closed\ z,  closed\ app\ F_{1} \ F_{2}, \neg closed\ (app\ E_{1} E_{2}) \If
\neg closed\ E_1 \Or \neg closed\ E_{2})
\eneq
Now, $def(\neg closed) = (\mnotd cloz) \otimes ((\mnotd clolam) 
\otimes (\mnotd cloapp))$, \ie:
\beq
\Pi E : exp.\ \neg closed\ (lam\ E) \If \Pi x : exp.\ closed\ x \Imp 
\neg closed\ (E\ x)\\
\Pi E_{1}E_{2}:exp.\ \neg closed\ (app\ E_{1} E_{2}) \If 
\neg closed\ E_1 \Or \neg closed\ E_{2}
\eneq
which by renaming and irrelevance of augmentation \ref{??} is 
equivalent to the expected definition of \texttt{open} on the same 
signature:
\beq
oplam &: & \Pi E : exp.\ open\ (lam\ E)  \If \Pi x : exp.\ open\ (E\ x)\\
opapp &: & \Pi E_{1}E_{2}:exp.\ open\ (app\ E_{1} E_{2}) \If open\ E_1 \Or open\ E_{2}
\eneq
\end{Examplen}


Note that for the fragment covered in this dissertation CSU's are 
unary (fully applied patterns) or at most finitary (non-fully applied 
ones \cite{CP97}) For infinite CSU's, we can achieve a finite 
presentation, by adopting a CLP attitude.  For $mi : q\ \vM_{i}\If 
G_{i}$, for $i=1,2$:
\beq
 m1 \otimes' m2 & = & q\ \vX\If (\vX \ebe \vM_{1}) \And (\vX \ebe \vM_{2}) 
 \And G_1\And G_2
\eneq

\begin{Ppn} $\otimes$ is associative, idempotent, commutative.
\end{Ppn}
\begin{proof} It follows immediately by definition of CSU.
\end{proof}

This property is useful as it allows to build the complementation of a 
predicate in an \emph{incremental} fashion, by merging pairwise, in 
arbitrary order the $m$-candidates.  Moreover we could prove that 
$\otimes$ is distributive \wrt union.  De Morgan holds as well as 
double negation elimination.  This would eventually lead, together 
with the fundamental result Theorem \ref{th: ppart}, to the fact that 
the algebra of terminating programs is boolean.


In the usual horn setting undefined predicates, \ie predicates which 
occur only in bodies of clauses are dealt with in the transformational 
approach by adding the `universal' negative clause, say $\Pi \vx . \neg q\ 
\vx$.  We have to refine this to treat \emph{hypothetically defined} 
predicates, \ie undefined crucial predicates: for those we add instead 
an extensional negative clause: $\all \vx . \neg q\ \vx$, where the 
latter quantifier instantiates only to closed terms.

\begin{Examplen}
\[
\begin{array}{l}
universal (\lx Q\ x) \If \Pi x : exp. term x \Imp universal (Q\ x)\\
\ldots\\
\all x: exp.\ \neg term\ x
\end{array}
\] 
\end{Examplen}

We state some basic properties:

\begin{Lemma}
\label{le:2}
$\GG\prv \vM \in \|  \vN_1\|$ and $\GG\prv \vM \in \| \vN_2\|$ iff
$\GG\prv \vM \in \| \vN_1\|\cap \| \vN_2\|$.
\end{Lemma}
\begin{proof} Obvious
\end{proof}

\begin{Lemma}
\label{le:facts}
If $def(q) = \bigcup_{i=1}^{n} q\ \vM_i \If G_i$ in $\PP$, $facts(\neg q)
= \bigotimes_{i=1}^{n} \{\neg q \ \vN \mid \vN\in\mnot \vM_i\}$.
\end{Lemma}
\begin{proof}
Obvious from Definition \ref{def:calgebra} and Lemma \ref{le:2}.
\end{proof}

\begin{Lemma}
\label{le:emptydef}
$\Pi \vX: A.  q\ \vX$ is in $def(q)$ iff $def(\neg q) = \eset$.
\end{Lemma}
\begin{proof}
Immediate by  Definition \ref{def:calgebra}.
\end{proof}


\begin{Lemma} 
\label{le:per}
Given clauses $m1: q\ \vN_{1}\If G_{1}$ and $m2: q\ 
\vN_{2}\If G_{2}$ in $\PP$ then 
\beq
Rules(\mnotd m1 \otimes \mnotd m2) & =  &\\
\{\neg q\ M'_{1}\If G'_{1}\mid M'_{1}=\q M_{1}, \q\in CSU(M_{1},S), 
S\in\mnot M_{2}\} \cup
\{\neg q\ M'_{2}\If G'_{2}\mid M'_{2}=\q M_{2}, \q\in CSU(M_{2},S), 
S\in\mnot M_{1}\}\\
& & \mbox{if $M_{1}$ and $M_{2}$ are not unifiable}\\
&  \neg  q\ \vN_{1}\If \notg G_{1}\otimes \neq q\ 
\vN_{2}\If\notg G_{2} & \mbox{otherwise}
\eneq
\end{Lemma}
\begin{proof}
By Definition \ref{def:palgebra}
\end{proof}


% \begin{Lemma} 
% \label{le:per}
% Given clauses $m1: q\ \vN_{1}\If G_{1}$ and $m2: q\ 
% \vN_{2}\If G_{2}$ in $\PP$  for all clause $ nm: \neg q\ \vN\If \mnot 
% G$ in $\mnot(m1\cup m2)$ it holds:
% \ben
% \item
% $\fnp  G$ only if $\fnp  G_{1}$ or $\fnp  G_{2}$
% \item
% $\snp G$ only if $\snp G_{1}$ and $\snp G_{2}$.
% \enen
% \end{Lemma}
% \begin{proof}
% Suppose $\vM_{1}$ and $\vM_{2}$ are unifiable: then set $nm$ to 
% $\mnot(m1)\otimes\mnot(m2)$.  Otherwise, considering symmetries, there 
% is a fact $\neg q\ S$ in $\mnot (m2)$ such that $S$ and $\vM_{1}$ are 
% unifiable.  Then let $\vN$ be $\q \vM_{1}$ for $\q\in CSU(\vM_{1},S)$ and $G$ 
% be $\q G_{1}$.  Note that $\vM_{1}$ is more general then $\vM$.  Thus, in 
% both cases it is easy to see that, by inversion on failure and success 
% of conjunctive goals, $1.$ and $2.$ hold.
% \end{proof}
% 

\begin{Lemma}[Persistence]
\label{co:per}
Given   clauses $m_i : q\ \vN_{i} \If G_{i}$ in  $def(q)$
 in $\PP$,  for all  clauses $ nm: \neg q\ \vN\If \mnot 
G$ in $def(\neg p)$ in $\PM$ it holds that:
\ben
\item
$\fnp  G$ only if there is an $i$ s.t.\ $\fnp  G_{i}$
\item
$\snp G$ only if  for every $i$: $\snp G_{i}$.
\enen
\end{Lemma}
\begin{proof}
By iteration of Lemma \ref{le:per} on $def(q)$.  Note that for every 
$i$ it is the case that $\vM_{1}$ is more general then $\vM$.  Thus 
it is easy to see that, by inversion on failure and success of 
conjunctive goals, $1.$ and $2.$ hold.
\end{proof}


\section{Main result}

As we did with terms, we wish to prove that the $\mnotd$ operator does behave as
 complementation on programs, \ie that for any complementable program and 
allowed goal:
\begin{Theorem}
\label{th: ppart}
\ben
\item (Disjointness) It is not the case that $\ga\spp G$ and $\gna\snp  G$.
\item (Exhaustivity) $\ga\spp G$ or $\gna\snp  G$.
\enen
\end{Theorem}

As we need to prove this by induction on the length of a success or failure
derivation from the positive program, we reformulate the above claim
in the following equivalent form, under the assumption of termination 
of $G$ \wrt $\cP$.

\begin{Ppn}[Disjointness]
If $\ga\spp G$ then $\gna\fnp  G$
\end{Ppn}
\begin{proof}
Base: case Sa1: $\ga\sp q\ 
\vM$ only if $q\ \vN\in \cP\cup\cA$ and $\GG\prv \vM\in\|\vN\|$. Subcase $1$:
there is a clause $\Pi \vX. q\ \vX$ in $\PP$. Then, by Lemma \ref{le:emptydef}
$def(\neg q) = \emptyset$ and $\neg q\ \vM$ fails trivially.
 Otherwise, 
there is at least an $i$ such that $\GG\prv \vM \in \|\vN_i\|$. Then
by the term partition lemma (\ref{le:part}) $\GG \prv\vM\in \|\vec(S)\|$ for $\vec{S}\in \mnot \vN_i$.
Hence, for every $\q$, $\GG\prv\vM\not\in\|\q\vec{S}\|$ for $\neg q\ \q\vec{S}$
 in $facts(\neg q)$. Again $\gna\fn \neg q\ \vM$.

%take $def(q)=\bigcup_{i=1}^n q\ \vN_i$
%Then $heads(\mnot q) = \bigotimes_{i=1}^n \{\neg q\ s\mid \GG s\in\|\mnot(\vN_i)\|\}$.  By the term partition lemma (\ref{le:part}) $\GG \vM\not\in \|s\|$ 
%for all $s$ s.t. $\neg q\ s \If G$ in $\PM$. Again it fails at length $1$.

Step:
\bit
\item Case Sa2. Suppose $\ga\spp q\ \vM$; then
 $q\ \vN\If G\in \cP\cup\cA,\GG\prv \vM\in \|\vN\|$ and $\ga\spp G $. By induction hypothesis $\gna\fnp G$. By 
persistence (Corollary \ref{co:per}) $\gna\fnp q\ \vM$.
\item Case $S\Pi$. $\ga\spp \Pi x:A.G$ iff $
\GG,y:A;\cA\spp[y/x] G$ which entails, by IH, $\GG,y:A;\mnots\cA\fnp[y/x]G$
iff  $\ga\fnp \Pi x:A.G$
\item Case $S\Imp$. $\ga\spp \al\Imp G$ iff  $\GG;\cA,\al\spp G$, which by IH
entails $\GG;\mnots\cA,\al\fnp G $ iff $\ga\fn \al\Imp \mnot G$
 iff $\ga\fnp (\al\Imp G)$.
\enit
The rest analogously follows by IH.
\end{proof}



\begin{Ppn}[Exhaustivity]
If $\ga\fpp G$ then $\gna\snp  G$
\end{Ppn}
\begin{proof}
Base: case Fa1: Subcase $1$: there is no definition for $q$ in $\PP$.  
Then $\all \vx .\neg q\vx\in \PM$ and $\neg q\ \vM$ is provable.  
Otherwise, $\all (q\ \vN)\in \cP\cup\cA\quad\GG\prv 
\vM\not\in\|\vN\|$.  By the term partition lemma (\ref{le:part}) 
$\GG\prv \vM\in \|\mnot \vN_i\|$.  By lemma \ref{le:2} $\neg q\ \vM$ 
follows from $\neg q\ \vec{S}$ for $\vec{S} \in \bigcap_{i=1}^n \mnot 
\vN_i$.

Step:
\bit
\item Case Fa2.\footnote{see manuscript}
\item Case $F\Imp$. $\ga\fpp \al\Imp G$ iff  $\GG;\cA,\al\fpp G$, which by IH
entails $\GG;\mnots \cA,\al\snp G $ iff  $\ga\sn \al\Imp \mnot G$ iff
 $\ga\snp (\al\Imp G)$.
\enit
The rest analogously follows by IH.
\end{proof}