$Augmentation without indeces

\newcommand{\vYx}{\vec{Y\ \vx}}
\newcommand{\vEx}{\vec{E\ \vx}}
\begin{Definition}[Unary augmentation]
  For a program $\cP$ over a signature $\Sigma$, let $p$ be predicate
  defined recursively by structural induction \beq
  m &:& p\ (\l \vx . (a\ (\vYx) \ (\vEx)) \\
  & &\If  \vec{p\ (\l \vx .(Y \vx))} \\
  & &  \If \vec{(\Pi z : A.\ p\ (\l \vx.(E\ \vx\ z)))}\\
& & \If G \eneq
 \bit
\item
 $a\in \Sigma\cup\vx$
% \item
% $m$ is a second-order $\Pi$-allowed recursive clause thru $q$ in $\cP$:
\item
 $\vY : \vec{C}$ is a vector of first-order variables 
\item
 $\vec{E} : \vec{B}$ is a vector of second-order variables \ie $\omicron(B_{i}) = 2$
\item
$G$ is about predicates defined in a lower stratum then $def(p)$
\item
$A_B_{i}\leq \vec{B}$
\enit
Then define 
\beq
aug(m) &:& p\ (\l \vx . (a\ (\vYx) \ (\vEx)) \\ 
& &\If \vec{p\ (\l \vx .(Y \vx))} \\
& & \If \vec{(\Pi z : A.\  \neg p\ (\l \vx.z)\Imp p\ (\l \vx.(E\ \vx\ z)))} \\
 & & \If G
\eneq
Define $aug(\cP)$ as the augmentation of every clause in $\cP$.
\end{Definition}

% start of proofr without indeces

\begin{proof}
We give a proof by induction  (course-of-value and structural) on the 
lexicographically ordered pair $\la S(p),M\ra$  over $\Sigma$
% %  the inductive hypothesis being\ldots
% :
\bit
\item
 Base of main induction: $p$ is defined at stratum 1: we show 
 $\GG^{+}\prv p\ M$ or $\GG^{-}\prv \neg p\ M$ by induction over $M$: 
 first observe that $p$ and $\neg p$ can depend only on its recursive 
 call for n-ary constructors:

 \bit
\item
Base: projection from $\xn$:
\ben
\item
 consider $p\ (\l\vx.x_{i})$; if $p\ 
(\l\vx.x_{i})\not\in heads(def(p))$, then there is is a clause in $dp$ 
of the form $\neg p\ (\l\vx.x_{i})$.  Thus $1.$ holds trivially.  
Otherwise $p\ (\l\vx.x)$ must match a fact, since $p$ cannot 
depend neither on itself or other predicates. Hence $\prv p\ 
(\l\vx.x)$ and thus $1.$
\item
 Suppose $p\ (\l\vx.x)\And\neg p\ (\l\vx.x)$ hold: then 
 $(\l\vx.x) \cap Not(\l\vx.x) \not=\eset$; but this is 
 impossible by the Partition lemma \ref{lemma:part} hence $2.$.  
%  Simmetrically for $\neg p\ (\l\vx.x)$ 
 Analogously for a unary 
 constructor.  
\enen
\item
Step: $n$-ary constructor:
 \ben
 \item % Exh
 the induction hypothesis is (pushing in the universals):
\beq
( \vec{p\ (\l \vx .(Y \vx))} 
\And \GG^{+} \Imp \vec{p\ (\l \vx.(E\ \vx\ 
z)))} \And\\
 (\vec{\neg p\ (\l \vx .(Y \vx)) }
\Or \GG^{-} \Imp\vec{\neg p\ (\l \vx.(E\ \vx\ 
z))})
\eneq
By cases:
\[
\begin{array}{ll}
\vec{p\ (\l \vx .(Y \vx))} \And 
\GG^{+} \Imp \vec{p\ (\l \vx.(E\ \vx\ z))}
& \mbox{first case from IH}\\
p\ (\l \vx . (a\ (\Ym \vx) \ (\Ep \vx)) 
& \mbox{by inversion on $m$}\\
\GG^{+}\Imp p\ (\l \vx . (a\ (\Ym \vx) \ (\Ep \vx)) \Or 
\GG^{-}\imp\neg p\ (\l \vx . (a\ (\Ym \vx) \ (\Ep \vx))
& \mbox{by weakening}
\skl
(\vec{\neg p\ (\l \vx .(Y \vx)) }
\Or \GG^{-} \Imp \vec{\neg p\ (\l \vx.(E\ \vx\ 
z))}& \mbox{second case from IH}\\
\neg p\ (\l \vx . (a\ (\Ym \vx) \ (\Ep \vx)) 
& \mbox{by inversion on $m$}\\
\GG^{+}\Imp p\ (\l \vx . (a\ (\Ym \vx) \ (\Ep \vx)) \Or 
\GG^{-}\imp\neg p\ (\l \vx . (a\ (\Ym \vx) \ (\Ep \vx))
& \mbox{by weakening}
\end{array}
\]

\item % Dsj
 the induction hypothesis is (pushing in the universals):
\beq
\neg ( \vec{p\ (\l \vx .(Y \vx))} 
\And \GG^{+} \Imp \vec{p\ (\l \vx.(E\ \vx\ z))}) \And\\
(  \vec{\neg p\ (\l \vx .(Y \vx))} 
\Or \GG^{-} \Imp \vec{\neg p\ (\l \vx.(E\ \vx\ z))})
\eneq

Again, suppose the negation of the thesis holds: but the result of applying 
inversion on $\neg m$ contradicts the IH.

\benen % end of 1.2. for S=1.

\enit 

\item
Step for $S(p)$: suppose $p$ is defined at stratum $i$ and every 
predicate in $G$ is defined at stratum $j < i$: proceed as above, with 
the difference that if $p\ (\l \xn .  (a\ (\Ym \xn) \ (\Ep \xn))$ 
matches a clause $p\ N \If G$, we may use the induction hypothesis on 
$G$, since every predicate in the latter is defined al a lower stratum 
or is a recursive call on a smaller term; Hence infer $ \GG^+ (G) \prv 
G$ or $\GG^{-}(G) \prv\neg G$ and thus the thesis.
\enit
\end{proof}

% Augmentation with indices

\begin{Definition}[Unary augmentation]
  For a program $\cP$ over a signature $\Sigma$, let $p$ be predicate
  defined recursively by structural induction \beq
  m &:& p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn)) \\
  & &\If \BAnd \limits^m_{j = 1} p\ (\l \xn .(\ol{Y_{j}} \xn)) \\
  & & \If \BAnd \limits^p_{i = 1}(\Pi z_{i} : A_{i}.\\Imp p\ (\l \xn.(E\ \xn\ z_{i}))) \\
& & \If G \eneq
 \bit
\item
 $a\in \Sigma\cup\xn$
% \item
% $m$ is a second-order $\Pi$-allowed recursive clause thru $q$ in $\cP$:
\item
 $\Ym : \ol{C_{m}}$ is a vector of first-order variables 
\item
 $\Ep : \ol{B_{p}}$ is a vector of second-order variables \ie $\omicron(B_{i}) = 2$
\item
$G$ is about predicates defined in a lower stratum then $def(p)$
\item
$A_{i}\leq B_{i},\ i\in 1..p$.
\enit
Then define 
\beq
aug(m) &:& p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn)) \\ 
& &\If \BAnd \limits^m_{j = 1} p\ (\l \xn .(\ol{Y_{j}} \xn)) \\
& & \If \BAnd \limits^p_{i = 1}(\Pi z_{i} : A_{i}.\  \neg p\ (\l \xn.z_{i})
 \Imp p\ (\l \xn.(E\ \xn\ z_{i}))) \\
 & & \If G
\eneq
Define $aug(\cP)$ as the augmentation of every clause in $\cP$.
\end{Definition}

% proof with indeces
\begin{proof}
We give a proof by induction  (course-of-value and structural) on the 
lexicographically ordered pair $\la S(p),M\ra$  over $\Sigma$
% %  the inductive hypothesis being\ldots
% :
\bit
\item
 Base of main induction: $p$ is defined at stratum 1: we show 
 $\GG^{+}\prv p\ M$ or $\GG^{-}\prv \neg p\ M$ by induction over $M$: 
 first observe that $p$ and $\neg p$ can depend only on its recursive 
 call for n-ary constructors:

 \bit
\item
Base: projection from $\xn$:
\ben
\item
 consider $p\ (\l\xn.x_{i})$; if $p\ 
(\l\xn.x_{i})\not\in heads(def(p))$, then there is is a clause in $dp$ 
of the form $\neg p\ (\l\xn.x_{i})$.  Thus $1.$ holds trivially.  
Otherwise $p\ (\l\xn.x_{i})$ must match a fact, since $p$ cannot 
depend neither on itself or other predicates. Hence $\prv p\ 
(\l\xn.x_{i})$ and thus $1.$
\item
 Suppose $p\ (\l\xn.x_{i})\And\neg p\ (\l\xn.x_{i})$ hold: then 
 $(\l\xn.x_{i}) \cap Not(\l\xn.x_{i}) \not=\eset$; but this is 
 impossible by the Partition lemma \ref{lemma:part} hence $2.$.  
%  Simmetrically for $\neg p\ (\l\xn.x_{i})$ 
 Analogously for a unary 
 constructor.  
\enen
\item
Step: $n$-ary constructor:
 \ben
 \item % Exh
 the induction hypothesis is (pushing in the universals):
\beq
( \BAnd \limits^m_{j = 1} p\ (\l \xn .(\ol{Y_{j}} \xn)) 
\And \GG^{+}(p) \Imp \BAnd \limits^p_{i = 1} p\ (\l \xn.(E\ \xn\ 
z_{i}))) \Or\\
( \BOr \limits^m_{j = 1} \neg p\ (\l \xn .(\ol{Y_{j}} \xn)) 
\Or \GG^{-}(p) \Imp \BOr \limits^p_{i = 1} \neg p\ (\l \xn.(E\ \xn\ 
z_{i})))
\eneq
By cases:
\[
\begin{array}{ll}
\BAnd \limits^m_{j = 1} p\ (\l \xn .(\ol{Y_{j}} \xn)) \And 
\GG^{+} \Imp \BAnd \limits^p_{i = 1} p\ (\l \xn.(E\ \xn\ z_{i}))
& \mbox{first case from IH}\\
p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn)) 
& \mbox{by inversion on $m$}\\
\GG^{+}\Imp p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn)) \Or 
\GG^{-}\imp\neg p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn))
& \mbox{by weakening}
\skl
\BOr \limits^m_{j = 1} \neg p\ (\l \xn .(\ol{Y_{j}} \xn)) 
\Or \GG^{-}(p) \Imp \BOr \limits^p_{i = 1} \neg p\ (\l \xn.(E\ \xn\ 
z_{i}))& \mbox{second case from IH}\\
\neg p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn)) 
& \mbox{by inversion on $m$}\\
\GG^{+}\Imp p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn)) \Or 
\GG^{-}\imp\neg p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn))
& \mbox{by weakening}
\end{array}
\]
Similarly for the other case

