\begin{Theorem}[Termination]
\label{thm:termination}
Assume $\cP$ is terminating. Then for every  goal either $\ga\sp
G$ or $ \gna\fp G$.
\end{Theorem}

\begin{proof}
\renewcommand{\ga}{\Gamma;[\s]\cD }
\renewcommand{\gna}{ \Gamma;[\q]\cD }
We generalize this to: let $\s$ and $\q$ be well-typed
substitutions such that $\GG\vd\s$, $\GG\vd\q$ and
$x\not\in (dom(\s)\cup dom(\q))$; let $D\in \defp(q,\cP\And\cD)$:
\ben
\item
Either there is a   $\s$ such that $\SM \semic   \ga\sp [\s] G$ or for all
 $\q$ $\SP \semic  \gna\fp[\q] G$.
\item
Either there is a   $\s$ such that $\IM \semic  \ga\sp [\s]  D \imm [\s] Q$
or  for all  $\q$, $\IP \semic  \gna\fp [\q]  \imm  [\q] Q$.
\enen
We proceed by mutual induction on the goal ordering induced by $\cP$
terminating and on the structure of   $D\in \defp(q,\cP\And\cD)$:
\bit
\itc $D=\perp=[\s]\perp$. Then
$$\ianc{}{\ga\sp\perp_Q\imm [\s] Q}{\imm\perp}$$
Hence  the claim.
\bmeta No case for $\top$\emeta
% \itc $ D=\q\top=\top\ \foq$. Then
% $$\ianc{}{\foq\gna\fp\top_q\imm\q Q}{\notimm\top}$$
% Hence by weakening the thesis.
\itc $D=D_1\If G_1$. Hence for all $\rho $ $[\rho] G_1\less [\rho] D_1$ by termination.
By the first IH either $\SM \semic   \ga\sp [\s] G_1$ or $\foq\SP \semic \gna\fp[\q]
G_1$; by the second IH $\ga\sp[\s] D_1\imm[\s] Q$ or $\gna\fp[\q] D_1\imm[\q] D_1$:
\ben
\item %1.
\btab
 $\SM \semic   \ga\sp [\s] G_1$\ba
$\ga\sp[\s] D_1\imm[\s] Q$\ba
$\ga\sp [\s] D_1 \If [\s] G_1\imm [\s] Q $\br $\imm\Imp$\\
$\ga\sp [\s](D_1\If G_1)\imm [\s] Q $\bsu\\
Hence the claim.
\etab
\item %2.
\btab
 $\SP \semic    \foq\gna\fp [\q] G_1$\ba
