\documentclass{lecture}

\usepackage{amsmath}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{exptrees}
\usepackage{epsfig}

\newcommand\comment[1]{} 

\newtheorem{theorem}{Theorem}

\newcommand{\qed}{}

\newenvironment{proof}{
 \noindent{\bf Proof:}}{\mbox{\bf Q.E.D.}\vspace{1ex}}

\newtheorem{definition}{Definition}

\newtheorem{lemma}{Lemma}

\newtheorem{corollary}{Corollary}

\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$}
}

\newcommand{\pordered}[3]{#1 <_{\texttt{\scriptsize #2}} #3}
\newcommand{\Revpordered}[3]{#1 >_{\texttt{\scriptsize #2}} #3}
\newcommand{\LRPord}[2]{\pordered{#1}{LRP}{#2}}
\newcommand{\cutord}[2]{\pordered{#1}{cut}{#2}}
\newcommand{\snoneord}[2]{\pordered{#1}{sn1}{#2}}
\newcommand{\dtord}[2]{\pordered{#1}{dt}{#2}}
\newcommand{\Revdtord}[2]{\Revpordered{#1}{dt}{#2}}

\begin{document}


\title{% \raisebox{-0.6em}{\epsfig{file=anu.ps,height=1cm}}
       Australian National University}

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

\begin{tabular*}{\linewidth}{@{\hspace{2cm}}l@{\extracolsep{1.5cm}}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@discus.anu.edu.au} \hspace{1cm}  &
                                  \texttt{rpg@discus.anu.edu.au}         \\
\texttt{discus.anu.edu/{\small$\mytilde$}jeremy} &
                        \texttt{discus.anu.edu.au/{\small$\mytilde$}rpg} \\
\end{tabular*}

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

\end{slide}


\begin{slide}
  \begin{Heading}
    {Semantics and Syntax of Logic of Relation Algebras}
  \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 \hfill ::=         \hfill c          \hfill \mid 
                           \hfill p          \hfill \mid 
                           \hfill \bnot A   \hfill \mid 
                           \hfill A \band A \hfill \mid 
                           \hfill A \bor A  \hfill \mid 
                           \hfill \conv A    \hfill \mid 
                           \hfill A \mand A \hfill \mid 
                           \hfill A \mor A$


  \item $\bnot$ is complement \hfill $\band$, $\bor$ are $\cap$, $\cup$
\hfill $A + B$ is $\lnot (\lnot A \mand \lnot B)$

\item[converse] $\conv A := \{ (y, x) | (x, y) \in A \}$ 

\item[composition] $A \mand B := \{ (x, z) | 
                      \exists y \in U. \ (x, y) \in A \ \& \ (y, z) \in B\}$

\comment{
  \item[Structure:] \hfill 
        $X \hfill ::= \hfill A          \hfill \mid 
                          \hfill I          \hfill \mid
                          \hfill \ast X     \hfill \mid
                          \hfill X \comma X \hfill \mid 
                          \hfill E          \hfill \mid 
                          \hfill \blob X    \hfill \mid
                          \hfill X \semic X \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} 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 \hfill ::=         \hfill c          \hfill \mid 
                           \hfill p          \hfill \mid 
                           \hfill \bnot A   \hfill \mid 
                           \hfill A \band A \hfill \mid 
                           \hfill A \bor A  \hfill \mid 
                           \hfill \conv A    \hfill \mid 
                           \hfill A \mand A \hfill \mid 
                           \hfill A \mor A$

  \item[Structure:] \hfill 
        $X \hfill ::= \hfill A          \hfill \mid 
                          \hfill I          \hfill \mid
                          \hfill \ast X     \hfill \mid
                          \hfill X \comma X \hfill \mid 
                          \hfill E          \hfill \mid 
                          \hfill \blob X    \hfill \mid
                          \hfill X \semic X \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[Intuition:] Allow us to unravel complex structures: think of
    high school algebra where we solved $x^2 -4 = 0$ by ``making $x$
    the subject''
    
  \item[Invertible rules:] Reversible, merely bookkeeping device

\comment{
\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}: 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.

\comment{
  \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}: 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$ & $\conv$ & $\mand$ \\
       Connective & $I$ & $\ast$ & $\comma$ & $\myE$ & $\blob$ & $\semic$ \\
       Succedent Part & $\bbot$ & $\bnot$ & $\bor$ & $\mbot$ &  $\conv$ & $\mor$
   \end{tabular}
\vspace*{-0.2em}
     \item Example: $\ast (p_0 \semic p_1) \vdash \ast \blob (p_1 \comma p_3)$ 
     means $\lnot (p_0 \mor p_1) \vdash \lnot \conv (p_1 \band 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  Purely syntactic class of formulae
\comment{
  \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}
    { 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).  

\vfill
  \item Examples: from modal logic  

  \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$}} 
\comment{
    \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}

\comment{
  \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}
    { 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 Kracht shows how to convert each primitive equation into a purely
    structural rule

\comment{
  \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}
    { 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 \hfill ::=     \hfill c          \hfill \mid 
                           \hfill p          \hfill \mid 
                           \hfill \bnot A   \hfill \mid 
                           \hfill A \band A \hfill \mid 
                           \hfill A \bor A  \hfill \mid 
                           \hfill \conv A    \hfill \mid 
                           \hfill A \mand A \hfill \mid 
                           \hfill A \mor A$

  \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  \hfill ::= \hfill A          \hfill \mid 
                          \hfill I          \hfill \mid
                          \hfill \ast X     \hfill \mid
                          \hfill X \comma X \hfill \mid 
                          \hfill E          \hfill \mid 
                          \hfill \blob X    \hfill \mid
                          \hfill X \semic X \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''} is syntactic sugar for

 \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{rls} is the set of rules of $\Dl{RA}$

A shallow embedding would provide, not model, the set of rules.
\end{slide}

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

True derivation has leaves 
%\texttt{Der (''A'' |- ''A'') id  []} 
\texttt{Der (PP ''p'' |- PP ''p'') id  []} 

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

Example: 

\begin{tabular}[c]{rr}
  \begin{minipage}[c]{0.25\linewidth}
    {\vpf
     \bpf
     \A "$A \vdash p$"
     \A "$A \vdash A$"
     \B [1em] "$A, A \vdash p \land A$" "($\vdash \land $)"
     \U "$A \vdash p \land A$" "(\textsl{ctr})"
     \epf
    }
  \end{minipage}
&
\begin{minipage}[c]{0.7\textwidth}
\begin{verbatim}
Der (''A'' |- PP ''p'' && ''A'') cA
 [Der (''A'', ''A'' |- PP ''p'' && ''A'') ands 
 [Unf (''A'' |- PP ''p''), 
  Der (''A'' |- ''A'') idf []]]
\end{verbatim}
\end{minipage}
\end{tabular}

\texttt{idf} is the \emph{admissible} rule $A \vdash A$
\end{slide}

\begin{slide}
  \begin{Heading}
    {Reasoning About Derivations}
  \end{Heading}
  
\begin{verbatim}
datatype dertree = Der sequent rule (dertree list) 
                | Unf sequent 
\end{verbatim}

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

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

\texttt{allDT wfb} returns true if every rule application in
\texttt{dertree} is well formed

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

\end{slide}

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

\begin{definition}
  \texttt{IsDerivableR rules prems concl} holds iff there exists a
  derivation tree \texttt{dt} which uses only rules from set
  \texttt{rules}, is well-formed, has conclusion \texttt{concl}, and
  has premisses from set \texttt{prems}.
\end{definition}

\begin{verbatim}
 "IsDerivableR rules prems concl == (EX dt.
    allDT (frb rules) dt & allDT wfb dt &
    conclDT dt = concl & set (premsDT dt) <= prems)"
\end{verbatim}

\begin{lemma}
The sequent \ \texttt{PP ''p'' |- PP ''p''} is derivable for all atoms $p$
\end{lemma}

Proof: Let \texttt{dt} be  \texttt{Der (PP ''p'' |- PP ''p'') id []} in

 \begin{verbatim}
  IsDerivableR rls {} (PP ''p'' |- PP ''p'')
 \end{verbatim}


\end{slide}

\begin{slide}
  \begin{Heading}
    {Results About Derivability}
  \end{Heading}

Our main result about derivability is a recursive
characterisation of derivability.

\begin{theorem}
  A conclusion \texttt{concl} is derivable from premisses
  \texttt{prems} using rules \texttt{rules} iff either \texttt{concl}
  is one of \texttt{prems}, or there exists an instantiated
  \texttt{rule} obtained from \texttt{rules} and the conclusion of
  \texttt{rule} is \texttt{concl} and the premisses of \texttt{rule}
  are themselves derivable from \texttt{prems} using \texttt{rules}.
\end{theorem}

\begin{verbatim}
IsDerivableR_recur = 
"IsDerivableR ?rules ?prems ?concl = 
  (?concl : ?prems 
    | (EX rule. ruleFromSet rule ?rules 
       & conclRule rule = ?concl 
       & (ALL p : set (premsRule rule). 
           IsDerivableR ?rules ?prems p))
   )" : thm
\end{verbatim}

\end{slide}

\begin{slide}
  \begin{Heading}
    {Formalising Derivable Rules}
  \end{Heading}

\begin{verbatim}
"IsDerivable rules (Rule prems concl) = 
        IsDerivableR rules (set prems) concl"
\end{verbatim}
  
  \begin{lemma}[\texttt{idf} ] The sequent \ \texttt{''A'' |- ''A''} is derivable
    for all formulae $A$ that contain no formula variables
  \end{lemma}

Add the rule \texttt{idf} to \texttt{rls} :

\begin{verbatim}
  idf == Rule [] (''A'' |- ''A'')
\end{verbatim}

\texttt{Der (''A'' |- ''A'') idf []} stands for a complete
  derivation which uses the (proven) admissible rule \texttt{idf}
  that $A \vdash A$ is derivable

\texttt{Unf (''A'' |- ''A'')} stands for an incomplete
  derivation with unfinished premiss $A \vdash A$

\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 a Principal reduction (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 all ancestor occurrences of this $A$
    up $\Pi_{L}$:

  \item Let $\Pi[A ?= Y]$ mean ``in $\Pi$, 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 (similarly make it also right principal)
  \end{itemize}

\end{slide}


\begin{slide}
  \begin{heading}
    {Making a cut left-principal -- simpler cases}
  \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
      \vspace{-1ex}
      \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 $" 
      \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 $" 
      \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}

% following slide inserted from slce.tex
\begin{slide}
  \begin{Heading}
    {Making a cut (left-and-right-)principal}
  \end{Heading}
  
  \begin{itemize}
  \item Similarly to make a left-principal cut also right principal
  \item But note, one cut $\leadsto$ \emph{several} cuts (in general)
  \item Summing up:

\begin{tabular}{r@{\ $\leadsto$\ }l}
single non-principal cut & several left-principal cuts \\
single left-principal cut & several principal cuts \\
single principal cut & several cuts on sub-formulae 
\end{tabular}
  \item 
    To deal with several 
    left-and-right-principal/left-principal/arbitrary cuts,
    deal with a top-most one first (sub-tree containing single cut)
  \item Procedurally, this is a deeply nested recursion. 
  \item Is an equally deeply nested inductive proof necessary?
  \end{itemize}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Cut-Admissibility (Weak Normalisation)}
  \end{Heading}

 Show that the cut rule \cut is \ \ \ \ \textit{admissible} 
 
 Assume: we have cut-free derivations of $X \vdash A$ and $A
 \vdash Y$ 
 
 Show: that there is a cut-free derivation of $X \vdash Y$

 In general, cut-elimination proceeds by repeatedly eliminating an
 arbitrary top-most cut

 Must show that this procedure terminates
 
 Usual argument is a double induction on the size (degree) of the cut
 formula and the heights of the given derivations (grade)

\end{slide}

\begin{slide}
  \begin{Heading}
    {Cut-Admissibility By Structural Induction}
  \end{Heading}

\begin{description}
\item[\texttt{elim}] eliminates a single arbitrary top-most cut,
by turning it into several left-principal cuts 
% (\texttt{allLP} says this is possible)
and using \texttt{elimAllLP} to eliminate them \ldots

\item Our initial derivation contains only one bottom-most cut which
  is not left and right principal and we know how to turn it into
  multiple left principal cuts

\comment{
\item[\texttt{elimAllLP}] eliminates several left-principal cuts,
by repeatedly using \texttt{elimLP} to eliminate the top-most remaining one
\ldots
\item[\texttt{elimLP}] eliminates a top-most left-principal cut,
by turning it into several principal cuts 
% (\texttt{allLRP} says this is possible)
and using \texttt{elimAllLRP} to eliminate them \ldots
\item[\texttt{elimAllLRP}] eliminates several principal cuts,
by repeatedly using \texttt{elimLRP} to eliminate the top-most remaining one
\ldots
\item[\texttt{elimLRP}] eliminates a top-most principal cut,
by turning it into several cuts on \defn{smaller} cut-formulae, 
and using \texttt{elimAll} to eliminate them \ldots
\item[\texttt{elimAll}] eliminates several arbitrary cuts,
by repeatedly using \texttt{elim} to eliminate the top-most remaining one
\ldots \hfill \defn{termination}
}
\end{description}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Cut-Admissibility By Structural Induction}
  \end{Heading}

\begin{description}
\item[\texttt{elim}] eliminates a single arbitrary top-most cut,
by turning it into several left-principal cuts 
% (\texttt{allLP} says this is possible)
and using \texttt{elimAllLP} to eliminate them \ldots

\item all new cuts are left principal

\item[\texttt{elimAllLP}] eliminates several left-principal cuts,
by repeatedly using \texttt{elimLP} to eliminate the top-most remaining one
\ldots

\comment{
\item[\texttt{elimLP}] eliminates a top-most left-principal cut,
by turning it into several principal cuts 
% (\texttt{allLRP} says this is possible)
and using \texttt{elimAllLRP} to eliminate them \ldots
\item[\texttt{elimAllLRP}] eliminates several principal cuts,
by repeatedly using \texttt{elimLRP} to eliminate the top-most remaining one
\ldots
\item[\texttt{elimLRP}] eliminates a top-most principal cut,
by turning it into several cuts on \defn{smaller} cut-formulae, 
and using \texttt{elimAll} to eliminate them \ldots
\item[\texttt{elimAll}] eliminates several arbitrary cuts,
by repeatedly using \texttt{elim} to eliminate the top-most remaining one
\ldots \hfill \defn{termination}
}
\end{description}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Cut-Admissibility By Structural Induction}
  \end{Heading}

\begin{description}
\item[\texttt{elim}] eliminates a single arbitrary top-most cut,
by turning it into several left-principal cuts 
% (\texttt{allLP} says this is possible)
and using \texttt{elimAllLP} to eliminate them \ldots
\item[\texttt{elimAllLP}] eliminates several left-principal cuts,
by repeatedly using \texttt{elimLP} to eliminate the top-most remaining one
\ldots
\item[\texttt{elimLP}] eliminates a top-most left-principal cut,
by turning it into several principal cuts 
% (\texttt{allLRP} says this is possible)
and using \texttt{elimAllLRP} to eliminate them \ldots

\item all new cuts are left-and-right principal
\comment{
\item[\texttt{elimAllLRP}] eliminates several principal cuts,
by repeatedly using \texttt{elimLRP} to eliminate the top-most remaining one
\ldots
\item[\texttt{elimLRP}] eliminates a top-most principal cut,
by turning it into several cuts on \defn{smaller} cut-formulae, 
and using \texttt{elimAll} to eliminate them \ldots
\item[\texttt{elimAll}] eliminates several arbitrary cuts,
by repeatedly using \texttt{elim} to eliminate the top-most remaining one
\ldots \hfill \defn{termination}
}
\end{description}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Cut-Admissibility By Structural Induction}
  \end{Heading}

\begin{description}
\item[\texttt{elim}] eliminates a single arbitrary top-most cut,
by turning it into several left-principal cuts 
% (\texttt{allLP} says this is possible)
and using \texttt{elimAllLP} to eliminate them \ldots
\item[\texttt{elimAllLP}] eliminates several left-principal cuts,
by repeatedly using \texttt{elimLP} to eliminate the top-most remaining one
\ldots
\item[\texttt{elimLP}] eliminates a top-most left-principal cut,
by turning it into several principal cuts 
% (\texttt{allLRP} says this is possible)
and using \texttt{elimAllLRP} to eliminate them \ldots
\item[\texttt{elimAllLRP}] eliminates several principal cuts,
by repeatedly using \texttt{elimLRP} to eliminate the top-most remaining one
\ldots
\item[\texttt{elimLRP}] eliminates a top-most principal cut,
by turning it into several cuts on \defn{smaller} cut-formulae, 
and using \texttt{elimAll} to eliminate them \ldots

\item all new cuts are on strictly smaller cut-formulae

\comment{
\item[\texttt{elimAll}] eliminates several arbitrary cuts,
by repeatedly using \texttt{elim} to eliminate the top-most remaining one
\ldots \hfill \defn{termination}
}
\end{description}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Cut-Admissibility By Structural Induction}
  \end{Heading}

\begin{description}
\item[\texttt{elim}] eliminates a single arbitrary top-most cut,
by turning it into several left-principal cuts 
% (\texttt{allLP} says this is possible)
and using \texttt{elimAllLP} to eliminate them \ldots
\item[\texttt{elimAllLP}] eliminates several left-principal cuts,
by repeatedly using \texttt{elimLP} to eliminate the top-most remaining one
\ldots
\item[\texttt{elimLP}] eliminates a top-most left-principal cut,
by turning it into several principal cuts 
% (\texttt{allLRP} says this is possible)
and using \texttt{elimAllLRP} to eliminate them \ldots
\item[\texttt{elimAllLRP}] eliminates several principal cuts,
by repeatedly using \texttt{elimLRP} to eliminate the top-most remaining one
\ldots
\item[\texttt{elimLRP}] eliminates a top-most principal cut,
by turning it into several cuts on \defn{smaller} cut-formulae, 
and using \texttt{elimAll} to eliminate them \ldots
\item[\texttt{elimAll}] eliminates several arbitrary cuts,
by repeatedly using \texttt{elim} to eliminate the top-most remaining one
\ldots \hfill \defn{termination}

\end{description}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Putting It All Together}
  \end{Heading}
  
\begin{verbatim}
  canElim      :: "(dertree => bool) => bool"
  canElimAll   :: "(dertree => 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)"
\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!)

Chaining these implications gives \\
 \texttt{canElim (cutIsLRP ?A) ==> 
 %  canElimAll (cutIsLRP ?A) ==> canElim  (cutIsLP ?A) ==>
 %  canElimAll (cutIsLP ?A) ==>
  canElim (cutOnFmls {?A})}

Dealing with left-right-principal cuts gives \\
\texttt{canElimAll (cutOnFmls \{?A, ?B\}) ==> \\
\qquad canElim (cutIsLRP (?A v ?B))}
\begin{verbatim}
elimFmls = "canElim (cutOnFmls ?s) ==> canElimAll (cutOnFmls ?s)" 
\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}
  
  A proof by induction on the structure of a formula then 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}
    {Strong Normalisation}
  \end{Heading}
  
Cut-admissibility proceeds by eliminating the 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_n < \Pi_{n-1} < \cdots < \Pi_2 < \Pi_0$
\item $\Pi_n$ is cut-free
\item $n$ is finite
\item weak-normalisation (attacking top most cut) is an instance of this method
\end{itemize}

Usually define reductions as either a parametric or principal move,
with proviso that we must not cross a cut in a parametric move

\end{slide}

\begin{slide}
  \begin{Heading}
    {Why Formalise (in Isabelle) ?}
  \end{Heading}

Strong-normalisation proofs are notoriously difficult involving many cases

We tried to formalise Heinrich Wansing's proof of strong-normalisation
for display logic, but got stuck at one particular case

\comment{
Found a bug ... Wansing assumes that $\Pi^1_L$ is unchanged!


    \begin{center}
      {\small
      \bpf
      \A "$\Pi^{1}_{L}$"
      \U "$V \vdash A $" "($\vdash A$) $V$ is $(*A \comma X)$"
      \U "$X \vdash A, A$" "(dp)"
      \U "$X \vdash A $" "(ctr)"
      \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}

Can construct counter-examples where his proof goes into loops: a
given cut is reduced to itself ... his procedure will not terminate
}

\end{slide}

\begin{slide}
  \begin{Heading}
    {Why Formalise (in Isabelle) ?}
  \end{Heading}

Strong-normalisation proofs are notoriously difficult involving many cases

We tried to formalise Heinrich Wansing's proof of strong-normalisation
for display logic, but got stuck at one particular case

Found a problem ... Wansing assumes that $\Pi^1_L$ is unchanged! 

      \hfill $V_A$ is $(*A \comma X)$ \hfill 
      $V_Y$ is $(*Y \comma X)$ \hfill \mbox{}


    \begin{center}
      {\small
      \bpf
      \A "$\Pi^{1}_{L}$"
      \U "$V_A \vdash A $" "($\vdash A$)"
      \U "$X \vdash A, A$" "(dp)"
      \U "$X \vdash A $" "(ctr)"
      \A "$\Pi_R$"
      \U "$A \vdash Y$" 
      \B [2em] "$X \vdash Y$" "($cut$)"
      \epf
      \qquad \qquad
      \bpf
      \A "$\Pi'^{1}_{L}$"
      \U "$V_Y \vdash A $" "($\vdash A$)"
      \A "$\Pi_R$"
      \U "$A \vdash Y$" 
      \B [2em] "$V_Y \vdash Y$" "($cut$)"
      \U "$X \vdash Y, Y$" "(dp)"
      \U "$X \vdash Y $" "(ctr)"
      \epf
      }
    \end{center}

% Can construct counter-examples where his proof goes into loops: a
% given cut is reduced to itself ... his procedure will not terminate

\end{slide}

\begin{slide}
\begin{heading}
  { Branch in left subtree --- before and after}
\end{heading}
\begin{center}
\bpf
\A "$\Pi'$"
\U "$X' \vdash A $" "(intro-$A$)"
\A "$\Pi''$"
\U "$X'' \vdash A $" "(intro-$A$)"
\B [1em] "$\Pi_L$" "($\pi$)"
\U "$X \vdash A $" "($\rho$)"
\A "$\Pi_R$"
\U "$A \vdash Y$"
\B [0em] "$X \vdash Y$" "($cut$)"
\epf

\bpf
\A "$\Pi'$"
\U "$X' \vdash A $" % "(intro-$A$)"
\A "$\Pi_R$"
\U "$A \vdash Y$"
\B [1em] "$X' \vdash Y$" "($cut$)"
\A "$\Pi''$"
\U "$X'' \vdash A $" % "(intro-$A$)"
\A "$\Pi_R$"
\U "$A \vdash Y$"
\B [1em] "$X'' \vdash Y$" "($cut$)"
\B [1em] "$\Pi_L[A \,?\!= Y]$" "($\pi$)"
\U "$X \vdash Y $" "($\rho$)"
\epf
\end{center}
\end{slide}

\begin{slide}
\begin{heading}
  { Two successive introductions -- before }
\end{heading}

\begin{center}
\bpf
\A "$\Pi$"
\U "$X, B \vdash * B $" "($\rho$)"
\U "$X, B \vdash \lnot B $" "($\vdash \lnot$)"
\U "$*\lnot B, X \vdash *B $" "(dp)"
\U "$*\lnot B, X \vdash \lnot B $" "($\vdash \lnot$)"
\U "$X \vdash \lnot B, \lnot B $" "(dp)"
\U "$X \vdash \lnot B $" "($\vdash \mbox{cont}$)"
\A "$\Pi_R$"
\U "$\lnot B \vdash Y$"
\B [2em] "$X \vdash Y$" "($cut$)"
\epf
\end{center}
\end{slide}

\begin{slide}
\begin{heading}
  { Two successive introductions -- after }
\end{heading}
\begin{center}
\bpf
\A "$\Pi$"
\U "$X, B \vdash * B $" "($\rho$)"
\U "$X, B \vdash \lnot B $" "($\vdash \lnot$)"
\A "$\Pi_R$"
\U "$\lnot B \vdash Y$"
\B [2em] "$X, B \vdash Y $" "($cut$)"
\U "$*Y, X \vdash * B $" "(dp)"
\U "$*Y, X \vdash \lnot B $" "($\vdash \lnot$)"
\A "$\Pi_R$"
\U "$\lnot B \vdash Y$"
\B [0em] "$*Y, X \vdash Y $" "($cut$)"
\U "$X \vdash Y, Y $" "(dp)"
\U "$X \vdash Y $" "($\vdash \mbox{cont}$)"
\epf
\end{center}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Defining Reductions}
  \end{Heading}

  \begin{definition}
    Assuming a relation \texttt{cutReduces} (defined later),
    derivation tree $\Pi_0$ \texttt{reduces} to derivation tree
    $\Pi_1$ if either
  \begin{itemize}
  \item[(a)] $\Pi_0$ \texttt{cutReduces} to $\Pi_1$, or
  \item[(b)] $\Pi_0$ and $\Pi_1$ are identical except that exactly one
       of the immediate subtrees of $\Pi_0$ reduces to the
       corresponding immediate subtree of $\Pi_1$.
  \end{itemize}
  \end{definition}

\begin{verbatim} 
reduces_Unf = "reduces (Unf ?seq) ?dtn = False"
reduces_Der  = "reduces (Der ?seq ?rule ?dtl) ?dtn = 
 ( (EX dtl'. onereduces ?dtl dtl' & ?dtn = Der ?seq ?rule dtl') 
   | cutReduces (Der ?seq ?rule ?dtl) ?dtn )"

onereduces_Nil  = "onereduces [] ?dtl' = False"
onereduces_Cons = "onereduces (?h # ?t) ?dtl' = ( ?dtl' ~= [] 
  & (reduces ?h (hd ?dtl') & ?t = (tl ?dtl') 
     | ?h = (hd ?dtl') & onereduces ?t (tl ?dtl')) )"
\end{verbatim}

\end{slide}

\begin{slide}
  \begin{Heading}
    {Defining Strongly Normalising Derivation Trees}
  \end{Heading}
  
  \begin{definition}
    The set \texttt{sn\_set} is the \defn{smallest} set of derivation trees
    such that:
  \begin{itemize}
  \item[(a)] if $\Pi_0$ cannot be reduced then
  $\Pi_0 \in \texttt{sn\_set}$ 
  \item[(b)] if every tree $\Pi_1$ to which $\Pi_0$ reduces is in
  \texttt{sn\_set} then $\Pi_0 \in \texttt{sn\_set}$.
  \end{itemize}
  
  A derivation tree is \emph{strongly normalisable} iff it is a member
  of \texttt{sn\_set}.
  \end{definition}

\begin{verbatim} 
inductive "sn_set" 
  intrs 
    snI "(ALL dtn. 
    reduces ?dt dtn --> dtn : sn_set) ==> ?dt : sn_set"
