\newcommand{\Dl}[1]{\mbox{$\bf \mathbf{\delta}#1$}}
\newcommand{\mytilde}{\scriptstyle\sim}

\newcommand{\InConv}{\smallsmile}

\newcommand{\mystrut}[1]{
\bpf \A ; "$\vphantom{X}$" \U ['] ; "$\vphantom{X}$" "#1" \epf \ %
}

\newcommand{\idrule}[2]{
 \mbox{#1 \ $\mbox{#2}$}}

\newcommand{\ds}{\displaystyle\strut}

\newcommand{\urule}[3]{
 \mbox{#1 \ $\frac{\ds \mbox{#2}}{\ds \mbox{#3}}$}}


\newcommand{\brule}[4]{
 \mbox{#1 \ $\frac{\ds \mbox{#2}\ \ \ \ \mbox{#3}}
                   {\ds \mbox{#4}}$}}


\newcommand\invrule[3]{
\begin{tabular}{r@{}l}
 \multicolumn{1}{r}{#1} & 
 \begin{tabular}{@{}c@{}}
     \raisebox{0.2em}{#2} 
     \\ \hline \hline 
     \raisebox{-0.2em}{#3} 
 \end{tabular}
\end{tabular}
}

\newcommand\doubleinvrule[4]{
\begin{tabular}{r@{}l}
 \multicolumn{1}{r}{#1} & 
 \begin{tabular}{@{}c@{}}
     #2 \\[0.4em] \hline \hline 
     \raisebox{-0.4em}{#3} \\[0.7em] \hline \hline 
     \raisebox{-0.4em}{#4} 
 \end{tabular}
\end{tabular}
}

\newcommand{\AstLeft}{
 \invrule{ }{$\ast X \vdash Y$}{$\ast Y \vdash X$}
}

\newcommand{\AstRight}{
 \invrule{ }{$X \vdash \ast Y$}{$Y \vdash \ast X$}
}

\newcommand{\AstAstLeft}{
 \invrule{$(\ast \ast \vdash)$}{$X \vdash Y$}{$\ast \ast X \vdash Y$}
}

\newcommand{\AstAstRight}{
 \invrule{$(\vdash \ast \ast)$}{$X \vdash Y$}{$X \vdash \ast \ast Y$}
}

\newcommand{\ResidConv}{
 \invrule{ }{$\stc X \vdash Y$}{$X \vdash \stc Y$}
}

\newcommand{\ConvConvLeft}{
 \invrule{ }{$\stc \stc X \vdash Y$}{$X \vdash Y$}
}

\newcommand{\ConvConvRight}{
 \invrule{ }{$X \vdash \stc \stc Y$}{$X \vdash Y$}
}

\newcommand{\DualResidInt}{
 \doubleinvrule{ }{$Z \semic \ast \stc Y \vdash X$}
                  {$Z \vdash X \semic Y$}
                  {$\ast \stc X \semic Z \vdash Y$}
}

\newcommand{\ResidInt}{
 \doubleinvrule{ }{$X \vdash Z \semic \ast \stc Y$}
                  {$X \semic Y \vdash Z$}
                  {$Y \vdash \ast \stc X \semic Z$}
}

\newcommand{\DualResidExt}{
 \doubleinvrule{ }{$Z \comma \vphantom{\semic} \ast Y \vdash X$}
                  {$Z \vdash X \vphantom{\semic} \comma Y$}
                  {$\ast X \comma \vphantom{\semic} Z \vdash Y\,\,\,$}
}

\newcommand{\ResidExt}{
 \doubleinvrule{ }{$X \vdash Z \vphantom{\semic} \comma \ast Y$}
                  {$X \comma Y \vphantom{\semic} \vdash Z$}
                  {$Y \vdash \ast X \vphantom{\semic} \comma Z \,\,\,$}
}