\bit  %bit of one
\itc
$$\SP=\ianc{\ga\spp \defp(q,\PP\And\cD)\imm Q}{\ga\spp Q}{ \vd  {\rm atm}}$$
and $\SM$ ends in $\gna\snp (Q)$:
\btab
$\ga\spp  \defp(q,\PP\And\cD)\imm Q$\bs
%$\ga\spp D\imm Q$ for $D\inn  \defp(q,\PP\And\cD)$\bs
$\gna\sn\neg Q$\br $\mnotg\atm$\\
%$\gna\sn \defp(\neg q,\cP\cD)\imm \neg Q$\bv
$\ga\sn \defp(\neg q,\PP\And\cD)\imm \neg Q$ \bv
\etab
\bit
\item[\subcase]
\btab
$\ga\sn \mnotd(\defp(q,\cP))$\` By definition\\
$\perp$\bi $2.i$, $i\in\{1,3\}$ according to $D$ static or dynamic
\etab
\item[\subcase]
\btab
$\ga\sn \mnota(\defp(q,\cD))$\` By definition\\
$\perp$\bi $2.i$, $i\in\{2,4\}$ according to $D$ static or dynamic 
\etab
\enit
%And
\itc
$$\SP=\ibnc{\ga\spp G_1}{\ga\spp G_{2}}{\ga\spp G_{1}\And G_{2}}
{ \vd\And}$$
and $\SM$ ends in $\gna\snp (G_1\And G_2)$
\btab
 $\ga\spp G_1$\bs
 $\ga\spp G_2$\bs
 $\gna\sn\mnotg(G_1)\Or\mnotg(G_2)$\br $\mnotg\And$
\etab
\bit
\item[\subcase]
\btab
$\gna\snp(G_1)$\bv
$\perp$\bi $1$
\etab
\item[\subcase]
\btab
$\gna\snp(G_2)$\bv
$\perp$\bi $1$
\etab
\enit
%Or 1
\itc
$$\SP=\ianc{\ga\spp G_1}{\ga\spp G_{1}\Or G_{2}}
{ \vd\Or}$$
and $\SM$ ends in $\gna\snp (G_1\Or G_2)$
\btab
 $\ga\spp G_1$\bs
$\gna\sn\mnotg(G_1)\And\mnotg(G_2)$\br $\mnotg\Or$\\
 $\gna\snp (G_1)$\bv
$\perp$\bi $1$
\etab
%Or 2
\itc
$$\SP=\ianc{\ga\spp G_2}{\ga\spp G_{1}\Or G_{2}}
{ \vd\Or}$$
and $\SM$ ends in $\gna\snp (G_1\Or G_2)$. Symmetrical.
% \btab
%  $\ga\spp G_2$\bv
% $\gna\sn\mnotg(G_1)\And\mnotg(G_2)$\bv
%  $\gna\snp (G_1)$\bv
%  $\gna\snp (G_2)$\bv
% $\perp$\bi $1$
% \etab
\itc %\PI
$$\SP=\ianc{(\GG,y\oftp A);\cD\sp[y/x]G'}{\ga\sp \PIXA G'}{{\prv}
  \Pi^*}$$
and $\SM$ ends in $\gna\sp\mnotg(\PIXA G')$:
\btab
$(\GG,y\oftp A);\cD\sp[y/x]G'$\bs
%$\gna\sp\Pixa\mnotg(G')$\br $\mnotg\Pi$\\
$(\GG,y\oftp A);\cD\sp\mnotg([y/x]G')$\br $\mnotg\Pi$\\
%$(\GG,y\oftp A);\cD\sn[y/x]\mnotg(G')$\bv
$\perp$\bi $1$
\etab
\itc %\Imp
$$\SP= \ianc{\GG;(\cD\And D') \sp G'}{\ga\sp D' \Imp G'}{{\prv} \Imp}$$
and $\SM$ ends in $\gna\sp\mnotg(D'\Imp G')$:
\btab
$\GG;(\cD\And D') \sp G'$\bs
$\gna\sn D'\Imp \mnotg(G')$\br $\mnotg\Imp$\\
$\GG;(\cD\And D') \sp \mnotg(G')$\bv
$\perp$\bi $1$
\etab
\itc The (dis)equality case follows from the decidability of the (dis)equality
 judgment.
\enit