\end{verbatim}

  
  Example, the rules $\{0 \in \mathcal S, n \in \mathcal S
  \Longrightarrow n+2 \in \mathcal S\}$ define $\mathcal S$ to be the
  set of even naturals, although the set of all naturals also
  satisfies the rules.
  
\end{slide}

% \begin{slide}
%   \begin{Heading}
%     {Various Binary Orderings}
%   \end{Heading}
  
%   Definition: For two lists \texttt{dtl1} and \texttt{dtl2} of
%   derivation trees, \texttt{sn1red dtl1 dtl2} holds iff the lists
%   \texttt{dtl1} and \texttt{dtl2} are non-empty and differ at only one
%   position where \texttt{dtl1} contains tree \texttt{dt1} and
%   \texttt{dtl2} contains tree \texttt{dt2}, and \texttt{dt1} reduces
%   to \texttt{dt2}, and \texttt{dt1} is strongly normalisable.

% % from SN0.thy
% \begin{verbatim} 
% sn1red_Nil  = "sn1red [] ?dtl2 = False"
% sn1red_Cons = "sn1red (?h # ?t) ?dtl2 = (?dtl2 ~= [] & 
%        (reduces ?h (hd ?dtl2) & ?h : sn_set & ?t = (tl ?dtl2) 
%        | ?h = (hd ?dtl2) & sn1red ?t (tl ?dtl2)) )"
% \end{verbatim}

