%%
%% Template appendix.tex
%%

\appendix

\chapter{An example of the Cut-Elimination procedure}
\label{app:cut}
The following is a proof of the sequent
$ \smile (A \land B) \vdash \smile (A \lor C) $.
The proof-trees show successive stages in the elimination of (cut) from the
proof.  Note that the ML cut-elimination procedure of Chapter~\ref{ch:cut}
produces a final proof-tree which, when compared with the last one below,
has some extra steps involving inserting, moving and removing `$\bullet$'
operators.

\vpf
\begin{center}
\bpf
\A "$ A \vdash A $" 
\U "$ A, B \vdash A $" "($M \vdash $)"
\U "$ (A \land B) \vdash A $" "($\land \vdash $)"
\U "$ \bullet (A \land B) \vdash \bullet A $" "(\texttt{blbl})"
\U "$ \bullet (A \land B) \vdash \smile A $" "($\vdash \smile $)"
\U "$ \smile (A \land B) \vdash \smile A $" "($\smile \vdash $)"
\A "$ A \vdash A $" 
\U "$ A \vdash A, C $" "($\vdash M $)"
\U "$ A \vdash (A \lor C) $" "($\vdash \lor $)"
\U "$ \bullet A \vdash \bullet (A \lor C) $" "(\texttt{blbl})"
\U "$ \smile A \vdash \bullet (A \lor C) $" "($\smile \vdash $)"
\U "$ \smile A \vdash \smile (A \lor C) $" "($\vdash \smile $)"
\B [2.0em] "$ \smile (A \land B) \vdash \smile (A \lor C) $" "(cut)"
\epf

\vspace{1.0ex}
Original proof

\bpf
\A "$ A \vdash A $" 
\U "$ A, B \vdash A $" "($M \vdash $)"
\U "$ (A \land B) \vdash A $" "($\land \vdash $)"
\U "$ \bullet (A \land B) \vdash \bullet A $" "(\texttt{blbl})"
\U "$ \bullet (A \land B) \vdash \smile A $" "($\vdash \smile $)"

\A "$ A \vdash A $" 
\U "$ A \vdash A, C $" "($\vdash M $)"
\U "$ A \vdash (A \lor C) $" "($\vdash \lor $)"
\U "$ \bullet A \vdash \bullet (A \lor C) $" "(\texttt{blbl})"
\U "$ \smile A \vdash \bullet (A \lor C) $" "($\smile \vdash $)"

\B [2.0em] "$ \bullet (A \land B) \vdash \bullet (A \lor C) $" "(cut)"
\U "$ \bullet (A \land B) \vdash \smile (A \lor C) $" "($\vdash \smile $)"
\U "$ \smile (A \land B) \vdash \smile (A \lor C) $" "($\smile \vdash $)"
\epf

\vspace{1.0ex}
Cut now immediately follows introduction of $\smile A$ on both sides

\bpf
\A "$ A \vdash A $" 
\U "$ A, B \vdash A $" "($M \vdash $)"
\U "$ (A \land B) \vdash A $" "($\land \vdash $)"

\A "$ A \vdash A $" 
\U "$ A \vdash A, C $" "($\vdash M $)"
\U "$ A \vdash (A \lor C) $" "($\vdash \lor $)"

\B [2.0em] "$ A \land B \vdash A \lor C $" "(cut)"
\U "$ \bullet (A \land B) \vdash \bullet (A \lor C) $" "(\texttt{blbl})"
\U "$ \bullet (A \land B) \vdash \smile (A \lor C) $" "($\vdash \smile $)"
\U "$ \smile (A \land B) \vdash \smile (A \lor C) $" "($\smile \vdash $)"
\epf

\vspace{1.0ex}
After changing cut on $\smile A$ to cut on $A$ using (C8)

\bpf
\A "$ A \vdash A $" 
\U "$ A \vdash A, C $" "($\vdash M $)"
\U "$ A \vdash A \lor C $" "($\vdash \lor $)"
\U "$ A, B \vdash A \lor C $" "($M \vdash $)"
\U "$ A \land B \vdash A \lor C $" "($\land \vdash $)"
\U "$ \bullet (A \land B) \vdash \bullet (A \lor C) $" "(\texttt{blbl})"
\U "$ \bullet (A \land B) \vdash \smile (A \lor C) $" "($\vdash \smile $)"
\U "$ \smile (A \land B) \vdash \smile (A \lor C) $" "($\smile \vdash $)"
\epf

\vspace{1.0ex}
Final proof, without cut
\end{center}

\chapter{Source Code Files} \label{app:code}

The ML source files written for this project are too long to reprint here.
They are available on-line.  Please look at
\verb|http://arp.anu.edu.au:80/~jeremy/files/|.
In future, 
when this page no longer exists, part or all of this thesis may have been
published as an Automated Reasoning Project
Technical Report, and there may be a link to the files
under \texttt{http://arp.anu.edu.au:80/ftp/techreports/}.

\newcommand\sfile[1]{\label{#1} } %{ \section{#1} \label{#1} \mbox{}}

\sfile{RS.thy}
\sfile{RS.ML}
\sfile{RS.tac}
\sfile{dRA.thy}
\sfile{dRA.ML}
\sfile{dRA.tac}
\sfile{glob.tac}
\sfile{nglob.tac}
\sfile{pat.tac}
\sfile{weak.tac}
\sfile{flip.tac}
\sfile{CT.ML}
\sfile{ded.ML}
\sfile{RA.thy}
\sfile{RA.ML}
\sfile{peirce.ML}
\sfile{thmisc.ML}
\sfile{Gord.ML}
\sfile{Mad.ML}
\sfile{tsl.ML}
\sfile{pftr.ML}
\sfile{name.ML}
\sfile{cut.ML}
\sfile{C8.ML}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "thesis"
%%% End: