\begin{figure}
\[
\begin{array}{c}
\ianc{}{\top\tensor D \setminus \top}{\tensor\top D}\qquad
\ianc{}{D\tensor\top \setminus \top}{\tensor D \top }\vsk
\ianc{}{\perp\tensor D \setminus D}{\tensor\perp D}\qquad
\ianc{}{D\tensor\perp \setminus D}{\tensor D \perp }
\vsk
\ianc{}{\Pi(q\ \vN_{1}\If G_{1})\tensor  \Pi(q\ \vN_{2}\If G_{2}) \setminus
\Pi(q\ \vN_{1}\If (\vN_{1}\eqd \vN_{2}) \And G_{1}\And G_{2})}{\tensor{\rm 
At}\atm}\vsk
\ianc{q\not\equiv q'}{\Pi(q\ \vN_{1}\If G_{1})\tensor  \Pi(q'\
  \vN_{2}\If G_{2}) \setminus\top}{\tensor{\rm At}\atm\not\equiv}\vsk 
\ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D_{2}\setminus D'}
{(D_{1}\tensor D'_{1})\tensor D_{2}\setminus D\tensor
  D'}{\tensor\tensor L}
\qquad
\ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D_{2}\setminus D'}
{(D_{1}\And D'_{1})\tensor D_{2}\setminus D\And D'}{\tensor\And L}
\vsk
\ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D_{2}\setminus D'}
{D_2\tensor (D_{1}\tensor D'_{1})\setminus D\tensor
  D'}{\tensor\tensor R}
\qquad
\ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D_{2}\setminus D'}
{D_2\tensor (D_{1}\And D'_{1})\setminus D\And D'}{\tensor\And R}
\end{array}
\]
\caption{$\tensor$-Elimination: $D_{1}\tensor D_{2}\setminus D$}
\label{fig:otimes}
\end{figure}

% \ibnc{\Pi(q\ \vN\If G)\tensor D_{1}\setminus D}{\Pi(q\ \vN\If
%   G)\tensor D_{2}\setminus D'} 
% {\Pi(q\ \vN\If G)\tensor (D_{1}\tensor D_{2})\setminus D\tensor
%   D'}{\tensor\atm\tensor}
% \vsk
% \ibnc{\Pi(q\ \vN\If G)\tensor D_{1}\setminus D}{\Pi(q\ \vN\If
%   G)\tensor D_{2}\setminus D'} 
% {\Pi(q\ \vN\If G)\tensor (D_{1}\And D_{2})\setminus D\And
%   D'}{\tensor\atm\And}
% \vsk

%  \ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D'_{2}\setminus D'}
%  {(D_{1}\And D'_{1})\tensor (D_{2}\tensor D'_2)\setminus D\tensor D'}{\tensor\And\Or}
% \vsk
%  \ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D'_{2}\setminus D'}
%  {(D_{1}\tensor D'_{1})\tensor (D_{2}\tensor D'_2)\setminus D\tensor D'}{\tensor\And\Or}