\documentclass{lecture}

\usepackage{amsmath}
\usepackage{latexsym}
\usepackage{amssymb}
%\usepackage{proof}
\usepackage{exptrees}

%\input{/home/arp/disk1/rpg/papers/relalg/csl96/defs}

\newcommand{\mytilde}{\scriptstyle\sim}

\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree

%%%%% Rule Forming Commands

\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{\Drel}{\mbox{\bf DRA }}
\newcommand{\Lg}[1]{\mbox{$\bf #1$}}

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

\newcommand{\stc}{\bullet}

\newcommand{\blob}{\bullet}

\newcommand{\mcyl}{\raisebox{0.2ex}{\bf c}}
\newcommand{\mor}{+}
\newcommand{\mand}{\circ}
\newcommand{\mnot}{\sim}
\newcommand{\mimp}{\rightarrow}
\newcommand{\mif}{\leftarrow}
\newcommand{\mtop}{\mbox{\bf 1}}
\newcommand{\mbot}{\mbox{\bf 0}}
%\newcommand{\myzero}{\mbox{\bf 0}}
\newcommand{\mstar}{\bigstar}

\newcommand{\mcal}[1]{\mbox{$\cal #1$}}

\newcommand{\btop}{\top}
\newcommand{\bbot}{\bot}
\newcommand{\bor}{\vee}
\newcommand{\band}{\wedge}
\newcommand{\bnot}{\neg}
\newcommand{\bimp}{\supset}

\newcommand{\conv}{\smallsmile}
\newcommand{\semic}{\mbox{ ; }}
\newcommand{\comma}{\raisebox{0.5ex}{ , }}
%\newcommand{\colon}{\mbox{ : }}
\newcommand{\myE}{ E }

\newcommand{\Dl}[1]{\mbox{$\bf \mathbf{\delta}#1$}}
\newcommand{\eqded}{\dashv \vdash}

\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 X \vdash Y$}{$X \vdash Y$}
}

\newcommand{\AstAstRight}{
 \invrule{ }{$X \vdash \ast \ast Y$}{$X \vdash 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{\ConvAstLeft}{
 \invrule{ }{$\stc \ast X \vdash Y$}{$\ast \stc X \vdash Y$}
}

\newcommand{\PTwoAstConvLeft}{
 \invrule{ }{$X \vdash Y$}{$\ast \stc \ast \stc X \vdash Y$}
}

\newcommand{\PTwoAstConvRight}{
 \invrule{ }{$Y \vdash X $}{$Y \vdash \ast \stc \ast \stc X $}
}

\newcommand{\ConvAstRight}{
 \invrule{ }{$X \vdash \stc \ast Y$}{$X \vdash \ast \stc Y$}
}

\newcommand{\ResidTwoLeft}{
 \doubleinvrule{ }{$X \vdash \ast (\ast Z \semic \stc Y)$}
                  {$X \semic Y \vdash Z$}
                  {$Y \vdash \ast (\stc X \semic \ast Z)$}
}

\newcommand{\ResidTwoRight}{
 \doubleinvrule{ }{$\ast (\ast Z \semic \stc Y) \vdash X $}
                  {$Y \vdash Z \semic X $}
                  {$\ast (\stc X \semic \ast Z) \vdash Y $}
}

\newcommand{\ResidOneLeft}{
 \doubleinvrule{ }{$X \vdash \ast \stc (Y \semic \ast \stc Z)$}
                  {$X \semic Y \vdash Z$}
                  {$Y \vdash \ast \stc (\ast \stc  Z \semic X)$}
}

\newcommand{\ResidOneRight}{
 \doubleinvrule{ }{$\ast \stc (Y \semic \ast \stc Z) \vdash X $}
                  {$Z \vdash X \semic Y$}
                  {$\ast \stc (\ast \stc  Z \semic X) \vdash Y $}
}

\newcommand{\dpcircleRight}{
 \doubleinvrule{ }{$\ast (\ast Z \semic \stc Y) \vdash X $}
                  {$Z \vdash X \semic Y$}
                  {$\ast (\stc X \semic \ast Z) \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 \,\,\,$}
}

\newcommand{\ConvDistrLeft}{
 \invrule{ }{$\stc (X \semic Y) \vdash Z$}
            {$(\stc Y) \semic (\stc X) \vdash Z$}
}

\newcommand{\ConvDistrRight}{
 \invrule{ }{$Z \vdash \stc (X \semic Y) $}
            {$Z \vdash (\stc Y) \semic (\stc X) $}
}


\newcommand{\dpstccircRight}{
 \invrule{ }{$Z \vdash \stc (X \semic Y) $}
            {$Z \vdash (\stc Y) \semic (\stc X) $}
}

\newcommand{\Tagging}{
 \urule{(tag)}{$X \semic Y \vdash Z $}
            {$\stc Y \semic \stc X \vdash \stc Z$}
}

\newcommand{\TagInvLeft}{
 \urule{$(taginv \vdash)$}{$\stc Y \semic \stc X \vdash \stc Z$}
              {$X \semic Y \vdash Z $}
}            

\newcommand{\TagInvRight}{
 \urule{$(\vdash taginv)$}{$\stc Z \vdash \stc Y \semic \stc X $}
              {$Y \vdash Z \semic X $}
}            

\newcommand{\ConvmyELeft}{
 \invrule{($\stc \myE \vdash$)}{$\myE \vdash X$}
            {$\stc \myE \vdash X$}
}

\newcommand{\ConvmyERight}{
 \invrule{($\vdash \stc \myE$)}{$X \vdash \myE$}
            {$X \vdash \stc \myE$}
}

\newcommand{\ConvTopLeft}{
 \invrule{($\stc I \vdash$)}{$I \vdash X$}
            {$\stc I \vdash X$}
}

\newcommand{\ConvTopRight}{
 \invrule{($\vdash \stc I$)}{$X \vdash I$}
            {$X \vdash \stc I$}
}

\newcommand{\CommaAssLeft}{
 \invrule{($A \vdash$)}{$X \comma  (Y  \comma  Z) \vdash W$}
            {$(X  \comma  Y) \comma  Z \vdash W$}
}

\newcommand{\CommaAssRight}{
 \invrule{($\vdash A$)}{$W \vdash X \comma  (Y  \comma  Z)$}
            {$W \vdash (X  \comma  Y) \comma  Z $}
}

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

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

\newcommand{\CommaComLeft}{
 \urule{($P \vdash$)}{$Y  \comma  X \vdash Z $}
            {$X  \comma  Y \vdash Z $}
}

\newcommand{\CommaComRight}{
 \urule{($\vdash P$)}{$Z \vdash Y  \comma  X $}
            {$Z \vdash X  \comma  Y $}
}

\newcommand{\CommaContLeft}{
 \urule{($C \vdash$)}{$X  \comma  X \vdash Z $}
            {$X  \vdash Z $}
}

\newcommand{\CommaContRight}{
 \urule{($\vdash C$)}{$Z \vdash X  \comma  X $}
            {$Z \vdash X $}
}

\newcommand{\CommaWeakLeft}{
 \urule{($M \vdash$)}{$X \vdash Z $}
            {$X  \comma  Y \vdash Z $}
}

\newcommand{\CommaWeakRight}{
 \urule{($\vdash M$)}{$Z \vdash X $}
            {$Z \vdash X \comma  Y$}
}


\newcommand{\AntiLogLeft}{
 \invrule{$(alg \vdash)$}{$X \semic Y \vdash Z $}
            {$\ast \stc Z \semic X \vdash \ast \stc Y$}
}

\newcommand{\AntiLogRight}{
 \invrule{$(\vdash alg)$}{$Z \vdash X \semic Y $}
            {$\ast \stc Y \vdash \ast \stc Z \semic X $}
}

\newcommand{\myEPlusMinusLeft}{
 \doubleinvrule{$(\myE^{+}_{-} \vdash)$}
               {$X \semic \myE \vdash Y$}
               {$X \vphantom{\semic} \vdash Y $}
               {$\myE \semic X \vdash Y$}
}

\newcommand{\myEPlusMinusRight}{
 \doubleinvrule{$(\vdash \myE^{+}_{-})$}
               {$X \vdash \myE \semic Y $}
               {$X \vphantom{\semic} \vdash Y $}
               {$X \vdash Y \semic \myE $}
}


\newcommand{\IPlusMinusLeft}{
 \doubleinvrule{$(I^{+}_{-} \vdash)$}
               {$X \comma I \vdash Y$}
               {$X \vdash Y $}
               {$I \comma X \vdash Y$}
}

\newcommand{\IPlusMinusRight}{
 \doubleinvrule{$(\vdash I^{+}_{-} )$}
               {$X \vdash I \comma Y $}
               {$X \vdash Y $}
               {$X \vdash Y \comma I $}
}


\newcommand{\ExI}{
 \urule{(ExI)}
          {$X \vdash I$}
          {$X \vdash Y$}
}

\newcommand{\VerI}{
 \urule{(VerI)}
          {$I \vdash X$}
          {$Y \vdash X$}
}

\newcommand{\mtopLeft}{
 \urule{$(\mtop \vdash)$}
          {$\myE \vdash Z $}
          {$\mtop \vdash Z$}
}

\newcommand{\mtopRight}{
 \idrule{$(\vdash \mtop)$}{$E \vdash \mtop$}
}

\newcommand{\mbotRight}{
 \urule{$(\vdash \mbot)$}
          {$Z \vdash \myE $}
          {$Z \vdash \mbot$}
}

\newcommand{\mbotLeft}{
 \idrule{$(\mbot \vdash)$}{$\mbot \vdash E $}
}

\newcommand{\mnotLeft}{
 \urule{$(\mnot \vdash)$}
          {$\ast \stc A \vdash Z $}
          {$\mnot A \vdash Z$}
}

\newcommand{\mnotRight}{
 \urule{$(\vdash \mnot)$}
          {$Z \vdash \ast \stc A $}
          {$Z \vdash \mnot A $}
}

\newcommand{\convLeft}{
 \urule{$(\conv \vdash)$}
          {$\stc A \vdash Z $}
          {$\conv A \vdash Z$}
}

\newcommand{\convRight}{
 \urule{$(\vdash \conv)$}
          {$Z \vdash \stc A $}
          {$Z \vdash \conv A $}
}

\newcommand{\mimpLeft}{
 \brule{$(\mimp \vdash)$}
          {$X \vdash A $}
          {$B \vdash Y $}
          {$A \mimp B \vdash \ast \stc X \semic Y$}
}

\newcommand{\mimpRight}{
 \urule{$(\vdash \mimp)$}
          {$A \semic X \vdash B $}
          {$X \vdash A \mimp B$}
}

\newcommand{\mifLeft}{
 \brule{$(\mif \vdash)$}
          {$B \vdash Y $}
          {$X \vdash A $}
          {$B \mif A \vdash Y \semic  \ast \stc X$}
}

\newcommand{\mifRight}{
 \urule{$(\vdash \mif)$}
          {$X \semic A \vdash B $}
          {$X \vdash B \mif A$}
}


\newcommand{\compLeft}{
 \urule{$(\circ \vdash)$}
          {$A \semic B \vdash Z $}
          {$A \circ B \vdash Z$}
}

\newcommand{\compRight}{
 \brule{$(\vdash \circ)$}
          {$X \vdash A $}
          {$Y \vdash B$}
          {$X \semic Y \vdash A \circ B $}
}

\newcommand{\morRight}{
 \urule{$(\vdash \mor)$}
          {$Z \vdash A \semic B$}
          {$Z \vdash A \mor B$}
}

\newcommand{\morLeft}{
 \brule{$(\mor \vdash)$}
          {$A \vdash X $}
          {$B \vdash Y$}
          {$A \mor B \vdash X \semic Y $}
}

\newcommand{\bnotLeft}{
 \urule{$(\bnot \vdash)$}
          {$\ast A \vdash Z $}
          {$\bnot A \vdash Z$}
}

\newcommand{\bnotRight}{
 \urule{$(\vdash \bnot)$}
          {$Z \vdash \ast A $}
          {$Z \vdash \bnot A $}
}

\newcommand{\bimpLeft}{
 \brule{$(\bimp \vdash)$}
          {$X \vdash A $}
          {$B \vdash Y $}
          {$A \bimp B \vdash \ast X \comma Y$}
}

\newcommand{\bimpRight}{
 \urule{$(\vdash \bimp)$}
          {$A \comma X \vdash B $}
          {$X \vdash A \bimp B$}
}


\newcommand{\bandLeft}{
 \urule{$(\band \vdash)$}
          {$A \comma  B \vdash Z $}
          {$A \band B \vdash Z$}
}

\newcommand{\bandRight}{
 \brule{$(\vdash \band)$}
          {$X \vdash A$}
          {$Y \vdash B$}
          {$X \comma Y \vdash A \band B $}
}

\newcommand{\borLeft}{
 \brule{$(\bor \vdash)$}
          {$A \vdash X$}
          {$B \vdash Y$}
          {$A \bor B \vdash X \comma Y$}
}

\newcommand{\borRight}{
 \urule{$(\vdash \bor)$}
          {$Z \vdash A \comma B$}
          {$Z \vdash A \bor B $}
}

\newcommand{\BTopLeft}{
 \urule{$(\vdash \btop)$}
          {$I \vdash Z $}
          {$\btop \vdash Z $}
}

\newcommand{\BTopRight}{
\idrule{$(\vdash \btop)$}{$I \vdash \btop$}
}

\newcommand{\BBotRight}{
\urule{$(\vdash \bbot)$}
      {$X \vdash I$}
      {$X \vdash \bbot$}
}

\newcommand{\BBotLeft}{
\idrule{$(\bbot \vdash)$}{$\bbot \vdash I$}
}

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

\newcommand{\cut}{
\brule{(cut)}
      {$X \vdash A$} 
      {$A \vdash Y$} 
      {$X \vdash Y$} 
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Modal Axioms

\newcommand{\Refl}{
 \urule{(T)}
       {$\blkb X \vdash Y $}
       {$ X \vdash Y$}
}

\newcommand{\Trans}{
 \urule{(4)}
       {$\blkb X \vdash Y $}
       {$\blkb \blkb X \vdash Y$}
}

\newcommand{\Sym}{
 \urule{(B)}
       {$\blkb X \vdash Y $}
       {$ \ast \blkb \ast X \vdash Y$}
}


\begin{document}


\title{ }
\begin{slide}
  \begin{Heading}
Formalising Cut-elimination for the Display Calculus of Relation Algebras
  \end{Heading}

\begin{center}
\begin{tabular*}{\linewidth}{@{}l@{\extracolsep{\fill}}l@{}} 
\multicolumn{2}{c}{Jeremy E.\ Dawson and Rajeev Gor\'{e}}
\\ \\
Automated Reasoning Group      & Formal Methods Group                 \\
Computer Sciences Laboratory   & Dept.\ of Computer Science           \\
Res.\ Sch.\ of Inf.\ Sci.\ and Eng.\ & Fac.\ of Eng.\ and Inf.\ Tech. \\
Institute of Advanced Studies  & The Faculties                        \\
\multicolumn{2}{c}{Australian National University}                    \\
\texttt{jeremy@arp.anu.edu.au} \hspace{1cm}  &
                                  \texttt{rpg@arp.anu.edu.au}         \\
\texttt{arp.anu.edu/{\small$\mytilde$}jeremy} &
                        \texttt{arp.anu.edu.au/{\small$\mytilde$}rpg} \\
\end{tabular*}
\end{center}

\begin{itemize}
\small 
\item[ ] Gor{\'e} supported by an Australian Research Council Queen Elizabeth II Fellowship.
   
 \item[ ] Dawson supported by an Australian Research Council Large Research Grant.
\end{itemize}

\end{slide}


\begin{slide}
  \begin{Heading}
    {Display Calculus \Dl{RA} for Relation Algebra}
  \end{Heading}

  \begin{description}
  \item[RA:] Algebra of binary relations (sets of ordered pairs) over underlying set $U$

  \item[Atomic constants:] $c ::= \bbot \mid 
                                  \btop \mid 
                                  \mtop \mid 
                                  \mbot $
                                  \hfill ($\emptyset \mid$
                                  $U \times U \mid$ identity $\mid$ diversity)
    
    
  \item[Atomic formulae:] $p ::=  p_0  \mid 
                                  p_1  \mid 
                                  p_2  \mid 
                                  \cdots$
                                  \hfill (relation symbols)
    
  \item[Formulae:] 
     $A \ B \hfill ::=     \hfill c          \hfill \mid 
                           \hfill p          \hfill \mid 
                           \hfill \bnot A   \hfill \mid 
                           \hfill A \band B \hfill \mid 
                           \hfill A \bor B  \hfill \mid 
                           \hfill \conv A    \hfill \mid 
                           \hfill A \mand B \hfill \mid 
                           \hfill A \mor B$


  \item \hspace{7cm} $U \times U - A$ \hspace{1.2cm} 
                     $\cap$ \hspace{2.1cm}
                     $\cup$ \hspace{1.2cm}
                     converse 
                     composition \hspace{0.1cm}



  \item[Structure:] \hfill 
        $X \ Y \hfill ::= \hfill A          \hfill \mid 
                          \hfill I          \hfill \mid
                          \hfill \ast X     \hfill \mid
                          \hfill X \comma Y \hfill \mid 
                          \hfill E          \hfill \mid 
                          \hfill \blob X    \hfill \mid
                          \hfill X \semic Y \hfill  $

  \item[Sequent:] \hfill $X \vdash Y$ \hfill where $X$ is the
    \defn{antecedent} and $Y$ is the \defn{succedent}

  \item[Sequent rule:] \hfill 
                        \urule{(name)}
                              {$X_1 \vdash Y_1 \cdots X_n \vdash X_n$}
                              {$X \vdash Y$}
                        \hfill
                        \urule{}
                              {\defn{premisses}}
                              {\defn{conclusion}}

  \end{description}
\end{slide}

\begin{slide}
  \begin{Heading}
    { Display Calculus \Dl{RA}: Display Postulates}
  \end{Heading}

  \begin{description}

  \item[ ]
    \begin{picture}(500,160)%(30, 0)
    \thicklines
    \put (0,   120) { \AstLeft }         \put (100,   120) { \AstRight }      
    \put (200, 120) { \AstAstLeft }           
    \put (380,  120) { \ResidConv }      \put (500, 120) { \ConvConvLeft }
    \put (0,    10) { \ResidInt}         \put (160,    10) { \DualResidInt}
    \put (360,  10) { \ResidExt}         \put (500,   10) { \DualResidExt}
    \end{picture}
\vfill
  \item[Theorem (Belnap82):]  For every sequent $X \vdash Y$ and every
    substructure $Z$ of $X \vdash Y$, there is a structurally
    equivalent sequent $Z \vdash Y'$ or $X' \vdash Z$ that has $Z$
    displayed as the whole of its antecedent or succedent.

  \item[e.g.] \urule{}
              {$\ast p_3 \vdash p_0 \semic (p_0 \mand p_1) $}
              {$\ast (p_0 \semic (p_0 \mand p_1)) \vdash p_3$}
         \urule{}
              {$\ast p_3 \semic \ast \blob (p_0 \mand p_1) \vdash p_0 $}
              {$\ast p_3 \vdash p_0 \semic (p_0 \mand p_1) $}
         \urule{}
              {$\ast \blob p_0 \semic p_3 \vdash p_0 \mand p_1$}
              {$\ast p_3 \vdash p_0 \semic (p_0 \mand p_1) $}

  \end{description}
\end{slide}

\begin{slide}
  \begin{Heading}
    { Display Calculus \Dl{RA}: Logical Rules} 
  \end{Heading}

  \begin{itemize}
  \item Left and right introduction rules for every logical connective

%  \item 
%    \begin{picture}(300,580)(0,0)
%    \thicklines
%    \put (0,    540) { \mbotLeft}        \put (200,  530) { \mbotRight}
%    \put (0,    490) { \mtopLeft}        \put (200,  500) { \mtopRight}
%    \put (0,    450) { \compLeft}        \put (200,  450) { \compRight}
%    \put (0,    410) { \morLeft}         \put (200,  410) { \morRight}
%%    \put (0,    370) { \mifLeft}         \put (200,  370) { \mifRight}
%%   \put (0,    330) { \mimpLeft}        \put (200,  330) { \mimpRight}
%    \put (0,    290) { \convLeft}        \put (200,  290) { \convRight}
%    \put (0,    250) { \mnotLeft}        \put (200,  250) { \mnotRight}
%    \put (0,    220) { \BBotLeft}        \put (200,  210) { \BBotRight}
%    \put (0,    170) { \BTopLeft}        \put (200,  180) { \BTopRight}
%    \put (0,    130) { \borLeft}         \put (200,  130) { \borRight}
%    \put (0,     90) { \bandLeft}        \put (200,   90) { \bandRight}
%%    \put (0,     50) { \bimpLeft}        \put (200,   50) { \bimpRight}
%    \put (0,     10) { \bnotLeft}        \put (200,   10) { \bnotRight}
%    \end{picture}

\vspace*{-1em}

  \item $\id$ \hfill $\cut$ 
\vspace*{-0.2em}      
  \item $\morLeft$ \hspace{1.5cm} decoding/rewrite \hspace{1.5cm} $\morRight$
\vspace*{-0.2em}
  \item $\bandLeft$ \hspace{3cm} rewrite/decoding \hspace{0.5cm} $\bandRight$
\vspace*{-0.2em}
  \item Introduced formula is always displayed
\vspace*{-0.2em}
  \item Gentzen overloading:
    \begin{tabular}{ccccccc}
       Antecedent Part & $\btop$ & $\bnot$ & $\band$ & $\mtop$ & $\mnot$ & $\mand$ \\
       Connective & $I$ & $\ast$ & $\comma$ & $\myE$ & $\blob$ & $\semic$ \\
       Succedent Part & $\bbot$ & $\bnot$ & $\bor$ & $\mbot$ &  $\mnot$ & $\mor$
   \end{tabular}
\vspace*{-0.2em}
     \item Example: $\ast (p_0 \semic p_1) \vdash \ast \blob (p_1 \comma
       p_3)$ \hfill $\semic$ is $\mor$ and $\comma$ is $\band$

   \end{itemize}

\end{slide}

\begin{slide}
  \begin{Heading}
    { Display Logic \Dl{RA}: Structural Rules}
  \end{Heading}
  
  A \defn{structural} rule contains no logical connectives and no
  formula variables.
    
  \begin{picture}(600,250)(30,0)
  \thicklines
  
  \put (0,  210) { \SemicAssLeft}    \put (275,  210) { \CommaAssRight}
                                     \put (550,  210) { \CommaComRight}
  \put (0,  100) { \IPlusMinusLeft}  \put (190,  100) { \myEPlusMinusRight}
                                     \put (400,  100) { \ConvmyERight}
                                     \put (570,  100) { \ConvTopLeft}
  \put (0,  0) { \CommaWeakLeft}     \put (300,  0) { \CommaContRight}
                                     \put (550,  0) { \Tagging}         
  \end{picture}

\vfill
  Note: no (M) (P) or (C) rules for $\semic$ since $\mand/\mor$ are
  not classical connectives

\end{slide}

\begin{slide}
  \begin{Heading}
    { Logical Variation Via Structural Rules (modularity)}
  \end{Heading}

  \begin{itemize}
  \item An equation $A \leq B$ is {\bf primitive} iff $A$ and $B$ are
    built from relational variables and the constants $\btop$ and
    $\mtop$ with the help of $\conv$, $\band$, $\bor$ and $\mand$
    only, and if no relational variable appears in $A$ more than once
    (Kracht96).  

  \item[]
    \begin{picture}(600, 80)(20,0)
    \thicklines 
    \put(0,  80) {\mbox{ reflexivity }} 
    \put(160, 80) {\mbox{ seriality}} 
    \put(320, 80) {\mbox{ symmetry}} 
    \put(480, 80) {\mbox{ transitivity}} 
    \put(0,   50) {\mbox{ $(T) \ \mtop \leq A$}}
    \put(140,  50) {\mbox{ $(D) \ A \mand \btop = \btop $}} 
    \put(300, 50) {\mbox{ $(B) \ A = \, \conv\! A$}} 
    \put(460, 50) {\mbox{ $(4) \ A \mand B  \leq A \bor B$}} 
    \put(-10,  0) {\urule{$(T)$}{$X \vdash Z$}
                                {$\myE \vdash Z$}} 
    \put(140,   0) {\invrule{$(D)$}{$I \vdash Z$}
                                  {$X \semic I \vdash Z$}} 
    \put(300,  0) {\invrule{$(B)$}{$\blob X \vdash Z$}
                                  {$X \vdash Z$}} 
    \put(460, 0) {\brule{$(4)$}{$X_{1} \vdash Z$}{$X_{2} \vdash Z$}
                                 {$X_{1} \semic X_{2} \vdash Z$}}
    \end{picture}

  \item Theorem [Belnap~82]: Any display calculus whose rules obey eight
    conditions given by Belnap enjoys cut-elimination. If $X \vdash Y$
    is derivable, then it is derivable without the cut rule.
    
  \item Theorem: Using results of Kracht~96 we can construct a
    \defn{cut-free} display calculus which is sound and complete for
    any primitive extension of RA.

  \end{itemize}
\end{slide}


\begin{slide}
  \begin{Heading}
    {Formalising \Dl{RA} in Isabelle/HOL}
  \end{Heading}

  \begin{itemize}
\item[Formulae:] 
     $A \ B \hfill ::=     \hfill c          \hfill \mid 
                           \hfill p          \hfill \mid 
                           \hfill \bnot A   \hfill \mid 
                           \hfill A \band B \hfill \mid 
                           \hfill A \bor B  \hfill \mid 
                           \hfill \conv A    \hfill \mid 
                           \hfill A \mand B \hfill \mid 
                           \hfill A \mor B$

  \end{itemize}  

\begin{verbatim}
datatype formula = Btimes formula formula ("_ && _" [68,68] 67)
                 | Rtimes formula formula ("_ oo _" [68,68] 67)
                 | Bplus formula formula ("_ v _" [64,64] 63)
                 | Rplus formula formula ("_ ++ _" [64,64] 63)
                 | Bneg formula ("--_" [70] 70)
                 | Rneg formula ("_^" [75] 75)
                 | Btrue ("T")
                 | Bfalse("F")
                 | Rtrue ("r1")
                 | Rfalse("r0")
                 | PP string 
                 | FV string 

\end{verbatim}

\end{slide}


%\begin{slide}
%  \begin{Heading}
%    {Formalising \Dl{RA} in Isabelle/HOL}
%  \end{Heading}

%  \begin{description}
%    \item[Structure:] \hfill 
%        $X \ Y \hfill ::= \hfill A          \hfill \mid 
%                          \hfill I          \hfill \mid
%                          \hfill \ast X     \hfill \mid
%                          \hfill X \comma Y \hfill \mid 
%                          \hfill E          \hfill \mid 
%                          \hfill \blob X    \hfill \mid
%                          \hfill X \semic Y \hfill  $

%     \item[Sequent rule:] \hfill 
%                        \urule{(name)}
%                              {$X_1 \vdash Y_1 \cdots X_n \vdash X_n$}
%                              {$X \vdash Y$}
%                        \hfill
%                        \urule{}
%                              {\defn{premisses}}
%                              {\defn{conclusion}}

%  \end{description}

%\begin{verbatim}
%datatype structr = Comma structr structr 
%                 | SemiC structr structr 
%                 | Star structr  
%                 | Blob structr  
%                 | I | E | Structform formula | SV string   

%datatype sequent = Sequent structr structr       

%datatype rule = Rule (sequent list) sequent 
%              | Bidi sequent sequent
%              | InvBidi sequent sequent 
%\end{verbatim}
  
%\end{slide}


%\begin{slide}
%  \begin{Heading}
%    {Example Rules}
%  \end{Heading}
  
%  Some purely syntactic operators, together with
%  \texttt{print-translation} and \texttt{parse-translation} allow
%  \texttt{Sequent (SV ''X'') ''Y''} to be written as \\
%  \texttt{\$X |- \$Y}

%\vfill

%\invrule{}{$X \vdash Y \semic Z$}{$\ast \blob Y \semic X \vdash Z$}

%\begin{verbatim}
%  defs
%      ss1   "ss1 == Bidi ($''X'' |- $''Y''; $''Z'') 
%                         ( *@$''Y''; $''X'' |- $''Z'')"  
%\end{verbatim}

%\end{slide}


\begin{slide}
  \begin{Heading}
    {Formalising \Dl{RA} in Isabelle/HOL}
  \end{Heading}

  \begin{description}
    \item[Structure:] \hfill 
        $X \ Y \hfill ::= \hfill A          \hfill \mid 
                          \hfill I          \hfill \mid
                          \hfill \ast X     \hfill \mid
                          \hfill X \comma Y \hfill \mid 
                          \hfill E          \hfill \mid 
                          \hfill \blob X    \hfill \mid
                          \hfill X \semic Y \hfill  $

  \end{description}

\begin{verbatim}
datatype structr = Comma structr structr                '
                 | SemiC structr structr                ;
                 | Star structr                         *
                 | Blob structr                         @
                 | I                                    $I
                 | E                                    $E
                 | Structform formula          
                 | SV string                            $''X''
\end{verbatim}

 \texttt{datatype sequent = Sequent structr structr} \hfill \texttt{|-}
 
 \texttt{\$''X'' |- ''A''} via \texttt{print-translation} and
 \texttt{parse-translation} becomes
 \texttt{Sequent (SV ''X'') (Structform (FV ''A''))}
  
\end{slide}

\begin{slide}
  \begin{Heading}
    {A Deep Embedding of Rules}
  \end{Heading}

  \urule{(name)}{$X_1 \vdash Y_1 \cdots X_n \vdash X_n$}
                      {$X \vdash Y$}
        \hfill
  \invrule{}{$X \vdash Y \semic Z$}
            {$\ast \blob Y \semic X \vdash Z$}

  \begin{verbatim}
    datatype rule = Rule (sequent list) sequent 
                  | Bidi sequent sequent
                  | InvBidi sequent sequent 
  \end{verbatim}

  \begin{verbatim}
    ss1   "ss1 == Bidi ($''X'' |- $''Y''; $''Z'')
                       ( *@$''Y''; $''X'' |- $''Z'')"
  \end{verbatim}

Deep embedding because of the \texttt{''X''}. Shallow embedding would use \texttt{?X}.

This means we must handle substitutions explicitly.

%\texttt{seqRep b X Y seq1 seq2} holds if 
%\texttt{seq1} and \texttt{seq2} are the same, except that (possibly)
%one or more occurrences of \texttt{X} in \texttt{seq1} appear as
%corresponding occurrences of \texttt{Y} in \texttt{seq2},
%where such differences occur only in succedent (antecedent) positions,
%according as \texttt{b} is \texttt{True} or \texttt{False}. 

\end{slide}

\begin{slide}
  \begin{Heading}
    {Formalising Derivations}
  \end{Heading}
  
\begin{verbatim}
datatype pftree = Pr sequent rule (pftree list) 
                | Unf sequent 
\end{verbatim}

Leaves of successful derivation have form 
\texttt{Pr (''A'' |- ''A'') id  []} 

A derived rule will have some \texttt{Unf}inished leaf sequents

\texttt{wfb :: "pftree => bool"} returns true if the end-sequent of
\texttt{pftree} and the end-sequents of its immediate children in
\texttt{pftree list} are a well-formed instance of \texttt{rule} 

\texttt{allPT :: "(pftree => bool) => pftree => bool"} returns true if
every node of \texttt{pftree} satisfies the given boolean valued
function

\texttt{allPT wfb} returns true if every rule application in
\texttt{pftree} is well formed

\texttt{allPT (frb rules)} returns true if every rule application in
\texttt{pftree} is a member of set \texttt{rules}

\end{slide}

\begin{slide}
  \begin{Heading}
    {Formalising Derivations}
  \end{Heading}
  
\texttt{IsProvableR :: "rule set => [sequent set, sequent] => bool"}

\begin{verbatim}
idf_der = "IsProvableR rls {} (?p |- ?p)"

 "IsProvableR rules prems concl == (? pftr.
    allPT (frb rules) pftr & allPT wfb pftr &
    conclPT pftr = concl & set (premsPT pftr) <= prems)"

"IsProvable rules (Rule prems concl) = 
        IsProvableR rules (set prems) concl"
\end{verbatim}
  
\end{slide}


\begin{slide}
  \begin{Heading}
    {Reducing a Left-and-Right Principal Cut}
  \end{Heading}
  
  \begin{itemize}
  \item A cut on $A$ is \defn{left- [right-] principal} if the left [right]
    inference immediately above the cut introduces $A$ via a logical
    rule, written $(\vdash A)$ [$(A \vdash)$]


  \item[ ]
         \begin{center}{\small
         \vpf
         \bpf
           \A "$\Pi_{L}$"
           \U "$X \vdash A$" "($\vdash A$)"
           \A "$\Pi_{R}$"
           \U "$A \vdash Y$" "($A \vdash$)"
           \B "$X \vdash Y$"
         \epf
         }\end{center}

  \item C8: All left-and-right principal cuts can be replaced by cuts
    on strictly smaller subformulae of $A$


   \item Base Case:
   \brule{(cut)}
         {$p \vdash p$}
         {$p \vdash p$}
         {$p \vdash p$} reduced to just $p \vdash p$

    \item Similar cases for $\btop$, $\mtop$, $\bbot$, $\mbot$
      
  \end{itemize}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Example of C8 condition}
  \end{Heading}
  
{\small
\vpf
\bpf
\A "$\Pi_{ZAB}$"
\U "$Z \vdash A, B$"
\U "$Z \vdash A \bor B$" "($\vdash \bor $)"
\A "$\Pi_{AX}$"
\U "$A \vdash X$"
\A "$\Pi_{BY}$"
\U "$B \vdash Y$"
\B [1em] "$A \bor B \vdash X, Y$" "($\bor \vdash $)"
\B [2em] "$Z \vdash X, Y$" "($cut$)"
\U ['] "Principal cut on formula $A \bor B$"
\epf
\hfill
\vpf
\bpf
\A "$\Pi_{ZAB}$"
\U "$Z \vdash A, B$"
\U "$*A, Z \vdash B$" "(dp)"
\A "$\Pi_{BY}$"
\U "$B \vdash Y$"
\B [2em] "$*A, Z \vdash Y$" "($cut$)"
\U "$Z \vdash A, Y$" "(dp)"
\U "$Z, *Y \vdash A$" "(dp)"
\A "$\Pi_{AX}$"
\U "$A \vdash X$"
\B [2em] "$Z, *Y \vdash X$" "($cut$)"
\U "$Z \vdash X, Y$" "(dp)"
\U ['] "Transformed derivation uses cuts only on $A$ and $B$"
\epf
}

\vfill

Must exhibit and hard-wire such transformations for every logical connective

So if cut is \defn{not} left-and-right principal then we try to make
it so ...

\end{slide}

\begin{slide}
  \begin{Heading}
    {Making a cut left-principal}
  \end{Heading}
  
  \begin{itemize}

  \item Given a derivation ending in a non left-and-right principal
    cut on formula $A$, we trace the ancestor occurrences of this $A$
    up $\Pi_{L}$:

  \item[ ]
         \begin{center}{\small
         \vpf
         \bpf
           \A "$\Pi_{L}$"
           \U "$X \vdash A$" 
           \A "$\Pi_{R}$"
           \U "$A \vdash Y$" 
           \B "$X \vdash Y$"
         \epf
         }\end{center}

     
   \item an ancestor of $A$ is \defn{principal} if introduced by
     logical rule $(\vdash A)$
     
   \item all other ancestors of $A$ are \defn{parametric} ancestors
     (including those ``introduced'' by weakening
     
   \item there must be at least one introduction of $A$ in every
     branch
     
   \item not all occurrences of $A$ need be ancestors of this
     occurrence of $A$

  \end{itemize}

\end{slide}

\begin{slide}
  \begin{Heading}
    {Making a cut left-principal}
  \end{Heading}
  
  \begin{itemize}

  \item Given a derivation ending in a non left-and-right principal
    cut on formula $A$, we trace the ancestor occurrences of this $A$
    up $\Pi_{L}$:

  \item Let $\Pi[A := Y]$ mean ``replace all parametric ancestors of $A$
  with $Y$'' 

  \item Suppose $\Pi_L$ does not branch at all for simplicity

  \item[]
    \begin{center}
      {\small
      \bpf
      \A "$\Pi^{1}_{L}$"
      \U "$V \vdash A $" "($\vdash A$)"
      \U "$\Pi^{2}_{L}$" "($\pi$)"
      \U "$X \vdash A $" "($\rho$)"
      \A "$\Pi_R$"
      \U "$A \vdash Y$" 
      \B [2em] "$X \vdash Y$" "($cut$)"
      \epf
      \qquad \qquad
      \bpf
      \A "$\Pi^{1}_{L}$"
      \U "$V \vdash A $" "($\vdash A$)"
      \A "$\Pi_R$"
      \U "$A \vdash Y$" 
      \B [2em] "$V \vdash Y$" "($cut$)"
      \U "$\Pi^{2}_L[A := Y]$" "($\pi$)"
      \U "$X \vdash Y $" "($\rho$)"
      \epf
      }
    \end{center}

  \item New cut is left-principal
  \end{itemize}

\end{slide}


\begin{slide}
  \begin{Heading}
    {Making a cut left-principal}
  \end{Heading}
  
  \begin{itemize}

  \item Base case of induction, $\Pi^{1}_{L}$ is empty, $A$ introduced
    by $A \vdash A$. No new cuts needed
  \item[]
      {\small
      \vpf
      \bpf
      \A "$A \vdash A $" 
      \U "$\Pi^{2}_{L}$" "($\pi$)"
      \U "$X \vdash A $" "($\rho$)"
      \A "$\Pi_R$"
      \U "$A \vdash Y$" 
      \B [2em] "$X \vdash Y$" "($cut$)"
      \epf
      \qquad \qquad \qquad \qquad
      \bpf
      \A "$\Pi_R$"
      \U "$A \vdash Y$" 
      \U "$\Pi^{2}_L[A := Y]$" "($\pi$)"
      \U "$X \vdash Y $" "($\rho$)"
      \epf
      }

  \item Case for ``introduction'' by weakening, no new cuts needed

      {\small
      \vpf
      \bpf
      \A "$\Pi^{1}_{L}$"
      \U "$V \vdash W \comma Z(A) $" "(Wk $Z(A)$)"
      \U "$\Pi^{2}_{L}$" "($\pi$)"
      \U "$X \vdash A $" "($\rho$)"
      \A "$\Pi_R$"
      \U "$A \vdash Y$" 
      \B [2em] "$X \vdash Y$" "($cut$)"
      \epf
      \qquad \qquad
      \bpf
      \A "$\Pi^{1}_{L}$"
      \U "$V \vdash W \comma Z(Y) $" "(Wk $Z(A := Y)$)"
      \U "$\Pi^{2}_L[A := Y]$" "($\pi$)"
      \U "$X \vdash Y $" "($\rho$)"
      \epf
      }

  \end{itemize}

\end{slide}

\begin{slide}
  \begin{Heading}
    {Putting It All Together}
  \end{Heading}
  
\begin{verbatim}
  canElim      :: "(pftree => bool) => bool"
  canElimAll   :: "(pftree => bool) => bool"
\end{verbatim}

\texttt{canElim f} means that if a derivation tree \texttt{pt}
has no cuts other than
at the bottom, and satisfies \texttt{f}, then there is an equivalent 
cut-free derivation tree.

\texttt{canElimAll f} means that if every subtree of a given tree
\texttt{pt} satisfies \texttt{f}, then there is a cut-free derivation
tree \texttt{pt'} equivalent to \texttt{pt} (we also require that if
the bottom rule of \texttt{pt} is not (\textit{cut}), then the bottom
rule of \texttt{pt'} is the same).

\begin{verbatim}
allLP' = "canElimAll (cutIsLP ?A) ==> canElim (cutOnFmls {?A})" 
\end{verbatim}

Here \texttt{f} is \texttt{(cutIsLP ?A)} [\texttt{(cutOnFmls \{?A\})}]
which means that if the lowest rule application is cut then it is a
left-principal cut with cut formula \texttt{?A} \mbox{[if the lowest rule
application is cut then the cut formula is from set \texttt{\{?A\}}]}

\texttt{allLP'} means ``if you can eliminate several cuts, all
left-principal on $A$, then you can eliminate a single cut, at the
bottom, on $A$'' \hfill (its backwards!)
\end{slide}

\begin{slide}
  \begin{Heading}
    {Putting It All Together ...}
  \end{Heading}

\begin{verbatim}
allLP' = "canElimAll (cutIsLP ?A) ==> canElim (cutOnFmls {?A})" 
allLRP' = "canElimAll (cutIsLRP ?A) ==> canElim (cutIsLP ?A)" 
elimLRP = "canElim (cutIsLRP ?A) ==> canElimAll (cutIsLRP ?A)"
elimLP = "canElim (cutIsLP ?A) ==> canElimAll (cutIsLP ?A)"
elimFmls = "canElim (cutOnFmls ?s) ==> canElimAll (cutOnFmls ?s)" 
\end{verbatim}
  
  If we can eliminate one
  left-and-right-principal/left-principal/arbitrary cut then we can
  eliminate any number, one at a time, top down. \hfill (not backwards!)

Chain of implications \texttt{canElim (cutIsLRP ?A) ==> canElimAll
  (cutIsLRP ?A) ==> canElim  (cutIsLP ?A) ==> canElimAll (cutIsLP ?A)
  ==> canElim (cutOnFmls {?A})}

\begin{verbatim}
"canElimAll (cutOnFmls {?A, ?B}) ==> canElim (cutIsLRP (?A v ?B))"
\end{verbatim}

\begin{verbatim}
"[| canElim (cutOnFmls {?A}); canElim (cutOnFmls {?B}) |]
    ==> canElim (cutOnFmls {?A v ?B})"
\end{verbatim}

  
\end{slide}


\begin{slide}
  \begin{Heading}
    {Finally ...}
  \end{Heading}
  
\begin{verbatim}
"[| canElim (cutOnFmls {?A}); canElim (cutOnFmls {?B}) |]
    ==> canElim (cutOnFmls {?A v ?B})"
\end{verbatim}
  
  A proof by induction on the structure of a formula gives
\begin{verbatim}
canElimFml = "canElim (cutOnFmls {?fml})"
\end{verbatim}
(``you can eliminate one cut on any given formula \texttt{fml}''), 
\begin{verbatim}
canElimAny = "canElim (cutOnFmls UNIV)", 
\end{verbatim}
(``you can eliminate one cut whatever the cut-formula''), 
and, using \texttt{elimFmls},
\begin{verbatim}
canElimAll = "canElimAll (cutOnFmls UNIV)" 
\end{verbatim}

Finally we convert \texttt{canElimAll} into
\begin{verbatim}
cutElim = "IsProvableR rls {} ?concl  ==> 
           IsProvableR (rls - {cut}) {} ?concl"
\end{verbatim}

\end{slide}


\begin{slide}
  \begin{Heading}
    {Further Work}
  \end{Heading}
  
Our cut elimination theorem is quite naive: eliminate top-most cut.

Strong normalisation: define reduction steps, eliminate any cut that
can be reduced, and prove that this cut-elimination procedure terminates:
\begin{itemize}
\item $\Pi_0 > \Pi_1 > \Pi_2 > \cdots > \Pi_n$
\item $\Pi_n$ is cut-free
\item $n$ is finite
\item top most cut method is an instance of this method
\end{itemize}

\end{slide}


\begin{slide}
  \begin{Heading}
    {Belnap's Conditions and New C8}
  \end{Heading}

 \begin{center} 
 {\bf Appendix: Belnap's Conditions.}
 \end{center}
 \bigskip
 
 For every sequent rule Belnap82, page~388 first
 defines the following notions: in an application {\em Inf\ } of a
 sequent rule $(\rho)$, ``constituents occurring as part of occurrences
 of structures assigned to structure-variables are defined to be {\bf
   parameters} of {\em Inf\ }; all other constituents are defined as {\bf
   nonparametric}, including those assigned to formula-variables.
 Constituents occupying similar positions in occurrences of structures
 assigned to the same structure-variable are defined as {\bf congruent}
 in {\em Inf}\ ''. 
 %For example, in an instance of the associative rule
 %$(A)$, all constituents of structures assigned to the structure
 %variables are parameters. As usual, the introduction rules for the
 %logical connectives like $(\vdash \mimp)$ involve constituents (side
 %formulae) in the premisses and constituents (principal formulae) in
 %the conclusion that are not parameters.  
 The eight (actually seven)
 conditions shown below are from [Kracht96]:
 \begin{description}%\vspace{-1em}
 \item[{\bf (C1)}] Each formula which is a constituent of some premiss of a
   rule $\rho$ is a subformula of some formula in the conclusion of $\rho$.
 
 \item[{\bf (C2)}] Congruent parameters are occurrences of the same
   structure.
 
 \item[{\bf (C3)}] Each parameter is congruent to at most one constituent in
   the conclusion. Equivalently, no two constituents of the conclusion are
   congruent to each other.
 
 \item[{\bf (C4)}] Congruent parameters are either all antecedent parts
   or all succedent parts of their respective sequent.
 
 \item[{\bf (C5)}] If a formula is non-parametric in the conclusion of a
   rule $\rho$, it is either the entire antecedent, or the entire succedent.
   Such a formula is called a {\bf principal} formula.
 
 \item[{\bf (C6/7)}] Each rule is closed under simultaneous
   substitution of arbitrary structures for congruent parameters.
\end{description}

\end{slide}

\begin{slide}

\begin{description}
%\vspace*{-2em}
 
 \item[{\bf (C8)}] If there are inference rules $\rho_{1}$ and $\rho_{2}$ with
   respective conclusions $X \vdash \varphi$ and 
   $\varphi \vdash Y$ with $\varphi$ principal
   in both inferences (in the sense of C5), and if (cut) is applied to yield
   $X \vdash Y$ then, either $X 
   \vdash Y$ is identical to $X \vdash \varphi$ or to
   $\varphi \vdash Y$; 
   or it is possible to pass from the premisses of $\rho_{1}$ and
   $\rho_{2}$ to $X \vdash Y$ by means of inferences 
   falling under (cut) where
   the cut-formula is always a proper subformula of $\varphi$. 
%   If $\varphi$ satisfies
%   the ``if'' part of this condition it is known as a ``matching principal
%   constituent''.
 \end{description}

\end{slide}

%\begin{slide}
%  \begin{Heading}
%    { Heading}
%  \end{Heading}
  
%\end{slide}

\end{document}


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