\item % Dsj
 the induction hypothesis is (pushing in the universals):
\beq
\neg ( \BAnd \limits^m_{j = 1} p\ (\l \xn .(\ol{Y_{j}} \xn)) 
\And \GG^{+}(p) \Imp \BAnd \limits^p_{i = 1} p\ (\l \xn.(E\ \xn\ 
z_{i}))) \And\\
( \BOr \limits^m_{j = 1} \neg p\ (\l \xn .(\ol{Y_{j}} \xn)) 
\Or \GG^{-}(p) \Imp \BOr \limits^p_{i = 1} \neg p\ (\l \xn.(E\ \xn\ 
z_{i})))
\eneq

Again, suppose the negation of the thesis holds: but the result of applying 
inversion on $\neg m$ contradicts the IH.

\benen % end of 1.2. for S=1.

\enit

\item
Step of the main induction: suppose $p$ is defined at stratum $i$ and 
every predicate in $G$ is defined at stratum $j < i$: proceed as in 
the base of the main induction, with the difference that if $p\ (\l 
\xn .  (a\ (\Ym \xn) \ (\Ep \xn))$ matches a clause $p\ N \If G$ with 
$G$ failing, use the induction hypothesis on $G$ to infer$\neg G$ and 
hence $\neg p\ (\l \xn .  (a\ (\Ym \xn) \ (\Ep \xn))$.  \enit
\end{proof}



\begin{Definition}[Dependence$P dep Q in D$]
Given a program $\cP$, we say that $P$ 
\emph{depends positively [negatively] on $Q$ in $\cP$} 
iff
\begin{itemize}
\item $P$ depends positively on $Q$ in $P \If (G \If Q)$
\item $P$ depends negatively on $Q$ in $P \If (Q \Imp G)$

 \item $P$depends positively [negatively] on 
$Q$ in $(P \If\forall x :A.G )$ if $P$ depends 
positively [negatively] on $Q$ in $P \If G $ 
\item $P$ depends 
positivel y[negatively] in on $Q$ in $P \If(G_{1} \Imp G_{2})$ iff $P$ 
depends positively [negatively] on $Q$ in $P\If G_{2} $ or $P$ 
depends negatively [positively] on $Q$ in $P \If G_{1}$ 
\end{itemize}
\end{Definition}

\begin{Definition}[Head\footnote{Put elsewhere}]
 For every $G$ define $hd(\Pi\Xn:G_{n}.a) =a$
\end{Definition}

% \begin{Definition}[$DG(\cP)$]
% Let $\Sigma_{\cP}$ be a signature for a program $\cP$. The 
% \emph{dependency graph} $DG(\cP)$ is the dag whose nodes are the 
% predicated declared in the signature and whose arcs are twofold: for 
% every clause $D \equiv P \If G$ there is an $\If$-arc $P \If Q$ if 
% $Q= head(G)$. Thre is an 
% Let $_{*}$  denotes the trnasitive closure of the two relations. We say 
% that a clause $P\If G$ is \emph{recursive } if there is a 
% path $P \If^{*} P$: it is \emph{implicationally [left] recursive} if there is a 
% path $P \Imp^{*} P$
% \end{Definition}

Let $dep^{*}_{\pm}$ be the transitive closure of the above dependency 
relations (to accommodate simple and mutual recursion):

\begin{Definition}[Dependence]
We say that a clause $P\If G$ is \emph{recursive in $Q$} if $P\ 
dep^{*}_{+} $ on $Q$ in $\cP$: it is \emph{implicationally [left] 
recursive in $Q$} if $P\ dep^{*}_{-} $ on $Q$ in $\cP$
\end{Definition}

\begin{Definition}[Allowedness]
A program is \emph{allowed} if every left-recursive clause is 
$\Pi$-allowed. 
%  A left-recursive clause $P\If G$ is 
% \emph{$\Pi$-allowed} iff for every $Q$ such that $P\ dep^{*}_{-} Q$, 
% $Q$ contains an occurennce of an e.u.\ variable.

%  A non-horn recursive clause $P\If G$ is \emph{$\Pi$-allowed} iff for every 
%  secon-order variable $E$ in $P$ and for every $Q$ such that $P\ 
%  dep^{*}_{+} \ Q$, $E$ occurs universally quantified in $Q$.
 
  A 
%   non-horn 
  self-recursive clause $P\If G$ is \emph{$\Pi$-allowed} iff for every 
 second-order variable $E$ in $P$ $E$ occurs positively in the scope 
 of an universal quantifier in $G$.
% \smallskip
% Choose one of the following two
% \begin{Definition}[$\Pi$-Allowedness]
%  A left-recursive clause $P\If G$ is \emph{$\Pi$-allowed} iff for 
%  every second-order variable $E$ in $P$, $E$ occurs 
%  positively\footnote{define somewhere} in the scope of an universal 
%  quantifier in $G$.
%  \end{Definition}
 
  self-recursive clause $P\If G$ is \emph{$\Pi$-allowed} iff $\Delta 
  \prv G <_{\Pi} A$ in the following judgment \beq \frac{\Delta\prv 
  G_{2}<_{\Pi} P}{\Delta\prv G_{1}\Imp G_{2} <_{\Pi} }P{<_{\Pi}-\Imp} 
  & \frac{\Delta, \Pi x: A\prv [x/a]G<_{\Pi} P}{\Delta\prv \Pi x: A. 
  G<_{\Pi} P}{<_{\Pi}-\Pi}\\
    \frac{\Delta \prv M < N}{\Delta \prv p\ M <_{\Pi} p\ N}{<_{\Pi}-P}
\eneq
where $<$ is the adaptation of \ho subterm ordering \cite{EP96,Vir96}
  \end{Definition}


Thus \texttt{impI} is not $\Pi$-allowed, whereas clolam is.


% \begin{Definition}[Unary augmentation]\footnote{may bedefined 
% iteratively on every \ho E}
% Let $m : p (c E_{n} M_{m}) \If \Pi \Xn : a_{n}. G[(E_{n}\Xn)]$ be a 
% second-order $\Pi$-allowed recursive clause in $q$, where 
% \bit
% \item $E_{i} : (a_{i} \Imp A_{i}^{'}$\footnote{fix this}
% \item $\Gamma{a_{i} \leq \GG(E_{i})$
% \item $eu(p) = eu(q)
% \item $ord(A_{i}) = 2$ ??
% \item $M_{j}$ are \fo
% \enit  
% Then define $aug(m)$ as 
% $p (c E_{n} M_{m}) \If (\Pi \Xn : A_{n}.  \neg (q \Xn) \Imp G[(E_{n}\Xn)])$
% \end{Definition}


We define unary augmentation iteratively on every second-order 
variable $E$.

\begin{Definition}[Unary augmentation]
For  a program $\cP$, let $m : p (M[E]) \If (\Pi x : A. G \leftarrow 
q(N[E x])$ be a 
second-order $\Pi$-allowed recursive clause on $q$ in $\cP$, where 
\bit
\item $\omicron(G) = 1$, \ie G is not implicational
\item $E : A$ s.t.\ $\omicron(A) = 2$
\item $q : B \Imp type$ s.t.\ $A \leq B$
%\item $eu(p) = eu(q)
\enit  
Then define $aug_{E}(m) : p (M[E]) \If (\Pi x : A.  \neg (q(N[ x]) \Imp (G\leftarrow 
q(N[E x]))$
Denote with $aug(m)$ the augmentation of $m$ for every $E$ in $m$. 
Define $aug(\cP)$ as the augmentation of every clause in $\cP$.
\end{Definition}
\begin{Definition}[Augmentation]
For  a program $\cP$, let $m : p ([E_{n}]) \If (\Pi \xn : A_{n}. G \leftarrow 
q[E_{n} \xn])$ be a 
second-order $\Pi$-allowed recursive clause on $q$ in $\cP$, where 
\bit
\item $\omicron(G) = 1$, \ie G is not implicational
\item $E_{i} : A_{i}$ s.t.\ $\omicron(E_{i}) = 2$
\item $q : B_{n} \Imp type$ s.t.\ $A \leq B_{n}$
%\item $eu(p) = eu(q)
\enit 
Then define $aug(m) : p ([E_{n}]) \If (Not(\Pi \xn : A_{n}.  
(q \xn)) \Imp (G\leftarrow q[E_{n} \xn]))$. Define $aug(\cP)$ as 
the augmentation of every clause in $\cP$
\end{Definition}