\def\vd{\null\mathrel{\vdash}} %Frank's
\def\nprv{\null\mathrel{\not\vdash}} %Frank's
\renewcommand{\prv}{\vd}
 \renewcommand{\mnot}{{\rm Not }}
\newcommand{\mnots}{{\rm Not^* }}
\newcommand{\eqd}{\stackrel{\cdot}{=}}
\newcommand{\neqd}{\stackrel{\cdot}{\neq}}
\newcommand{\eq}{\approx}
\renewcommand{\neq}{\neg\approx}
%\newcommand{\mnotd}{{\rm Not}_{\mbox{$D$} }}
%\newcommand{\mnotg}{{\rm Not}_{{\mbox{$G$} }}}
\newcommand{\mnota}{{\rm Not}_{\mbox{$\alpha$} }}
\newcommand{\mnotd}{{\rm Not}_{\rm D}  }
\newcommand{\mnotg}{{\rm Not}_{\rm G}  }
\newcommand{\ald}{\alpha_{\mbox{$\tiny {\textrm{D}}$}}}
\newcommand{\alg}{\alpha_{\mbox{$\tiny {\textrm{G}}$}}}
% \newcommand{\PI}[2]{\Pi {#1}\!:\!{#2}.\,}
\newcommand{\of}[2]{ {#1} \!:\! {#2}}
\newcommand{\dspc}{.\,}
\newcommand{\PIXA}{\Pi x\!:\!A.\,}
\newcommand{\EXA}{\exists x\!:\!A.\,}
\newcommand{\PP}{\cP^{+}}
\newcommand{\PM}{\cP^{-}}
\renewcommand{\sp}{\prv_{\cP}}
\newcommand{\spp}{\prv_{\!_\PP}}
\newcommand{\snp}{\prv_{\!_\PM}\mnotg }
\newcommand{\sn}{\prv_{\!_\PM}}
\newcommand{\fpp}{\nprv_{\PP}}
\newcommand{\fnp}{\nprv_{\PM}\mnotg }
\newcommand{\fn}{\nprv_{\PM}}
\newcommand{\fp}{\nprv_{\cP}}
\newcommand{\cA}{{\cal A}}
\newcommand{\tensor}{\oplus}
\newcommand{\ga}{ } %change!
\newcommand{\gna}{ }%change!
\newcommand{\vN}{\vec{N}}
\newcommand{\vM}{\vec{M}}
% \newcommand{\PA}{\mid \cP\cup\cA\mid_{\GG}}
\newcommand{\PA}{\mid \cP\mid}
\newcommand{\pix}{\Pi^{\cal X}}
\newcommand{\imm}{>\!\!>}
\newcommand{\nimm}{>\!<}
\newcommand{\IM}{{\cal I}^{-}}
\newcommand{\IP}{{\cal I}^{+}}
\newcommand{\SM}{{\cal S}^{-}}
\newcommand{\SP}{{\cal S}^{+}}


\section{Assumptions}
\newcommand{\al}{\alpha}
\newcommand{\gfald}{\Gamma\prv_{\!\Phi}\ald}
\newcommand{\gfalg}{\Gamma\prv_{\!\Phi}\alg}

Assumptions are contexts which contains all negative occurrences of a 
goal: 
%at the moment we collect together clause assumption and 
%parameter assumptions (to avoid context within context) a' la 
%\emph{Elf}. 
% \beq
% \al(P) & = & \cdot\\
% \al(\Pi x:A.G) & = & x:A\,\al(G)\\
% \al(D\Imp G) & = & D\And\al(G)
% \eneq

Input logical variables are declared in a pool $\Phi$, parameters in 
 $\GG$
 
\begin{Definition}[Assumptions]
\beq
\gfald(Q) & = & \top\\
\gfald(\top) & = & \top\\
\gfald(\bot) & = & \bot\\
\gfald(D_{1}\And D_{2}) & = & \gfald(D_{1})\And \gfald(D_{2})\\
\gfald(D_{1}\oplus D_{2}) & = & \gfald(D_{1})\oplus \gfald(D_{2})\\
\gfald(\PIXA D) & = & \GG\prv_{\Phi,\of{x}{A}}\ald(D)\\
\gfald(Q\If G) & = & \gfalg(G)
\eneq
where the latter is defined as 
\beq
\gfalg(Q) & = & \top\\
\gfalg(\top) & = & \top\\
\gfalg(\bot) & = & \top\\
\gfalg(\vM \eqd \vN) & = & \top\\
\gfalg(\vM \neqd \vN) & = & \top\\
\gfalg(\PIXA G) & = & \GG, \of{x}{A}\prv_{\Phi}\alg(G)\\
\gfalg(D\Imp G) & = & D\And \gfalg(G)\\
\gfalg(G_{1}\And G_{2}) & = & \gfalg(G_{1})\And \gfalg(G_{2})\\
\gfalg(G_{1}\Or G_{2}) & = & \gfalg(G_{1})\Or \gfalg(G_{2})
\eneq
\end{Definition}

\begin{Examplen}
Consider the \texttt{copy} program on $\l$-terms:
\beq
cpapp &:& copy\ (app\ E_{1}E_{2}) (app\ F_{1}F_{2})\If  copy\ (E_{1}F_{1}) 
\If copy\ (E_{2}F_{2})\\
cplam &:& copy\ (lam\ E) (lam\ F)\If \PI {x,y}{ exp} \dspc\ copy\ (x\ y) \Imp copy\ (E\ x)(F\ y)
\eneq
$\ald(cplam) = \of{x}{exp},\of{y}{exp}\prv_{\of{E,F}{exp}} copy\ x\ y$, while 
$\ald(cpapp)$ is equivalent to $\top$ assuming, as we implicitly 
will, $\top$-absorption.
\beq
inall & : & \PI {A,B}{form} inst\ (all\ A) \ B \If \PI {x}{exp} term\ x \Imp\\
& & \quad  (\PI {T}{exp} copy\ x\ T) \Imp inst\ (A\ x)  \ B\\
\ald(inall) & = & \of{x}{exp}\prv_{A,B:form} term\ x\And 
(\PI {T}{exp} copy\ x\ T)\eneq
\end{Examplen}

\ignore{Remark that assumptions  need not to be 
left-linearized: $\al(sublam) = \of{z}{exp}\prv_{ \PI {M} { exp}} sub\ 
(\lx z) \ M \ z$. Note that the latter is still not accounted for
in the complement algorithm, since it contains an embedded parameter.}

We for now restrict to programs with
\bit
\item
flat parameters:\ie parameters can occur is assumption only at the 
top-level, or in the body of lambda:

$$e_x \bnfas x\bnfalt\lx e_x$$

\item
no mutual recursion
\item
no programs with empty assumptions, \ie of the form $\GG\vd\top$, 
with $\GG$ not empty. For example, we exclude for now:
$$ open\ lam\ E \If \PI {x}{exp} open\ (E\ x)$$
\enit

\newcommand{\gf}{\GG\prv_{\!_\Phi}}
\newcommand{\ngf}{\gf\mnot}
\newcommand{\ngfx}{\gf\mnot^x}
\newcommand{\ngfa}{\gf\mnota}

\begin{Definition)[Negation of an Assumption]
\label{def:notalpha}
\beq
\ngfx q(M_1\mdots  M_i\mdots M_m, x,\Nn) & = &
\top \quad \mbox{if } n=m=0\\
&=&
\neg q(M_1\mdots Z\mdots M_m, x,\Nn) \If M_i\neq Z\quad M\in\GG\cup\Phi\\
 & = &
\BAnd_{N\in\mnot M_i}\neg q(M_1\mdots N\mdots M_m, x,\Nn)
        \quad M_i\ \mbox{closed}\\
& = & \top      \quad\mbox{otherwise}\\
\eneq
\beq
\ngfx q(\Mm,x,\Nn) & = &
\BAnd^m_{i=1} \ngfx q(M_1\mdots  M_i\mdots M_m, x,\Nn)\And\mbox{}\\
& = &
\BAnd^n_{j=1} \ngfx q(\Mm, x,N_1\mdots N_j\mdots N_n)\\
\eneq
\beq
\ngfa (Q) & = & \pix (\BAnd_{x\in Q} \ngfx Q)\\
\ngfa (\top) & = & \perp\\
\ngfa(\perp) & = & \top\\
\ngfa ( D_{1}\And D_{2}) & = & \ngfa (D_{1}) \tensor \ngfa (D_{2})\\
\ngfa ( D_{1}\tensor D_{2}) & = & \ngfa (D_{1}) \And \ngfa (D_{2})\\
\ngfa (\PI {x}{A} D) & = & \pix(\ngfa (D))\\
\ngfa(P\If G) & = & \pix(\ngfa(P) \And \neg P \If \mnotg(G)) 
\eneq
\end{Definition}

%\beq\ngfa(def(P)) & = &  \BAnd_{i=1}^{n} \ngfa(P_i\If G_i)\eneq
%\beq
%\al(m_{i}) & = & \al(G_{i})\\
 %\al(def(P)) & = &  \BAnd_{i=1}^{n} \al(m_{i})\\
%\al(\cP) & = & \BAnd_{P\in\Sigma_\cP} \al(def(P)) \eneq 
% 
% 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}

\begin{Examplen}
\beq
\ald(oflam) & = & x: exp\prv_{\! \of{T_1}{tp}} of\ x\ T_{1}\\
\ngfa \al(oflam) & = &
 x: exp\prv_{\! T_1:tp} \Pi T: tp. \neg of\ x\ T \If T\neq\ T_{1}\\
\ignore{\al(sublam) &= & \of{z}{exp}\prv \PI { M_1} { exp} sub\ 
(\lx z) \ M \ z\\
\ngfa \al(sublam) &= & \of{z}{exp}\prv_{\!_\Phi} \PI { M_{1},M_{2}} {exp} \neg 
sub\ (\lx z) \ M_{1} \ M_{2}\If M_{2}\neq \ z \And \mbox{}\\
& & \PI { M_{1},M_{2}} {exp} \neg sub\ (\lx M_{2} x) \ M_{1} \ z\If 
M_{2} x\neq \ z \\}

\ngfa \al(inall) & = & \of{x}{exp}.\, \top
\eneq

Language modulo assumptions: fix a signature and a program $\cP$
\beq
% Q & \bnfas & q\ \vM \mid \neg q\ \vM \\
% G' &\bnfas & \al(\cP)\Imp G \\
% G & \bnfas & Q \mid G_{1}\And G_{2}\mid G_{1}\Or G_{2}\mid
% \PI {X}{A} G\mid \vM \eqd \vN\mid \vM \neqd \vN\\
% D & \bnfas & Q \mid \PI {x}{A} D\mid Q \If G'\mid D_{1}\And D_{2}\mid 
% \top\mid D_{1}\tensor D_{2}\mid \perp 
Q & \bnfas & q\ \vM \mid \neg q\ \vM \\
G & \bnfas & Q \mid  \al(\cP)\Imp G\mid  G_{1}\And G_{2}\mid G_{1}\Or G_{2}\mid
\PI {x}{A} G\mid \vM \eqd \vN\mid \vM \neqd \vN\\
D & \bnfas & Q \mid \PI {x}{A} D\mid Q \If G\mid D_{1}\And D_{2}\mid 
\top\mid D_{1}\tensor D_{2}\mid \perp 
\eneq

\begin{Lemma}[Parameter Context Weakening]
Assume $\ga\sp G$ and $\GG\subset \GG'$: then
 $\GG';\cA\sp G$.
\end{Lemma}
\begin{proof}
 by induction on $\sp$, using Lemma \ref{le:weak}
\end{proof}
\begin{Lemma}[Context Weakening]
Assume $\ga\sp G$  and $\GG\subset \GG', \Phi'\subset\Phi$: then
\ben
\item $\ga,\sp^{\Phi} G$
\item $\GG';\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}
