\begin{figure}
\label{fig:sf}
\[
\begin{array}{c}
% |-
% \ianc{}{}\ga\sp\top}{\top}\qquad\ianc{}{\gna\fp \perp}{S^{\nprv}_\perp}\vsk
% top and bot
\ianc{\vM = \vN}{\ga\sp \vM \eqd \vN}{S^{\prv}_{\eqd}}\qquad
\ianc{\vM \not = \vN}{\ga\fp \vM \eqd \vN}{S^{\nprv}_{\eqd}}\vsk
\ianc{\vM \not = \vN}{\ga\sp \vM \neqd \vN}{S^{\prv}_{\neqd}}\qquad
\ianc{\vM  = \vN}{\ga\fp \vM \neqd \vN}{S^{\nprv}_{\neqd}}\vsk
\ianc{\ga\sp G_1\quad\ga\sp G_{2}}{\ga\sp G_{1}\And G_{2}}{S^{\prv}_\And}
\qquad
\ianc{\ga\fp G_1\quad\ga\fp G_{2}}{\ga\fp G_{1}\Or G_{2}}{S^{\nprv}_\Or}
\vsk
\ianc{\ga\sp G_i}{\ga\sp G_{1}\Or G_{2}}{S^{\prv}_{\Or_i}}
\qquad
\ianc{\ga\fp G_i}{\ga\fp G_{1}\And G_{2}}{S^{\nprv}_{\And_i}}
% \qquad i\in 1\ \mbox{or} \ 2
\vsk
\ianc{ \ga\sp def(Q) \imm Q}{\ga\sp Q}{S{ {\rm atm}}}
\qquad
\ianc{ \ga\fp def(Q) \nimm Q}{\ga\fp Q}{S^{\nprv}_{ {\rm atm}}}
\ianc{\GG;\cA,\al\sp G}{\ga\sp \al\Imp G}{S^{\prv}_\Imp}
\qquad
\ianc{\GG;\cA,\al\fp G}{\ga\fp \al\Imp G}{S^{\nprv}_\Imp}
\vsk
\ianc{\GG,y:A;\cA\sp[y/x]G}{\ga\sp \Pi x:A.G}{S^{\prv}_\Pi}
\qquad
\ianc{\GG,y:A;\cA\fp[y/x]G}{\ga\fp \Pi x:A.G}{S^{\nprv}_\Pi}
\end{array}
\]
\caption{Provability and Denial}
\end{figure}

\begin{figure}
\label{fig:imm}
\[
\begin{array}{c}
% immediate >>
\ianc{}{\ga\sp\perp\imm  Q}{I^{\prv}_\perp}\qquad
\ianc{}{\ga\fp \top\nimm Q}{I^{\nprv}_\top}\vsk
\ianc{\vN = \vM}{\ga\sp q\ \vN \imm q\ \vM}{I^{\prv}_{\rm atm}}\qquad
\ianc{\vN \neq \vM}{\ga\fp q\ \vN \nimm q\ \vM}{I^{\nprv}_{\rm atm}}\vsk
\ianc{\mbox{for some $t:A$} \ \ga\sp  [t/x]D \imm Q}{\ga\sp \Pi x:A.D \imm Q}{I^{\prv}_\Pi}\qquad
\ianc{\mbox{for all $t:A$} \ \ga\fp [t/x]D \nimm Q}{\ga\fp \Pi x:A.D \nimm Q}{I^{\nprv}_\Pi}\vsk
\ianc{\ga\sp D_{i}\imm Q}{\ga\sp D_{1}\And D_{2}\imm Q}{I^{\nprv}_{\And_i}}\qquad
\ianc{\ga\fp D_{i}\nimm Q}{\ga\sp D_{1}\tensor D_{2}\nimm Q}{I^{\nprv}_{\tensor_i}}\vsk
\ianc{\ga\sp D_{1}\imm Q\quad \ga\sp D_{2}\imm Q}{\ga\sp D_{1}\tensor D_{2}\imm 
Q}{I^{\prv}_\tensor}\qquad
\ianc{\ga\fp D_{1}\nimm Q\quad \ga\fp D_{2}\nimm Q}{\ga\fp D_{1}\And D_{2}\nimm
Q}{I^{\nprv}_\And}\vsk
\ianc{\sp G}{ \ga\sp (G\Imp Q) \imm Q}{I^{\prv}_\Imp}
\vsk
\ianc{\ga\sp \vN\neqd\vM}{\ga\fp (G\Imp q\ \vN) \nimm q\ \vM}{I^{\nprv}_{\Imp_1}}
\qquad
\ianc{\ga\sp \vN\eqd\vM\quad\fp G} {\ga\fp (G\Imp q\ \vN) \nimm q\ \vM}{I^{\nprv}_{\Imp_2}}
% to avoid dependency pos-neg 
% \ianc{\ga\sp Q'\imm Q\quad\sp G}{ \ga\sp (G\Imp Q') \imm Q}{I^{\prv}_\Imp}
% \vsk
% \ianc{\ga\fp Q'\nimm Q}{ \ga\fp (G\Imp Q') \nimm Q}{I^{\nprv}_{\Imp_1}}
% \qquad
% \ianc{\ga\sp Q'\imm Q\quad\fp G} { \ga\fp (G\Imp Q') \nimm Q}{I^{\nprv}_{\Imp_2}}
\end{array}
\]
\caption{Immediate Entailment and its Complement}
\end{figure}\begin{figure}
\label{fig:sf}
\[
\begin{array}{c}
% |-
% \ianc{}{}\ga\sp\top}{\top}\qquad\ianc{}{\gna\fp \perp}{S^{\nprv}_\perp}\vsk
% top and bot
\ianc{\vM = \vN}{\ga\sp \vM \eqd \vN}{S^{\prv}_{\eqd}}\qquad
\ianc{\vM \not = \vN}{\ga\fp \vM \eqd \vN}{S^{\nprv}_{\eqd}}\vsk
\ianc{\vM \not = \vN}{\ga\sp \vM \neqd \vN}{S^{\prv}_{\neqd}}\qquad
\ianc{\vM  = \vN}{\ga\fp \vM \neqd \vN}{S^{\nprv}_{\neqd}}\vsk
\ianc{\ga\sp G_1\quad\ga\sp G_{2}}{\ga\sp G_{1}\And G_{2}}{S^{\prv}_\And}
\qquad
\ianc{\ga\fp G_1\quad\ga\fp G_{2}}{\ga\fp G_{1}\Or G_{2}}{S^{\nprv}_\Or}
\vsk
\ianc{\ga\sp G_i}{\ga\sp G_{1}\Or G_{2}}{S^{\prv}_{\Or_i}}
\qquad
\ianc{\ga\fp G_i}{\ga\fp G_{1}\And G_{2}}{S^{\nprv}_{\And_i}}
% \qquad i\in 1\ \mbox{or} \ 2
\vsk
\ianc{ \ga\sp def(Q) \imm Q}{\ga\sp Q}{S{ {\rm atm}}}
\qquad
\ianc{ \ga\fp def(Q) \nimm Q}{\ga\fp Q}{S^{\nprv}_{ {\rm atm}}}
\ianc{\GG;\cA,\al\sp G}{\ga\sp \al\Imp G}{S^{\prv}_\Imp}
\qquad
\ianc{\GG;\cA,\al\fp G}{\ga\fp \al\Imp G}{S^{\nprv}_\Imp}
\vsk
\ianc{\GG,y:A;\cA\sp[y/x]G}{\ga\sp \Pi x:A.G}{S^{\prv}_\Pi}
\qquad
\ianc{\GG,y:A;\cA\fp[y/x]G}{\ga\fp \Pi x:A.G}{S^{\nprv}_\Pi}
\end{array}
\]
\caption{Provability and Denial}
\end{figure}