% \end{slide}

\begin{slide}
  \begin{Heading}
    {Various Binary Orderings}
  \end{Heading}

\begin{enumerate}
  
\item\label{defn:porders-LRP} $\LRPord{\Pi_1}{\Pi_0}$ if the bottom
  inferences of derivations $\Pi_1$ and $\Pi_0$ are both cut, and
  either
  \begin{enumerate}
  \item\label{defn:porders-LRP-1} the cut in $\Pi_1$ is left-principal
    or right-principal, and the cut in $\Pi_0$ is neither, or
  \item\label{defn:porders-LRP-2} the cut in $\Pi_1$ is (left- and
    right-)principal, and the cut in $\Pi_0$ is not (left- and
    right-)principal.
  \end{enumerate}
  
\item\label{defn:porders-cut} $\cutord{\Pi_1}{\Pi_0}$ if the bottom
  inferences of derivations $\Pi_1$ and $\Pi_0$ are both cut, and if
  either
  \begin{enumerate}
  \item\label{defn:porders-cut-1} the size of the cut-formula of
    $\Pi_1$ is smaller than that of $\Pi_0$, or
  \item\label{defn:porders-cut-2} each derivation has the same
    cut-formula, and $\LRPord{\Pi_1}{\Pi_0}$.
  \end{enumerate}
  
