\begin{figure}
 \[
 \begin{array}{c}
 \ianc{}{\top\tensor D \setminus \top}{\tensor\top D}
	\qquad
 \ianc{}{D\tensor\top \setminus \top}{\tensor D \top }
\ianc{}{\perp\tensor D \setminus D}{\tensor\perp D}
	\qquad
 \ianc{}{D\tensor\perp \setminus \perp}{\tensor D \perp }

 \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}
\vsk
 \ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D'_{2}\setminus D'}
 {(D_{1}\And D'_{1})\tensor (D_{2}\And D'_2)\setminus D\And D'}{\tensor\And\Or}
 \end{array}
 \]
 \caption{$\tensor$-Elimination: $D_{1}\tensor D_{2}\setminus D$}
 \label{fig:otimes}
 \end{figure}