\begin{figure}
\label{fig:imm}
\[
\begin{array}{c}
% immediate >>
\ianc{}{\ga\sp\perp\imm  Q}{I^{\prv}_\perp}\qquad
\ianc{}{\ga\fp \top\nimm Q}{I^{\nprv}_\top}\vsk
\ianc{\vN = \vM}{\ga\sp q\ \vN \imm q\ \vM}{I^{\prv}_{\rm atm}}\qquad
\ianc{\vN \neq \vM}{\ga\fp q\ \vN \nimm q\ \vM}{I^{\nprv}_{\rm atm}}\vsk
\ianc{\mbox{for some $t:A$} \ \ga\sp  [t/x]D \imm Q}{\ga\sp \Pi x:A.D \imm Q}{I^{\prv}_\Pi}\qquad
\ianc{\mbox{for all $t:A$} \ \ga\fp [t/x]D \nimm Q}{\ga\fp \Pi x:A.D \nimm Q}{I^{\nprv}_\Pi}\vsk
\ianc{\ga\sp D_{i}\imm Q}{\ga\sp D_{1}\And D_{2}\imm Q}{I^{\nprv}_{\And_i}}\qquad
\ianc{\ga\fp D_{i}\nimm Q}{\ga\sp D_{1}\tensor D_{2}\nimm Q}{I^{\nprv}_{\tensor_i}}\vsk
\ianc{\ga\sp D_{1}\imm Q\quad \ga\sp D_{2}\imm Q}{\ga\sp D_{1}\tensor D_{2}\imm 
Q}{I^{\prv}_\tensor}\qquad
\ianc{\ga\fp D_{1}\nimm Q\quad \ga\fp D_{2}\nimm Q}{\ga\fp D_{1}\And D_{2}\nimm
Q}{I^{\nprv}_\And}\vsk
\ianc{\sp G}{ \ga\sp (G\Imp Q) \imm Q}{I^{\prv}_\Imp}
\vsk
\ianc{\ga\sp \vN\neqd\vM}{\ga\fp (G\Imp q\ \vN) \nimm q\ \vM}{I^{\nprv}_{\Imp_1}}
\qquad
\ianc{\ga\sp \vN\eqd\vM\quad\fp G} {\ga\fp (G\Imp q\ \vN) \nimm q\ \vM}{I^{\nprv}_{\Imp_2}}
% to avoid dependency pos-neg 
% \ianc{\ga\sp Q'\imm Q\quad\sp G}{ \ga\sp (G\Imp Q') \imm Q}{I^{\prv}_\Imp}
% \vsk
% \ianc{\ga\fp Q'\nimm Q}{ \ga\fp (G\Imp Q') \nimm Q}{I^{\nprv}_{\Imp_1}}
% \qquad
% \ianc{\ga\sp Q'\imm Q\quad\fp G} { \ga\fp (G\Imp Q') \nimm Q}{I^{\nprv}_{\Imp_2}}
\end{array}
\]
\caption{Immediate Entailment and its Complement}
\end{figure}