$\ga\sp[\s] D_1\imm [\s] Q$\ba
$\foq\gna\fp[\q] D_1 \If [\q] G_1\imm  [\q] Q $\br\\
$\foq\gna\fp[\q] ( D_1 \If G_1)\imm  [\q] Q $\` By subst.\\
Hence the claim.
\etab
\item %3.
\btab
$\ga\sp [\s] G_1$\ba
$\foq\ga\fp[\q] D_1\imm[\q] Q$\ba
$\foq\gna\fp [\q] D_1 \If [\q] G_1\imm [\q] Q$\br\\
$\foq\gna\fp [\q]( D_1 \If G_1)\imm [\q] Q$\bsu\\
Hence the claim.
\etab
\item %4 
\btab
$\foq\gna\fp [\q] G_1$\ba
$\foq\gna\fp[\q] D_1\imm Q$\ba
$\foq\gna\fp [\q] D_1 \If [\q] G_1\imm [\q] Q$\br\\
$\foq\gna\fp [\q]( D_1 \If G)\imm [\q] Q$\bsu\\
Hence the claim.
\etab
\enen
\itc %imm\tensor
$D=D_1\tensor D_2$. By the second IH $\ga\sp[\s] D_1\imm[\s] Q$ or for all $\gna\fp [\q] D_1
\imm  [\q] Q$ and $\ga\sp
[\s] D_2\imm[\s] Q$ or for all $\gna\fp [\q] D_2 \imm  [\q] Q$:
\ben
\item %1
\btab
 $\ga\sp [\s] D_1\imm[\s] Q$ \ba
$\ga\sp [\s] D_2\imm[\s] Q$\ba
$\ga\sp [\s] D_1\tensor [\s] D_2\imm [\s] Q$\br $\imm\tensor$\\
$\ga\sp [\s](D_1\tensor D_2)\imm [\s] Q$\bsu\\
\hence
\etab
\item %2
\btab
 $\ga\sp [\s] D_1\imm [\s] Q$ \ba
$\foq\gna\fp [\q] D_2 \imm [\q] Q$\ba
$\foq\gna\fp [\q] D_1\tensor [\q] D_2 \imm [\q] Q$\br \\
$\foq\gna\fp [\q] (D_1\tensor  D_2) \imm [\q] Q$\bsu\\
\hence
\etab
\item %3
\btab
 $\ga\sp [\s] D_2\imm [\s] Q$ \ba
$\foq\gna\fp[\q]  D_1 \imm[\q]  Q$\ba
$\foq\gna\fp [\q] D_1\tensor [\q] D_2 \imm[\q]  Q$\br \\
$\foq\gna\fp [\q] (D_1\tensor  D_2) \imm[\q]  Q$\bsu \\
\hence
\etab
\item %4
\btab
$\foq\gna\fp [\q] D_1 \imm [\q] Q$\ba
$\foq\gna\fp [\q] D_2 \imm  [\q] Q$\ba
$\foq\gna\fp [\q] D_1\tensor [\q] D_2 \imm [\q] Q$\br \\
$\foq\gna\fp [\q] (D_1\tensor  D_2) \imm [\q] Q$\bsu \\
\hence
\etab
\enen
\itc%And
$D=D_1\And D_2$. By the second IH $\ga\sp [\s] D_1\imm [\s] Q$ or $\foq\gna\fp [\q] D_1 \imm [\q] Q$ and $\ga\sp\s
D_2\imm[\s] Q$ or $\foq\gna\fp[\q]  D_2 \imm [\q] Q$:
\ben
\item %1
\btab
$\ga\sp [\s] D_1\imm[\s] Q$ \ba
$\ga\sp [\s] D_2\imm[\s] Q$\ba
$\ga\sp[\s] (D_1\And D_2)\imm [\s] Q$\br $\And$\\
\hence
\etab
\item %2
\btab
 $\ga\sp[\s] D_1\imm [\s] Q$ \ba
$\foq\gna\fp  [\q] D_2 \imm [\q]  Q$\ba
$\ga\sp [\s] (D_1\And D_2)\imm[\s] Q$\br\\
\hence
\etab
\item %3
\btab
 $\ga\sp [\s] D_2\imm[\s] Q$ \ba
$\foq\gna\fp[\q]  D_1 \imm [\q] Q$\ba
$\ga\sp [\s](D_1\And D_2)\imm [\s] Q$\br\\
\hence
\etab
\item %4
\btab
$\foq\gna\fp[\q]  D_1 \imm  [\q] Q$\ba
$\foq\gna\fp[\q]  D_2 \imm  [\q] Q$\ba
%$\foq\gna\fp  [\q] D_1 \And [\q] D_2 \imm [\q] Q$\br\\
$\foq\gna\fp[\q]( D_1\And D_2) \imm  [\q] Q$\br\\
\hence
\etab
\enen
\itc %\Pi imm
$D=\PIXA D'$. By the second IH, for some  $\GG\vd t\hastype A$, $\GG;[\s,t/x]\cD\sp
 [\s,t/x] D'\imm[\s,t/x ]Q$ or for all $\GG\vd n\hastype A$
 $\foq\GG;[\q,n/x]\cD\fp [\q,n/x] D'\imm[\q,n/x] Q$:
\ben
\item %1
\btab
$\GG;[\s,t/x]\cD\sp[ \s,t/x] D'\imm[\s,t/x] Q$\ba
$\GG;[\s,t/x]\cD\sp[\s](\PIXA D')\imm [\s,t/x] Q$\br $\imm\Pi$\\
$\ga\sp[\s](\PIXA D')\imm [\s] Q$\` Trivially\\
\hence
\etab
\item %2
\btab
$\foq\GG;[\q,n/x]\cD\fp [\q,n/x] D'\imm [\q,n/x] Q$\ba
$\foq\GG;[\q,n/x]\cD\fp [\q](\PI{x}{A} D')\imm [\q,n/x] Q$\br\\
$\foq\gna\fp [\q] (\PI{x}{A} D')\imm [\q] Q$\`Trivially\\
\hence
\etab
\enen
%start \vd G
\itc
By the second IH, for $D\in \defp(q,\cP\And\cD)$,
 $\ga\sp [\s] D \imm[\s] Q$ or $\foq\gna\fp [\q] D \imm [\q] Q$:
\ben
\item %1
\btab
$\ga\sp [\s] D \imm[\s] Q$\ba
$\ga\sp[\s] Q$\br\\
\hence
\etab
\item %2
\btab
$\foq\gna\fp [\q] D \imm[\q]  Q$\ba
$\foq\gna\fp[\q] Q$\br\\
\hence
\etab
\enen
\itc
By the first IH $\ga\sp[\s] G_1$ or $\foq\gna\fp[\q] G_1 $ and $\ga\sp[\s]  G_2$ or
 $\foq\gna\fp[\q] G_2 $:
\ben
\item % 1
\btab
$\ga\sp[\s]  G_1$\ba
$\ga\sp[\s]  G_2$\ba
$\ga\sp[\s]  (G_1\And G_2)$\br\\
\hence
\etab
\item %2
\btab
$\ga\sp[\s]  G_1$\ba
$\foq\gna\fp[\q] G_2 $\ba
$\foq\gna\fp[\q] (G_1\And G_2 )$\br\\
\hence
\etab
\item %3
\btab
$\ga\sp[\s]  G_2$\ba
$\foq\gna\fp[\q] G_1 $\ba
$\foq\gna\fp[\q] (G_1\And G_2) $\br\\
\hence
\etab
\item %4
\btab
$\foq\gna\fp[\q] G_1 $\ba
$\foq\gna\fp[\q] G_2 $\ba
$\foq\gna\fp[\q] (G_1\And G_2) $\br\\
\hence
\etab
\enen
\itc %or
By the first IH $\ga\sp[\s]  G_1$ or $\foq\gna\fp[\q] G_1 $ and $\ga\sp[\s]  G_2$ or
 $\foq\gna\fp[\q] G_2 $:
\ben
\item % 1
\btab
$\ga\sp[\s]  G_1$\ba
$\ga\sp[\s]  G_2$\ba
$\ga\sp[\s]  (G_1\Or G_2)$\br\\
\hence
\etab
\item %2
\btab
$\ga\sp[\s]  G_1$\ba
$\foq\gna\fp[\q] G_2 $\ba
$\ga\sp[\s]  (G_2\Or G_1)$\br\\
\hence
\etab
\item %3
\btab
$\ga\sp[\s]  G_2$\ba
$\foq\gna\fp[\q] G_1 $\ba
$\ga\sp[\s]   (G_2\Or G_1)$\br\\
\hence
\etab
\item %4
\btab
$\foq\gna\fp[\q]  G_1 $\ba
$\foq\gna\fp[\q] G_2 $\ba
$\foq\gna\fp[\q] (G_1\Or G_2) $\br\\
\hence
\etab
\enen
\itc %exa
By the first IH for some $\GG\vd t\hastype A$, $\GG;[\s,t/x]\cD\sp[\s ,t/x] G$
or for all $n$  $\GG\vd n\hastype A$, $\foq\GG;[\q,n/x]\cD\fp[\q,n/x] G $:
\ben
\item %1
\btab
$\GG\vd t\hastype A$\bh
$\GG;[\s,t/x]\cD\sp[\s ,t/x]G$\ba
$\GG;[\s,t/x]\cD\sp[\s ](\exa G)$\br\\
$\ga\sp[\s](\exa G)$\`Trivially\\
\hence
\etab
\item 
\btab
for all $n$  $\GG\vd n\hastype A$\bh
$\foq\GG;[\q,n/x]\cD\fp[\q,n/x] G$\ba
$\foq\GG;[\q,n/x]\cD\fp[\q](\exa G)$\br\\
$\foq\gna\fp[\q](\exa G)$\`Trivially\\
\hence
\etab
\enen
\itc %PIXA G
By the first IH, for a new parameter $y$, $(\GG,y\oftp A);[\s,y/x]\cD\sp[\s,y/x] G$
or  $\foq(\GG,y\oftp A);[\q,y/x]\cD\fp[\q,y/x] G $:
\ben
\item %1
\btab
$(\GG,y\oftp A);[\s,y/x]\cD\sp[\s,y/x] G$\ba
$\GG;[\s,y/x]\cD\sp[\s] (\PIXA G)$\br\\
$\ga\sp[\s](\PIXA G)$\`Trivially\\
\hence
\etab
\item %2 
\btab
$\foq(\GG,y\oftp A);[\q,y/x]\cD\fp[\q,y/x] G$\ba
$\foq\GG;[\q,y/x]\cD\fp\q(\PIXA G)$\br\\
$\foq\gna\fp[\q](\PIXA G)$\`Trivially\\ 
\hence
\etab
\enen
\itc %\Imp
By the first IH, $\GG;(\s\cD\And[\s] D)\sp[\s] G$ or $\foq\GG;([\q]\cD\And[\q]
D)\fp[\q] G$:
\ben
\item %1
\btab
 $\GG;(\s\cD\And[\s] D)\sp[\s] G$\ba
$\ga\sp[\s] D\Imp [\s] G$\br\\
$\ga\sp[\s]   (D\Imp G)$\bsu\\
\hence
\etab
\item % 2
\btab
 $\foq\GG;([\q]\cD\And[\q] D)\fp[\q] G$\ba
$\foq\gna\fp[\q] D\Imp[\q] G$\br\\
$\foq\gna\fp[\q](D\Imp G)$\bsu\\
\hence
\etab
\enen 
\itc The (dis)equality case follows immediately from the decidability of the $\eqd,\neqd $
 rules.
% to be detailed later in the unification logic judgment.
\enit% main bit
\end{proof}