\end{enumerate}

\end{slide}

\begin{slide}
  \begin{Heading}
    {Various Binary Orderings}
  \end{Heading}

\begin{enumerate}

\item\label{defn:porders-sn1} $\snoneord{\Pi_1}{\Pi_0}$ 
  if $\Pi_0$ and $\Pi_1$ are the same except that one of the immediate 
  subtrees of  $\Pi_0$ is strongly normalisable and reduces to the 
  corresponding immediate subtree of $\Pi_1$.
  
\item\label{defn:porders-dt} 
  $\dtord{\Pi_1}{\Pi_0}$ iff any of the following hold:
  \begin{enumerate}

  \item\label{defn:porders-dt-1} the bottom inference of $\Pi_1$ is
    not cut, but that of $\Pi_0$ is
  
  \item\label{defn:porders-dt-2} $\cutord{\Pi_1}{\Pi_0}$
  
  \item $\snoneord{\Pi_1}{\Pi_0}$.
  \end{enumerate}

\end{enumerate}

% \end{slide}

% \begin{slide}
%   \begin{Heading}
%     {Theorems About The Partial Orders}
%   \end{Heading}

\begin{theorem}
  The relations \texttt{LRPorder}, \texttt{cutorder},
  \texttt{sn1order}, and \texttt{dtorder} are well-founded
