\newcommand{\mnotr}{\mnot_{x}^{C}}
\newcommand{\zij}{[\ex/Z_i,N/Z_j]\ol{Z_n}}
\newcommand{\zi}{[\ex/Z_i]\ol{Z_n}}

\begin{figure}
\renewcommand{\ga}{\GG\vd}
    \[
    \begin{array}{c}
       \ianc{}{\GG\vda\mnota (\perp)  =  \top}{\mnota\perp}\vsk
 \ianc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}
%{sh(x,A_i)=\ex}
{\GG\vd\mnota (\top_q)  = \BAnd_{x\in 
 dom(\GG)}(\BAnd_{1\leq i\leq n,xR^{i}q} \mnotr(\top_q))
%\BAnd_{x\in dom(\GG)}\BAnd_{xR^{i}q}\mnotxi(\top_q)
}{\mnota\top}\vsk\\ 
\ianc{\GG\vd\mnotg(G) = G'}
{\GG\vd\mnota( \Pi(q\ \Mn\If G)) =(\BAnd_{x\in
           dom(\GG)} \mnotr(q\ \Mn)\And (\BAnd_{1\leq
           i\leq n,xR^{i}q}\GG\vd\mnotxi(q\ \Mn))) \And \Pi( \neg q\ \Mn)\If G')}{\mnota\If}  
\vsk\vsk
        \ibnc{\GG\vda\mnota (D_{1})= D_1'}{\GG\vda\mnota (D_{2})= D_2'}{\GG\vda\mnota
        ( D_{1}\And D_{2})=D_1'\tensor D_2'}{\mnot\And}\vsk
       \ibnc{\GG\vda\mnota (D_{1})= D_1'}{\GG\vda\mnota (D_{2})= D_2'}{\GG\vda\mnota
        ( D_{1}\tensor D_{2})=D_1'\And D_2'}{\mnot\tensor}
\vsk\vsk
\ianc{M_i\hastype A_i \mbox{ rigid},\cdot\vd sh(x,A_i)=\ex, M_i\not
  \equiv \ex}{\mnotr(q\ \Mn)= \BAnd_{1\leq i\leq n}
\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\  \zi}{\mnotr}
\vsk\vsk 
% Ex GAMMA case 
%\ibnc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\cdot\vd sh(x,A_i)=\ex}
% {\gfq\mnotxi(\top_q)  =
%       \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\  \ol{Z^i_{\ex}}\If \top}{\mnotxi\top}\vsk
%  \ianc{M_i\equiv \ex, head(M_j)\in\dom(\GG)}
% {\gfq\mnotxi  (q\ \Mn)=
%     \BAnd_{1\leq j\leq n}^{j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
%      \neg q\ \zi\If M_j\neqd Z_j)}{\mnotxi\GG}\vsk\\
\ianc{M_i\equiv \ex
%,head(M_j)\in\dom(\Sigma)\mbox{ or Flex}
}{\gfq\mnotxi  (q\ \Mn)=
    \BAnd_{1\leq j\leq n}^{j\not = i}(  \BAnd_{N\in(\GG\vd\mnot(M_j))}
(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}\neg q\ \zij))
%   \Pi(  \neg q\ Z_1\dots Z_{i-1}\ \ex\ Z_{i+1}\dots Z_{j-1}\ N\
%   Z_{j+1}\ \dots Z_n)
}{\mnotxi}

\vsk\vsk
\ianc{}{\gvd sh(x,a)=x}{\ex\atm}
\qquad
\ianc{\GG,y\oftp A\vd sh(x,B)=\ex}{\GG\vd sh(x,A\Imp B)=\lamb{y}{A}\ex}{\ex\Imp^y}
% \ianc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\gfq\mnotxi(\top_q)  =
%       \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ Z_1\dots Z_{i-1}\ x\
%       Z_{i+1}\dots Z_n}{\mnotxi\top}\vsk
%     \ianc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\gfq\mnotxi  (q\ \Mn)=
%     \BAnd_{1\leq j\leq n}^{j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
%      \neg q\ \zi\If M_j\neqd Z_j)}{\mnotxi\atm}
 \end{array}\]
    \caption{Assumption complementation: $\GG\vda\mnota(D)=D'$}
  \label{fig:notass}
\end{figure}







