\bit  %second case
\nitc $\IP$ ends in $\imm\top$
  \itc
  $$\IP=\ianc{}{\ga\spp\perp_q\imm  Q}{\imm \atm}$$
%  But there can be no proof of $\neg Q$ from  $\mnota(\perp)=\top$.
  But by schema satisfaction there can be no formula in the dynamic definition of $q$.
\itc
$$\IP=\ibnc{\ga\spp[\sigma]\vS\eqd \vM}{\ga\spp\s G}{\ga\spp \Pi(q\ \vS\If G)\imm q\ \vM}{\imm\Imp}$$
and
$\IM$ ends in $\gna\sn \mnota (\Pi(q\ \vT\If H))\imm \neg q\
\vM$.
\btab
$\ga\spp\s\vS\eqd \vM$\bs
$\ga\spp \s S_i\eqd M_i$ for every  $1\leq i\leq n$ $ (*)$\bs
%$\ga\spp G$\bs
$\gna\sn\nn{\vT}{\mnotg(G)} \imm \neg q\ \vM$\\
\` By  rule $\mnota\Imp$
\etab
\bit
\item[\subcase] %not^c
\btab
$\gna\sn\mnotr(q\ \vT)\imm \neg q\ \vM$\bv
$\gna\sn \BAnd_{1\leq j\leq n}
\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\  [\ex/Z_j] \Zn\imm \neg q\
\vM$\bv
$\gna\sn \ex\eqd  M_j$\bv
$\perp$\` From  line $(*)$ and   $S_j$ rigid
\etab
\item[\subcase]
\btab
$\gna\sn \BAnd_{1\leq i\leq n,\xrq}\mnotxi (q\ \vT) \imm\neg q \ \vM$ for a fixed $x$\bv
$\gna\sn \mnotxi (q\ \vT )\imm \neg q\ \vM$\bv
$\gna\sn \BAnd_{1\leq j\leq n}\BAnd_{N\in\GG\vd\mnot(T_j)}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}  \neg q\ \zij)\imm\neg  q\ \vM$\\
\br $\mnotxi\Imp$\\
$\ga\sn \ex\eqd M_i$\bv
%$\ga\sn[M_j/Z_j]Z_j\eqd M_j\And x\eqd M_i$
$\perp$\` From  line $(*)$ and   $S_i$ rigid
\etab
\item[\subcase]
\btab
$\gna\sn  \Pi(\neg q\ \vT\If\mnotg(H)) \imm \neg q\ \vM$\bv
$\gna\sn[\theta]\vT\eqd \vM$\bv
$\ga\sn \ex\eqd M_j$ for some $1\leq j\leq n$ \` By complementable clause\\
%$\ga\sn[M_j/Z_j]Z_j\eqd M_j\And x\eqd M_i$
$\perp$\` From  line $(*)$ and  $S_j$ rigid
\etab
\enit
\itc $\IP$ ends in $\imm\Imp$, $\IM$ ends in $\imm\perp$: But there
can be no proof of $\neg Q$ from $\GG\vd\mnota(\perp_q)=\top_q$.
\itc $\IP$ ends in $\imm\Imp$, $\IM$ ends in $\imm\top$:
\bit
\item[\subcase] $\GG=\cdot$ or for all $x\in\dom(\GG)$, for all $i$, $1\leq i\leq n$ it is
not the case that $\xrq$: then $\GG\vd\mnota(\top_q) = \top_q$ and 
an be no proof of $\neg Q$ from $\top_q$.
\item[\subcase] else $\GG\vd\mnota(\top_q) =  \BAnd_{x\in 
 dom(\GG)}(\BAnd_{1\leq i\leq n,xR^{i}q} \mnotr(\top_q))$; fix $x, i$:
\btab
$\ga\sn\mnotr(\top_q) \imm\neg q \ \Mn$\bv
$\ga\sn\BAnd_{1\leq i\leq n} \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\
[\ex/ Z_j] \Zn \imm\neg q \ \Mn$\bv
$\ga\sn \ex\eqd M_j$\bv
$\perp$ \` Above line and rigidity restriction on $S_j$ $(*)$.
\etab
\enit
%\enit
%in $2.1$.
\itc %imm\tensor
$$\IP= \ibnc{\ga\sp D_{1}\imm Q}{\ga\sp D_{2}\imm Q}{\ga\sp (D_{1}\tensor
  D_{2})\imm Q}{\imm\tensor}$$
%and $\IM$ ends in $\gna\sn\mnota (D'_{1}\tensor  D'_{2})\imm \neg Q$:
and  $\IM$ ends in $\ga\vd\mnota(D')\imm\neg Q$:
\btab
 $\ga\spp  D_1\imm Q$ \bs
$\perp$\bi $2.2$
\etab
\itc  %And 1
$$\IP= \ianc{\ga\sp D_{1}\imm Q}{\ga\sp (D_{1}\And
  D_{2})\imm Q}{\imm\And_1}$$
and $\IM$ ends in $\ga\vd\mnota(D')\imm\neg Q$:
\btab
 $\ga\spp  D_1\imm Q$ \bs
$\perp$\bi $2.2$
\etab
\itc %And 2
$$\IP= \ianc{\ga\sp D_{2}\imm Q}{\ga\sp (D_{1}\And
  D_{2})\imm Q}{\imm\And_2}$$
and $\IM$ ends in $\ga\vd\mnota(D')\imm\neg Q$:
Symmetric to the above.
\itc
$$\IM= \ianc{\ga\sp \mnota(D'_{1})\imm \neg Q}{\ga\sp\mnota (D'_{1}\tensor
  D'_{2})\imm\neg Q}{\imm\And_1}$$
and $\IM$ ends in $\ga\vd D\imm Q$. By IH $2.2$
\itc
$$\IM= \ianc{\ga\sp \mnota(D'_{2})\imm\neg  Q}{\ga\sp\mnota (D'_{1}\tensor
  D'_{2})\imm\neg Q}{\imm\And_2}$$
and $\IM$ ends in $\ga\vd D\imm Q$. By IH $2.2$.
\itc
$$\IM= \ibnc{\ga\sp \mnota(D'_{1})\imm\neg Q}{\ga\sp \mnota(D'_{2})\imm
  \neg Q}{\ga\sp \mnota(D'_{1}\And D'_{2})\imm\neg Q}{\imm\tensor}$$
and $\IM$ ends in $\ga\vd D\imm Q$. By IH $2.2$.
\enit

%%%%%%%%%%