\end{theorem}
  
  Despite notation, these relations are \textit{not} reflexive, and
  some are \textit{not} transitive.  
  
  Intuitively, $(\Pi_1, \Pi_0) \in \texttt{dtorder}$ means that
  $\Pi_1$ is closer to being cut-free (in some sense) than is $\Pi_0$.

\end{slide}

\begin{slide}
  \begin{Heading}
    {Inheriting Strong Normalisation}
  \end{Heading}

We next define \texttt{snHered}, a property of derivation trees which
indicates that a tree inherits strong normalisation from its immediate
subtrees.

\begin{definition}
  $\Pi$ satisfies \texttt{snHered} iff: if all the immediate subtrees
  of $\Pi$ are strongly normalisable then $\Pi$ is strongly
  normalisable.
\end{definition}

\begin{verbatim}
   snHered_def = "snHered ?dt == 
     set (nextUp ?dt) <= sn_set --> ?dt : sn_set"
\end{verbatim}

\begin{lemma}\label{hereds-sn}
  A derivation tree $\Pi$ is strongly normalisable iff every subtree
  of $\Pi$ has the property \texttt{snHered}.
\end{lemma}

% \begin{verbatim}
% hereds_sn = "(ALL dts. 
%   isSubt ?dt dts --> snHered dts) = (?dt : sn_set)" : thm
% \end{verbatim}

Proof: The ``only if'' part uses a clever instantiation of a theorem
generated automatically by Isabelle from the inductive definition of
\texttt{sn\_set}.

% \begin{verbatim}
% sn_set.induct = "[| ?xa : sn_set ; (!!dt. (ALL dtn. 
%     reduces dt dtn --> dtn : sn_set & ?P dtn) ==> ?P dt ) |]  
%  ==> ?P ?xa" : thm 
% \end{verbatim}
  
  The ``if'' part uses induction on the height of $\Pi$ using the
  assumption that every subtree of $\Pi$, including itself, has the
  property \texttt{snHered}.

\end{slide}

\begin{slide}
  \begin{Heading}
    {Defining Cut-Reductions}
  \end{Heading}
  
  \begin{definition}
    Two derivation trees $\Pi_0$ and $\Pi_1$ satisfy \texttt{nparRedP}
    if every subtree $\Pi_1^s$ of $\Pi_1$ with a bottom inference
    (cut) satisfies either
  \begin{itemize}
  \item[(a)] $\Pi_1^s$ is a proper subtree of $\Pi_0$, or
  \item[(b)] $\Pi_1^s$ and $\Pi_0$ have the same cut-formula and
    $\LRPord{\Pi_1^s}{\Pi_0}$.
  \end{itemize}
  \end{definition}

% \begin{verbatim}
% nparRedP_Unf = nparRedP "(Unf ?seq) ?dtn = False"

% nparRedP_Der  = "nparRedP (Der ?seq ?rule ?dtl) ?dtn = (ALL dts.
%  isSubt ?dtn dts & isCut dts --> 
%     isSubt (Der ?seq ?rule ?dtl) dts & Der ?seq ?rule ?dtl ~= dts 
%   | cutForm (Der ?seq ?rule ?dtl) = cutForm dts & 
%     (dts, Der ?seq ?rule ?dtl) : LRPorder)"
% \end{verbatim}

  \begin{definition}
    Two derivation trees $\Pi_0$ and $\Pi_1$ satisfy \texttt{c8redP}
    if the lowest rule of $\Pi_0$ is cut, and for each subtree
    $\Pi_1^s$ of $\Pi_1$ whose lowest rule is cut, either
  \begin{itemize}
  \item[(a)] $\Pi_1^s$ is a proper subtree of $\Pi_0$, or
  \item[(b)] the cut-formula of $\Pi_1^s$ is smaller than that of the
    lowest rule of $\Pi_0$.
  \end{itemize}
  \end{definition}
  
%   \texttt{c8redsfP} has (b) changed to read ``the cut-formula of
%   $\Pi_1^s$ is a proper subformula of the cut-formula of the lowest
%   rule of $\Pi_0$''

% \begin{verbatim}
%    c8redP = "c8redP ?dt ?dtn == ALL dts.
%      isSubt ?dtn dts & botRule dts = cutr -->
%        isSubt ?dt dts & ?dt ~= dts | 
%        size (cutForm dts) < size (cutForm ?dt)"
% \end{verbatim}

%   Note $(\Pi_1^s, \Pi_0) \in \texttt{dtorder}$ and \texttt{c8redsfP}
%   implies \texttt{c8redP}.
    
\end{slide}

\begin{slide}
  \begin{Heading}
    {Defining Cut-Reduction and Hence Reduction}
  \end{Heading}
    
  \begin{definition}
    The derivation tree $\Pi_0$ \emph{cut-reduces} to $\Pi_1$ if the
    following hold simultaneously:
    \begin{itemize}
    \item[(a)] $\Pi_0$ and $\Pi_1$ satisfy either \texttt{nparRedP}
      (for a parametric reduction) or \texttt{c8redP} (for a principal
      reduction)
    \item[(b)] $\Pi_0$ and $\Pi_1$ have the same conclusion
    \item[(c)] the bottom rule of $\Pi_0$ is cut
    \item[(d)] $\Pi_0$ and $\Pi_1$ are not identical
    \item[(e)] $\Pi_1$ does not consist solely of an unfinished leaf, and
    \item[(f)] $\Pi_0$ has at least one immediate subtree
    \end{itemize}
  \end{definition}

\end{slide}


\begin{slide}
  \begin{Heading}
    {Strong-Normalisation}
  \end{Heading}
  
  \begin{lemma}\label{dth}
    For a given derivation $\Pi_0$, if all derivation trees
    $\dtord{\Pi'}{\Pi_0}$ have the property \texttt{snHered}, then so
    does $\Pi_0$.
  \end{lemma}

\begin{verbatim}
dth = "ALL dt'. (dt', ?dt) : dtorder --> snHered dt' 
       ==> snHered ?dt" : thm
\end{verbatim}
  
  Proof: The machine-proof is quite complicated, and a careful
  examination of it highlights why the definition of \textit{dtorder}
  needs to be so complex.

\begin{theorem}
    Every derivation tree is strongly normalisable.
\begin{verbatim}
   all_snH = "snHered ?dt"    : thm
   all_sn  = "strongNorm ?dt" : thm
\end{verbatim}
\end{theorem}

Proof: By well-founded induction, it follows from Lemma~\ref{dth} that
every derivation tree satisfies \texttt{snHered}; the result follows
from Lemma~\ref{hereds-sn}. 

\end{slide}

\begin{slide}
  \begin{Heading}
    {Where are we?}
  \end{Heading}

We have actually shown using Isabelle that a class of reductions which
we have defined 
(in terms of \emph{cutReduces}, and hence of \emph{nparRedP} and \emph{c8redP})
is strongly normalising.
We would like to show that this
class of reductions contains the ones to which Wansing's theorem refers.

We can't do that, but we can at least show that this class contains
enough reductions to eliminate any cuts.

\end{slide}

\begin{slide}
  \begin{Heading}
    {Dealing With Parametric Cuts}
  \end{Heading}

\begin{theorem}\label{pRedLP2}
  Consider a parametric reduction of a cut which proceeds by
  transforming the left subtree (to change its conclusion from $X[A]
  \vdash A$ to $X[Y] \vdash Y$), using the function \texttt{mLP}.
  Assume that the transformation can be performed without traversing
  another cut. Also assume the cut is not already left-principal.
  Then the reduction satisfies the condition \texttt{nparRedP}.
\end{theorem}

\begin{theorem}
  The same as Theorem~\ref{pRedLP2}, except with conclusion 
  ``Then the reduction satisfies the condition \texttt{cutReduces}''.
%\\ {\rm   \texttt{ cutReduces ?dt ?dtY \& valid rls ?dtY"}}
\end{theorem}

Analogous theorems \texttt{pRedRP2}, \texttt{pRedRP3} guarantee that
we can make a cut right-principal, and consequently another theorem
which guarantees that we can make a cut (left and right) principal

The associated functions also produce derivations that satisfy
\texttt{cutReduces}

Thus every parametric move corresponds to a reduction 
in the class of strongly normalising reductions.

\end{slide}

\begin{slide}
  \begin{Heading}
    {Dealing With Principal Cuts}
  \end{Heading}

  \begin{theorem}
    Case for $\lor$: Given a valid derivation tree \texttt{dt}, assume
    that if the bottom rule of \texttt{dt} is cut, then the cut is
    principal and its cut-formula is $A \lor B$.  Then then there is a
    valid derivation tree \texttt{dtn} with the same conclusion as
    \texttt{dt} such that \texttt{dt} and \texttt{dtn} satisfy
    \texttt{c8redsfP} (since the original cut on $A \lor B$ is replaced
    with new cuts on its proper subformulae $A$ and $B$).
  \end{theorem}

These principal reductions satisfy \texttt{c8redsfP} and 
hence \texttt{c8redP}, and are in fact cut-reductions.
These results (one for each logical connective) give 

\begin{theorem}
  If the bottom-most rule of a valid derivation tree $\Pi_0$ is a
  (left and right) principal cut, then there exists a valid derivation
  tree $\Pi_1$ with the same conclusion as $\Pi_0$, such that $\Pi_0$
  \texttt{cutReduces} to $\Pi_1$.
\end{theorem}

Thus every principal move gives a reduction which is in the class of
strongly normalising reductions.

\end{slide}

\begin{slide}
  \begin{Heading}
    {Cut-Elimination Via Strong Normalisation}
  \end{Heading}
  
  \begin{definition}
    A \emph{valid reduction} is a reduction of tree $\Pi_0$ to tree
    $\Pi_1$, where $\Pi_1$ is a valid tree which has the same
    conclusion as $\Pi_0$.
  \end{definition}

% \begin{verbatim}
% validRed_def "validRed == {(dtn, dt).
%     conclDT dtn = conclDT dt & valid rls dtn & reduces dt dtn}"
% \end{verbatim}
%  \begin{lemma}
%   A valid reduction of a subtree is a valid reduction of the
%   whole tree.
%  \end{lemma}

  \begin{theorem}
    Parametric and principal moves give valid reductions.
  \end{theorem}
  
%   Proof: Using \texttt{pRedLP3}, \texttt{pRedRP3} and
%   \texttt{vformC8W'}.

% Theorem: For any valid tree with a single cut at the bottom there
% exists a cut-reduction to another valid tree with the same conclusion
% (using only parametric and principal moves).

% \begin{verbatim}
% cutExRed = "[| isCut ?dt; valid rls ?dt; 
%        allNextDTs (cutOnFmls {}) ?dt |]
%    ==> EX dtn. cutReduces ?dt dtn & valid rls dtn" : thm
% \end{verbatim}

% Proof: We use only \texttt{pRedLP3} and \texttt{pRedRP3} and
% \texttt{vformC8W'}, so that the reductions are restricted to
% parametric and principal moves. Note that \texttt{conclDT dtn =
%   conclDT dt} is implied by \texttt{cutReduces dt dtn}.

  \begin{theorem}
    For any valid tree which contains a cut, there is available at
    least one valid reduction (reduce a top-most cut).
  \end{theorem}

%  \begin{verbatim}
%  ExRed = "[| valid rls ?dt ; ~ allDT (Not o isCut) ?dt |]
%     ==> EX dtn. (dtn, ?dt) : validRed" : thm
%  \end{verbatim}
 
% From here, we obtain cut-elimination by performing repeated valid reductions. 
% The notation \verb|^*| denotes transitive closure, and
% \texttt{allDT (Not o isCut) dtn} means that \texttt{dtn} is
% cut-free since \texttt{o} stands for composition of functions in
% Isabelle/HOL.
% Finally, Theorem~\ref{cutElimSN} states our result in terms of
% cut-admissibility.

% Theorem: For any derivation tree $\Pi$ there exists a tree $\Pi^r$,
% obtained from $\Pi$ by repeated valid reductions, such that $\Pi^r$
% cannot be further validly reduced.
% \begin{verbatim}
% validRed_min = "EX dtn. (dtn, ?dt1) : validRed^* & 
%                 ~ (EX dts. (dts, dtn) : validRed)" : thm
% \end{verbatim}

% Proof: Every tree with a cut admits at least one valid reduction, and
% there is no infinite sequence of valid reductions.  So repeatedly
% perform any sequence of (principal and parametric) reductions until no
% reduction is possible.

% Theorem: For any valid tree $\Pi$, there exists a cut-free valid tree
% $\Pi^r$, obtained from $\Pi$ by repeated valid reductions, such that
% $\Pi^r$ has the same conclusion as $\Pi$.

% \begin{verbatim}
% redNoCut = "valid rls ?dt ==> EX dtn.  
%    allDT (Not o isCut) dtn & valid rls dtn & 
%    (dtn, ?dt) : validRed^* & conclDT dtn = conclDT ?dt" : thm
% \end{verbatim}

Corollary: Any sequence of principal and parametric moves starting
from some derivation $\Pi$ containing cuts, eventually terminates with
a cut-free derivation $\Pi^r$ that has the same conclusion as $\Pi$.

% Proof: In Theorem~\ref{redNoCut}, starting from $\Pi$, choose a
% sequence of parametric and principal reductions only.  Since valid
% reductions are reductions, they are strongly normalising by
% Theorem~\ref{thm:all-sn}, so this sequence terminates with some valid
% derivation $\Pi^r$ from which there is no reduction.  This is only
% possible if $\Pi^r$ is cut-free.

\begin{theorem}
  If a sequent can be derived using rules \texttt{rls}, then it can be
  derived from those rules omitting cut.
\end{theorem}

\begin{verbatim}
cutElim_SN = "IsDerivableR rls {} ?concl ==> 
              IsDerivableR (rls - {cutr}) {} ?concl" : thm
\end{verbatim}

\end{slide}

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

% \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
   (called a {\bf principal} formula).
 
 \item[{\bf (C6/7)}] Each rule is closed under simultaneous
   substitution of arbitrary structures for congruent parameters.
 
 \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}

\begin{slide}
  \begin{Heading}
    {Putting It All Together}
  \end{Heading}
  
\begin{verbatim}
  canElim      :: "(dertree => bool) => bool"
  canElimAll   :: "(dertree => 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}


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