%\newcommand{\Es}{\mbox{$\cal S$}}

%\newcommand{\reln}[2]{\mbox{${#1}_{#2}$}}
%\newcommand{\relR}[1]{\reln{R}{#1}}
%\newcommand{\relS}[1]{\reln{S}{#1}}

%\newcommand{\RInAnd}{\relR{\InAnd}}
%\newcommand{\RInOr}{\relR{\InOr}}


%\newcommand{\rpgnb}{\InNBut}
%\newcommand{\rpgbn}{\InButN}
%\newcommand{\rpgimp}{\InImp}
%\newcommand{\rpgif}{\InIf}
%\newcommand{\rpgcap}{\ExAnd}
%\newcommand{\rpgcup}{\ExOr}
%\newcommand{\rpgast}{\InAnd}
%\newcommand{\rpgplus}{\InOr}
%\newcommand{\rpgtop}{\ExTop}
%\newcommand{\rpgbot}{\ExBot}
%\newcommand{\rpgone}{\InTop}
%\newcommand{\rpgzero}{\InBot}
%\newcommand{\rpgleq}{\leq}
%\newcommand{\rpggeq}{\geq}

%\newcommand{\boldA}{\mbox{\bf A}}
%\newcommand{\onoimp}{\leftarrow}
%\newcommand{\onoimpp}{\rightarrow}
%\newcommand{\onocap}{\ExAnd}
%\newcommand{\onocup}{\ExOr}
%\newcommand{\onoast}{\InAnd}
%\newcommand{\onoplus}{\InOr}
%\newcommand{\onotop}{\ExTop}
%\newcommand{\onobot}{\ExBot}
%\newcommand{\onoone}{\InTop}
%\newcommand{\onozero}{\InBot}
%\newcommand{\onoleq}{\leq}

%\newcommand{\tridelta}{\vartriangle}

%\newcommand{\BiL}{\mbox{BiL}}
%\newcommand{\FL}{\mbox{FL}}

\newcommand{\rp}[2]{\mbox{\rm rp$(#1,#2)$}}
%\newcommand{\drp}[2]{\mbox{\rm drp$(#1,#2)$}}
%\newcommand{\rptwo}[3]{\mbox{\rm rp$(#1,#2,#3)$}}
%\newcommand{\drptwo}[3]{\mbox{\rm drp$(#1,#2,#3)$}}
%\newcommand{\gc}[2]{\mbox{\rm gc$(#1,#2)$}}
%\newcommand{\dgc}[2]{\mbox{\rm dgc$(#1,#2)$}}
%\newcommand{\gctwo}[3]{\mbox{\rm gc$(#1,#2,#3)$}}
%\newcommand{\dgctwo}[3]{\mbox{\rm dgc$(#1,#2,#3)$}}

%\newcommand{\dual}[1]{\mbox{$#1^{\delta}$}}
%\newcommand{\alphadual}[1]{\mbox{$#1^{\alpha}$}}

%%\newcommand{\Drel}{\mbox{\bf DRA }}
\newcommand{\Lg}[1]{\mbox{$\mathbf{#1}$}}
\newcommand{\Kt}{\Lg{K_{t}}}
\newcommand{\mcal}[1]{\mbox{$\cal #1$}}
\newcommand{\Dl}[1]{\mbox{$\bf \mathbf{\delta}#1$}}

%%\newcommand{\Fml}{\mbox{$\mathbf{Fml}$}}
%%\newcommand{\LAlg}{\mbox{$\mathfrak{Fml}/\!\!\equiv$}}

%\newcommand{\BiLC}{\mbox{BiLC}}

%%\newtheorem{theorem}{Theorem}
%%\newtheorem{conjecture}{Conjecture}
%%%\newtheorem{corollary}{Corollary}
%%\newtheorem{proposition}{Proposition}
%%\newtheorem{lemma}{Lemma}
%%\newtheorem{remark}{Remark}
%%\newtheorem{example}{Example}

%\newcommand{\qed}{\hspace*{\fill} q.e.d.}

%\newcommand{\tik}{\mbox{$\checkmark$}}

%%%%% Properties of functions

\newcommand{\tn}{\mbox{tn}}
%%\newcommand{\ton}[3]{\mbox{$#1^{#3}_{#2}$}}
\newcommand{\ton}[3]{\mbox{$\tn(#1,#2,#3)$}}
%\newcommand{\tonoid}[4]{{\cal #1} := (#2, #3, #4)}
%\newcommand{\pggl}[4]{{\cal #1} := (#2, #3, #4)}
%\newcommand{\mytrace}[3]{\mbox{$#1 : #2 \mapsto (#3)$}}
%\newcommand{\fn}[1]{f_{#1}}
%\newcommand{\FN}[1]{F_{#1}}
%\newcommand{\FNSTR}[1]{\circledS_{#1}}
%\newcommand{\FNSTRa}[1]{\circledS_{#1}^{a}}
%\newcommand{\FNSTRs}[1]{\circledS_{#1}^{s}}


%%%%%%%%% Lattice Connectives

%\newcommand{\LatTop}{\top}
%\newcommand{\LatBot}{\bot}

%\newcommand{\eqprv}{\dashv\vdash}

%%%%%% Intuitionistic Implication Defined

%\newcommand{\IntImp}{\Rightarrow}

%%%%%% Modalities

\newcommand{\WhtDia}{\Diamond}
\newcommand{\WhtBox}{\Box} 
\newcommand{\BlkDia}{\blacklozenge}
\newcommand{\BlkBox}{\blacksquare}

%\newcommand{\RealBang}{\mbox{\,!\,}}
%\newcommand{\RealGnab}{\mbox{\,?\,}}

%\newcommand{\Bang}{\blacklozenge}
%\newcommand{\Gnab}{\Box}

%\newcommand{\Exp}{\mbox{\scriptsize e}}
%\newcommand{\DExp}{\mbox{\scriptsize d}}


%%%%%% Intensional Connectives

%%\newcommand{\mcyl}{\raisebox{0.2ex}{\bf c}}

\newcommand{\InOr}{\oplus}
\newcommand{\InAnd}{\otimes}

%% define the font for par and with ...
%\DeclareFontFamily{U}{stmary}{}
%\DeclareFontShape{U}{stmary}{}{}{<5> <6> <7> <8> <9> <10> gen * stmary %
%        <10.95> <12> <14.4> <17.28> <20.74> <24.88> stmary10}{}
%\DeclareSymbolFont{linear}{U}{stmary}{}{}
%\DeclareMathSymbol{\por}{\mathbin}{linear}{'117}
%\DeclareMathSymbol{\with}{\mathbin}{linear}{'116}

%\newfont{\stmary}{stmary10 scaled\magstep3}
%%\newfont{\ams}{msxm10 scaled\magstep3}

%\newcommand{\InvAmpersand}{\por}

\newcommand{\InImp}{\rightarrow}
\newcommand{\InIf}{\leftarrow}
\newcommand{\InIff}{\leftrightarrow}

%%\newcommand{\InNBut}{\mbox{ $>\!\!\!-$ }}
%%\newcommand{\InNBut}{\mbox{ $\raisebox{0.16ex}{$\scriptstyle >$}\!-$ }}
%%\newcommand{\InButN}{\mbox{ $-\!\raisebox{0.16ex}{$\scriptstyle <$}$ }}

%\newcommand{\InNBut}{
%       \mbox{\,\raisebox{0.14ex}{$\scriptstyle>$}\!\!\raisebox{0.14ex}{$\scriptstyle -$}\,}}
%\newcommand{\InButN}{
%       \mbox{\,\raisebox{0.13ex}{$\scriptstyle-$}\!\!\raisebox{0.13ex}{$\scriptstyle <$}\,}}

%\newcommand{\InNButN}{
%       \mbox{ \raisebox{0.14ex}{$\scriptstyle>$}\!\raisebox{0.13ex}{$\scriptstyle\sim$}\!\raisebox{0.13ex}{$\scriptstyle <$} }}

%\newcommand{\InNImpN}{
%       \mbox{ \raisebox{0.14ex}{$\scriptstyle<$}\!\raisebox{0.13ex}{$\scriptstyle\sim$}\!\raisebox{0.13ex}{$\scriptstyle >$} }}

%\newcommand{\InTop}{\mbox{\bf 1}}
%\newcommand{\InBot}{\mbox{\bf 0}}
%\newcommand{\SmallInTop}{\mbox{\scriptsize \bf 1}}
%\newcommand{\SmallInBot}{\mbox{\bf \scriptsize 0}}

%%%%%%%%% Negations

%\newcommand{ \InIfNot   }[1] { \mbox{$\mbox{\!}^{\SmallInBot}\!#1$} }    
%\newcommand{ \InImpNot  }[1] { \mbox{$#1^{\SmallInBot}$} }    
%\newcommand{ \InButNNot }[1] { \mbox{$\mbox{\!}^{\SmallInTop}\!#1$}  } 
%\newcommand{ \InNButNot }[1] { \mbox{$#1^{\SmallInTop}$} }

%\newcommand{\negR}{\neg_{r}}% = \InImpNot
%\newcommand{\negL}{\neg_{l}}% = \InNButNot

%\newcommand{\simR}{\sim_{r}}% = \InIfNot
%\newcommand{\simL}{\sim_{l}}% = \InButNNot

%%%%%%%%%% Converses

%%\newcommand{\Inyzero}{\mbox{\bf 0}}
%%\newcommand{\mstar}{\bigstar}

%\newcommand{\InConv}{\smallsmile}
%%\newcommand{\conv}{\smallsmile}

%%
%%%\newcommand{\fiss}{+}

%%%%%%% Extensional Connectives

\newcommand{\ExTop}{\top}
\newcommand{\ExBot}{\bot}
\newcommand{\ExOr}{\vee}
\newcommand{\ExAnd}{\wedge}
\newcommand{\ExNot}{\neg}
%\newcommand{\ExImp}{\supset}

%%\newcommand{\eqded}{\dashv \vdash}

%%%%%% Structural Connectives

%\newcommand{\conv}{\mbox{$\scriptsize \raisebox{0.15em}{\copyright}$}}

%\newcommand{\pesm}{--}

%\newcommand{\stc}{\circ}

%\newcommand{\mycolon}{\mbox{ : }}
%\newcommand{\mybar}{\mbox{ | }}

\newcommand{\semic}{\mbox{ ; }}

%\newcommand{\InTpBt}{\Phi}
\newcommand{\ExTpBt}{\mbox{\rm I}}

\newcommand{\blkb}{\bullet}
%\newcommand{\whtb}{\circ}

%%\newcommand{\blkcnv}{\bullet}
%%\newcommand{\whtcnv}{\circ}

%\newcommand{\rht}{\mbox{ \raisebox{0.2ex}{$\scriptstyle >$} }}
%\newcommand{\lft}{\mbox{ \raisebox{0.2ex}{$\scriptstyle <$} }}

%\newcommand{\shp}{\sharp}
%\newcommand{\flt}{\flat}

%%\newcommand{\comma}{\raisebox{0.5ex}{ , }}
%%%\newcommand{\colon}{\mbox{ : }}

%%%%%% Rule Names

\newcommand{\Str}{\mbox{\rm Str}}
\newcommand{\Ass}{\mbox{\rm Ass}}
\newcommand{\Ctr}{\mbox{\rm Ctr}}
\newcommand{\Wk}{\mbox{\rm Wk}}
\newcommand{\Com}{\mbox{\rm Com}}
%\newcommand{\ComRhs}{\mbox{$(\vdash \Com)$}}
\newcommand{\Ver}[1]{\mbox{\rm Ver-#1}}
\newcommand{\Efq}[1]{\mbox{\rm Efq-#1}}

%%%%%% Rule Forming Commands

%\newcommand{\ahstrut}%          %% phantom for proofs
%  {\makebox[0cm]{\phantom{\rule{0em}{1.3em}}}}

%\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{\CopyrightRP}{
% \invrule{\rp{\conv}{\conv}}{$\conv X \vdash Y$}{$X \vdash \conv Y$}
%}

%\newcommand{\NegDGC}{
% \invrule{\dgc{\shp}{\flt}}{$\shp X \vdash Y$}{$\flt Y \vdash X$}
%}

%\newcommand{\NegGC}{
% \invrule{\gc{\shp}{\flt}}{$X \vdash \shp Y$}{$Y \vdash \flt X$}
%}

%\newcommand{\WhtBlobRP}{
% \invrule{\rp{\whtb}{\whtb}}{$\whtb X \vdash Y$}{$X \vdash \whtb Y$}
%}

\newcommand{\BlkBlobRP}{
 \invrule{\rp{\blkb}{\blkb}}{$\blkb X \vdash Y$}{$X \vdash \blkb Y$}
}

%\newcommand{\WhtCnvRP}{
% \invrule{\rp{}{}}{$ X \vdash Y$}{$X \vdash Y$}
%}

%\newcommand{\BlkCnvRP}{
% \invrule{\rp{}{}}{$X \vdash Y$}{$X \vdash Y$}
%}


%\newcommand{\ConvConvLeft}{
% \invrule{$(\conv \conv \vdash)$}{$X \vdash Y$}{$\conv \conv X \vdash Y$}
%}

%\newcommand{\ConvConvRight}{
% \invrule{$(\vdash \conv \conv)$}{$X \vdash Y$}{$X \vdash \conv \conv Y$}
%}


%\newcommand{\ImpRP}{
% \doubleinvrule{$\rptwo{\!\!\semic\!\!}{\!\!\rht\!\!}{\!\!\lft\!\!}$}
%                  {$X \vdash Z \lft Y$}
%                  {$X \semic Y \vdash Z$}
%                  {$Y \vdash X \rht Z$}
%}


%\newcommand{\ImpDRP}{
% \doubleinvrule{$\drptwo{\!\!\semic\!\!}{\!\!\rht\!\!}{\!\!\lft\!\!}$}
%                  {$Z \lft Y \vdash X$}
%                  {$Z \vdash X \semic Y$}
%                  {$X \rht Z \vdash Y$}
%}


%\newcommand{\ConvDistLeft}{
% \invrule{$(\mbox{ dist } \vdash)$}
%         {$\conv (X \semic Y) \vdash Z $}
%         {$(\conv Y) \semic (\conv X) \vdash Z$}
%}            

%\newcommand{\ConvDistRight}{
% \invrule{$(\vdash \mbox{ dist })$}
%       {$Z \vdash \conv (X \semic Y) $}
%       {$Z \vdash (\conv Y) \semic (\conv X) $}}            


%\newcommand{\ConvInTpBtLeft}{
% \invrule{($\conv \InTpBt \vdash$)}{$\InTpBt \vdash X$}
%            {$\conv \InTpBt \vdash X$}
%}

%\newcommand{\ConvInTpBtRight}{
% \invrule{($\vdash \conv \InTpBt$)}{$X \vdash \InTpBt$}
%            {$X \vdash \conv \InTpBt$}
%}

%\newcommand{\ConvExTpBtLeft}{
% \invrule{($\conv \ExTpBt \vdash$)}{$\ExTpBt \vdash X$}
%            {$\conv \ExTpBt \vdash X$}
%}

%\newcommand{\ConvExTpBtRight}{
% \invrule{($\vdash \conv \ExTpBt$)}{$X \vdash \ExTpBt$}
%            {$X \vdash \conv \ExTpBt$}
%}

%%%% Structural Rules

%\newcommand{\StrSharpLeft}{
% \invrule{$(\shp \vdash)$}
%         {$X \rht \InTpBt \vdash Y$}
%         {$\shp X \vdash Y$}
%}

%\newcommand{\StrSharpRight}{
% \invrule{$(\vdash \shp)$}
%         {$Y \vdash X \rht \InTpBt$}
%         {$Y \vdash \shp X$}
%}

%\newcommand{\StrFlatLeft}{
% \invrule{$(\flt \vdash)$}
%         {$\InTpBt \lft X \vdash Y$}
%         {$\flt X \vdash Y$}
%}

%\newcommand{\StrFlatRight}{
% \invrule{$(\vdash \flt)$}
%         {$Y \vdash \InTpBt \lft X$}
%         {$Y \vdash \flt X$}
%}

\newcommand{\SemicAssLeft}{
 \invrule{($\Ass \vdash$)}
            {$X \semic  (Y  \semic  Z) \vdash W$}
            {$(X  \semic  Y) \semic  Z \vdash W$}
}

\newcommand{\SemicAssRight}{
 \invrule{($\vdash \Ass)$}
            {$W \vdash (X  \semic  Y) \semic  Z $}
            {$W \vdash X \semic  (Y  \semic  Z)$}

}

\newcommand{\SemicComLeft}{
 \urule{($\Com \vdash$)}
            {$Y  \semic  X \vdash Z $}
            {$X  \semic  Y \vdash Z $}
}

\newcommand{\SemicComRight}{
 \urule{($\vdash \Com$)}
            {$Z \vdash Y  \semic  X $}
            {$Z \vdash X  \semic  Y $}
}

\newcommand{\SemicContLeft}{
 \urule{($\Ctr \vdash$)}
            {$X  \semic  X \vdash Z $}
            {$X  \vdash Z $}
}

\newcommand{\SemicContRight}{
 \urule{($\vdash \Ctr$)}{$Z \vdash X  \semic  X $}
            {$Z \vdash X $}
}

\newcommand{\SemicWeakLeftOne}{
 \urule{($\Wk \vdash$)}{$X \vdash Z $}
            {$X  \semic  Y \vdash Z $}
}

\newcommand{\SemicWeakLeftTwo}{
 \urule{ }{$Y \vdash Z $}
            {$X  \semic  Y \vdash Z $}
}

\newcommand{\SemicWeakRightOne}{
 \urule{($\vdash \Wk)$}{$Z \vdash X $}
            {$Z \vdash X \semic  Y$}
}

\newcommand{\SemicWeakRightTwo}{
 \urule{ }{$Z \vdash Y $}
            {$Z \vdash X \semic  Y$}
}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Yetter's Rules

%\newcommand{\Yet}{\mbox{\rm Yet}}

%\newcommand{\YetterLeft}{
% \urule{$(\Yet \vdash)$}
%               {$Y \semic X \vdash \InTpBt$}
%               {$X \semic Y \vdash \InTpBt$}
%}
%\newcommand{\YetterRight}{
% \urule{$(\vdash \Yet)$}
%               {$\InTpBt \vdash Y \semic X$}
%               {$\InTpBt \vdash X \semic Y$}
%}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Grishin's Rules

%\newcommand{\Grn}{\mbox{\rm Grn}}
 
%\newcommand{\GrishinAiRight}{
% \urule{$(\vdash \Grn a(i))$}
%               {$W \vdash (X  \semic Y) \lft Z$}
%               {$W \vdash X \semic (Y \lft  Z)$}

%}

%\newcommand{\GrishinAiLeft}{
% \urule{$(\Grn a(i) \vdash)$}
%               {$X \rht (Y \semic Z)  \vdash W$}
%               {$(X \rht Y) \semic Z  \vdash W$}
%}

%\newcommand{\GrishinAiiLeft}{
% \urule{$(\Grn a(ii) \vdash)$}
%               {$(X \semic Y) \lft  Z \vdash W$}
%               {$X  \semic (Y \lft Z)  \vdash W$}
%}

%\newcommand{\GrishinAiiRight}{
% \urule{$(\vdash \Grn a(ii))$}
%               {$W \vdash X  \rht (Y \semic  Z)$}
%               {$W \vdash (X \rht Y) \semic Z$}
%}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\newcommand{\GrishinBiiLeft}{
% \urule{$(\Grn b(ii) \vdash)$}
%               {$X  \semic (Y \lft Z)  \vdash W$}
%               {$(X \semic Y) \lft  Z \vdash W$}
%}
 
%\newcommand{\GrishinBiRight}{
% \urule{$(\vdash \Grn b(i))$}
%               {$W \vdash X \semic (Y \lft  Z)$}
%               {$W \vdash (X  \semic Y) \lft Z$}
%}

%\newcommand{\GrishinBiLeft}{
% \urule{$(\Grn b(i) \vdash)$}
%               {$(X \rht Y) \semic Z  \vdash W$}
%               {$X \rht (Y \semic Z)  \vdash W$}
%}

%\newcommand{\GrishinBiiRight}{
% \urule{$(\vdash \Grn b(ii))$}
%               {$W \vdash (X \rht Y) \semic Z$}
%               {$W \vdash X  \rht (Y \semic  Z)$}
%}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\newcommand{\GrishiniiLeft}{
% \invrule{$(\Grn (ii) \vdash)$}
%               {$(X \semic Y) \lft  Z \vdash W$}
%               {$X  \semic (Y \lft Z)  \vdash W$}

%}
 
%\newcommand{\GrishiniRight}{
% \invrule{$(\vdash \Grn (i))$}
%               {$W \vdash (X  \semic Y) \lft Z$}
%               {$W \vdash X \semic (Y \lft  Z)$}

%}

%\newcommand{\GrishiniLeft}{
% \invrule{$(\Grn (i) \vdash)$}
%               {$X \rht (Y \semic Z)  \vdash W$}
%               {$(X \rht Y) \semic Z  \vdash W$}
%}

%\newcommand{\GrishiniiRight}{
% \invrule{$(\vdash \Grn (ii))$}
%               {$W \vdash X  \rht (Y \semic  Z)$}
%               {$W \vdash (X \rht Y) \semic Z$}
%}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\newcommand{\InTpBtPlusMinusLeft}{
% \doubleinvrule{$(\InTpBt^{+}_{-} \vdash)$}
%               {$X \semic \InTpBt \vdash Y$}
%               {$X \vdash Y $}
%               {$\InTpBt \semic X \vdash Y$}
%}

%\newcommand{\InTpBtPlusMinusRight}{
% \doubleinvrule{$(\vdash \InTpBt^{+}_{-} )$}
%               {$X \vdash \InTpBt \semic Y $}
%               {$X \vdash Y $}
%               {$X \vdash Y \semic \InTpBt $}
%}


\newcommand{\EfqExTpBt}{
 \urule{(\Efq{$\ExTpBt$})}
          {$X \vdash \ExTpBt$}
          {$X \vdash Y$}
}

\newcommand{\VerExTpBt}{
 \urule{(\Ver{$\ExTpBt$})}
          {$\ExTpBt \vdash X$}
          {$Y \vdash X$}
}

%%%%%%%%%%%%%%%%% Logical Rules


%\newcommand{\InTopLeft}{
% \urule{$(\InTop \vdash)$}
%          {$\InTpBt \vdash Z $}
%          {$\InTop \vdash Z$}
%}

%\newcommand{\InTopRight}{
% \idrule{$(\vdash \InTop)$}{$\InTpBt \vdash \InTop$}
%}

%\newcommand{\InBotRight}{
% \urule{$(\vdash \InBot)$}
%          {$Z \vdash \InTpBt $}
%          {$Z \vdash \InBot$}
%}

%\newcommand{\InBotLeft}{
% \idrule{$(\InBot \vdash)$}{$\InBot \vdash \InTpBt $}
%}

%%%%%%%%%%%%%%%%%%%%%%%%%%% Negations 


%\newcommand{\InNButNotLeft}{
% \urule{$(\InNButNot{.} \vdash)$}
%          {$\shp A \vdash Z $}
%          {$\InNButNot{A} \vdash Z$}
%}

%\newcommand{\InNButNotRight}{
% \urule{$(\vdash \InNButNot{.})$}
%          {$A \vdash Z $}
%          {$\shp Z \vdash \InNButNot{A} $}
%}

%\newcommand{\InButNNotLeft}{
% \urule{$(\InButNNot{.} \vdash)$}
%          {$\flt A \vdash Z $}
%          {$\InButNNot{A} \vdash Z$}
%}

%\newcommand{\InButNNotRight}{
% \urule{$(\vdash \InButNNot{.})$}
%          {$A \vdash Z $}
%          {$\flt Z \vdash \InButNNot{A} $}
%}

%\newcommand{\InImpNotLeft}{
% \urule{$(\InImpNot{.} \vdash)$}
%          {$Z \vdash A $}
%          {$\InImpNot{A} \vdash \shp Z$}
%}

%\newcommand{\IntImpNotRight}{
% \urule{$(\vdash \InImpNot{.})$}
%          {$Z \vdash \shp A $}
%          {$Z \vdash \InImpNot{A} $}
%}

%\newcommand{\InIfNotLeft}{
% \urule{$(\InIfNot{.} \vdash)$}
%          {$Z \vdash A $}
%          {$\InIfNot{A} \vdash \flt Z$}
%}

%\newcommand{\InIfNotRight}{
% \urule{$(\vdash \InIfNot{.})$}
%          {$Z \vdash \flt A $}
%          {$Z \vdash \InIfNot{A} $}
%}

%\newcommand{\InConvLeft}{
% \urule{$(\InConv \vdash)$}
%          {$\conv A \vdash Z $}
%          {$\InConv A \vdash Z$}
%}

%\newcommand{\InConvRight}{
% \urule{$(\vdash \ \InConv)$}
%          {$Z \vdash \conv A $}
%          {$Z \vdash \ \InConv A $}
%}

%\newcommand{\InNButLeft}{
% \urule{$(\InNBut \vdash)$}
%          {$A \rht B \vdash Z$}
%          {$A \InNBut B \vdash Z$}
%}

%\newcommand{\InNButRight}{
% \brule{$(\vdash \InNBut)$}
%          {$A \vdash X $}
%          {$Y \vdash B $}
%          {$X \rht Y \vdash A \InNBut B$}

%}

%\newcommand{\InButNRight}{
% \brule{$(\vdash \InButN)$}
%          {$X \vdash A$}
%          {$B \vdash Y$}
%          {$X \lft Y \vdash A \InButN B$}
%}

%\newcommand{\InButNLeft}{
% \urule{$(\InButN \vdash)$}
%          {$A \lft B \vdash Z$}
%          {$A \InButN B \vdash Z$}
%}

%\newcommand{\InImpLeft}{
% \brule{$(\InImp \vdash)$}
%          {$X \vdash A $}
%          {$B \vdash Y $}
%          {$A \InImp B \vdash X \rht Y$}
%}

%\newcommand{\InImpRight}{
% \urule{$(\vdash \InImp)$}
%          {$Z \vdash A \rht B $}
%          {$Z \vdash A \InImp B$}
%}

%\newcommand{\InIfLeft}{
% \brule{$(\InIf \vdash)$}
%          {$A \vdash X $}
%          {$Y \vdash B $}
%          {$A \InIf B \vdash X \lft Y$}
%}

%\newcommand{\InIfRight}{
% \urule{$(\vdash \InIf)$}
%          {$Z \vdash A \lft B $}
%          {$Z \vdash A \InIf B$}
%}

%\newcommand{\InAndLeft}{
% \urule{$(\InAnd \vdash)$}
%          {$A \semic B \vdash Z $}
%          {$A \InAnd B \vdash Z$}
%}

%\newcommand{\InAndRight}{
% \brule{$(\vdash \InAnd)$}
%          {$X \vdash A $}
%          {$Y \vdash B$}
%          {$X \semic Y \vdash A \InAnd B $}
%}

%\newcommand{\InOrRight}{
% \urule{$(\vdash \InOr)$}
%          {$Z \vdash A \semic B$}
%          {$Z \vdash A \InOr B$}
%}

%\newcommand{\InOrLeft}{
% \brule{$(\InOr \vdash)$}
%          {$A \vdash X $}
%          {$B \vdash Y$}
%          {$A \InOr B \vdash X \semic Y $}
%}

%\newcommand{\ExAndLeft}{
% \urule{$(\ExAnd \vdash)$}
%          {$A \vdash Z $}
%          {$A \ExAnd B \vdash Z$}
% \urule{}
%          {$B \vdash Z $}
%          {$A \ExAnd B \vdash Z$}
%}

%\newcommand{\ExAndRight}{
% \brule{$(\vdash \ExAnd)$}
%          {$Z \vdash A$}
%          {$Z \vdash B$}
%          {$Z \vdash A \ExAnd B $}
%}

%\newcommand{\ExOrLeft}{
% \brule{$(\ExOr \vdash)$}
%          {$A \vdash Z$}
%          {$B \vdash Z$}
%          {$A \ExOr B \vdash Z$}
%}

%\newcommand{\ExOrRight}{
% \urule{$(\vdash \ExOr)$}
%          {$Z \vdash A$}
%          {$Z \vdash A \ExOr B $}
% \urule{}
%          {$Z \vdash B$}
%          {$Z \vdash A \ExOr B $}
%}

%\newcommand{\ExTopLeft}{
% \urule{$(\vdash \ExTop)$}
%          {$\ExTpBt \vdash Z $}
%          {$\ExTop \vdash Z $}
%}

%\newcommand{\ExTopRight}{
%\idrule{$(\vdash \ExTop)$}{$\ExTpBt \vdash \ExTop$}
%}

%\newcommand{\ExBotRight}{
%\urule{$(\vdash \ExBot)$}
%      {$Z \vdash \ExTpBt$}
%      {$Z \vdash \ExBot$}
%}

%\newcommand{\ExBotLeft}{
%\idrule{$(\ExBot \vdash)$}{$\ExBot \vdash \ExTpBt$}
%}

%\newcommand{\id}{
%\idrule{(id)}{$p \vdash p$}
%}

%\newcommand{\cut}{
%\mystrut{(cut)}
%\bpf
%\A ; "$X \vdash A$" 
%\A ; "$A \vdash Y$" 
%\B ; "$X \vdash Y$"  
%\epf
%}


%\newcommand{\BlkBlobWkFirstLeft}{
% \urule{$(\blkb \Wk~1 \vdash)$}
%       {$\blkb X \vdash Z$}
%       {$\blkb X \semic \blkb Y \vdash Z$}
%}     
%\newcommand{\BlkBlobWkFirstRight}{
% \urule{$(\vdash \blkb\Wk~1)$}
%       {$Z \vdash \blkb X$}
%       {$Z \vdash \blkb X \semic \blkb Y$}
%}
%\newcommand{\BlkBlobWkSecondLeft}{
% \urule{$(\blkb\Wk~2 \vdash)$}
%       {$\blkb Y \vdash Z$}
%       {$(\blkb X) \semic (\blkb Y) \vdash Z$}
%} 
%\newcommand{\BlkBlobWkSecondRight}{
% \urule{$(\vdash\blkb\Wk~2)$}
%       {$Z \vdash \blkb Y$}
%       {$Z \vdash (\blkb X) \semic (\blkb Y)$}
%}
%\newcommand{\BlkBlobCtrLeft}{
% \urule{$(\blkb\Ctr \vdash)$}
%       {$(\blkb X) \semic (\blkb X) \vdash Z$}
%       {$\blkb X \vdash Z$}
%}     
%\newcommand{\BlkBlobCtrRight}{
% \urule{$(\vdash \blkb\Ctr )$}
%       {$Z \vdash (\blkb X) \semic (\blkb X)$}
%       {$Z \vdash \blkb X$}

%}

%\newcommand{\BangLeft}{
% \urule{$(\Bang \vdash)$}
%          {$\blkb A \vdash Z $}
%          {$\Bang A \vdash Z$}
%}

%\newcommand{\BangRight}{
% \urule{$(\vdash \Bang)$}
%          {$Z \vdash  A $}
%          {$\blkb Z \vdash \Bang A $}
%}

%\newcommand{\GnabLeft}{
% \urule{$(\Gnab \vdash)$}
%          {$ A \vdash Z $}
%          {$\Gnab A \vdash \blkb Z$}
%}

%\newcommand{\GnabRight}{
% \urule{$(\vdash \Gnab)$}
%          {$Z \vdash  \blkb A $}
%          {$ Z \vdash \Gnab A $}
%}

%\newcommand{\Dens}{\mbox{ Dens }}
%\newcommand{\Pers}{\mbox{ Pers }}

%\newcommand{\BlkBlobDensLeft}{
% \urule{$(\Dens\blkb \vdash)$}
%       {$\blkb \blkb X \vdash Y$}
%       {$\blkb X \vdash Y$}
%}  
%\newcommand{\BlkBlobDensRight}{
% \urule{$(\vdash \Dens\blkb)$}
%       {$ X \vdash \blkb \blkb Y$}
%       {$ X \vdash \blkb Y$}
%}
%\newcommand{\BlkBlobPersLeft}{
% \urule{$(\Pers\blkb \vdash)$}
%       {$ X \vdash Y$}
%       {$\blkb X \vdash Y$}
%}  
%\newcommand{\BlkBlobPersRight}{
% \urule{$(\vdash \Pers\blkb)$}
%       {$ X \vdash  Y$}
%       {$ X \vdash  \blkb Y$}
%}

%\newcommand{\BlkBlobInTpBtPlusRight}{
% \invrule{$(\vdash \blkb\InTpBt^{+}_{-})$}
%       {$ X \vdash  \InTpBt$}
%       {$ X \vdash  \blkb \InTpBt$}
%}
%\newcommand{\BlkBlobInTpBtPlusLeft}{
% \invrule{$(\blkb\InTpBt^{+}_{-} \vdash)$}
%       {$ \InTpBt \vdash  X $}
%       {$ \blkb \InTpBt \vdash X$}
%}

%\newcommand{\BlkBlobComRight}{
% \invrule{$(\vdash \blkb \Com )$}
%       {$ Z \vdash \blkb Y \semic X $}
%       {$ Z \vdash  X \semic \blkb Y$}
%}
%\newcommand{\BlkBlobComLeft}{
% \invrule{$(\blkb \Com \vdash)$}
%       {$ \blkb Y \semic X \vdash Z$}
%       {$ X \semic \blkb Y \vdash  Z$}
%}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: