\documentclass [fleqn]{article}

\everymath{\rm}
\everydisplay{\rm}
\usepackage{latexsym}
\setlength {\overfullrule }{0mm}
%\input{lgwinclude}

\usepackage{url}
\usepackage[dvipdfm=true]{hyperref}
\usepackage{amsmath}
\usepackage{theorem}
\usepackage{amssymb}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle=Logiweb sequent calculus}
\hypersetup{colorlinks=true}

% Save current \parindent (used by e.g. pyk display ... end display)
\newlength{\docparindent}
\setlength{\docparindent}{\parindent}

%Our extras
\newtheorem{Def}{Definition}[section]
\newtheorem{Lem}[Def]{Lemma}
\newtheorem{The}[Def]{Theorem}
\newtheorem{Cor}[Def]{Corollary}
\newtheorem{Alg}[Def]{Algorithm}
\theorembodyfont{\rmfamily} %normale bogstaver
\newtheorem{Exa}[Def]{Example}
\newtheorem{Rem}[Def]{Remark}

\newenvironment{proof}{
{\bf{\scriptsize{\uppercase{proof:}}}}\\}{
\begin{flushright}
\ensuremath{\blacksquare}
\end{flushright}}
\newcommand{\qedsubproof}{\begin{flushright}\ensuremath{\square}\end{flushright}}

\begin{document}
\title{Formal Logic}
\author{Lasse Nielsen \& Morten Ib Nielsen\\
Department of Computer Science, University of Copenhagen}
\date{\today}
\maketitle

\section{Initial remarks}
Initially we planned to show a simple result of Group Theory namely the
uniqueness of the neutral element. Our idea was to develop propositional logic
and predicate calculus first. Based on these we planned to develop the axiomatic set theory ZFC
and finally when we had sets we could define groups. Unfortunately it turned out that this was
much more cumbersome than we thought both because we are newcomers to Logiweb\texttrademark{} and also because core Logiweb\texttrademark{}
is very low level. Being newcomers to Logiweb\texttrademark{} we have used a lot of time
trying to find out how to use the system. This hasn't been easy due to the absence of a hands on users manual.
Thus we wasted a lot of time early on trying to parse other peoples code from earlier years in order to understand how
to use pyk (the language used to construct proofs ect. in Logiweb\texttrademark{}). This was a very frustrating and non-trivial task since this years pyk syntax is different from earlier years!
A lot of emailing back and forth with Klaus Grue helped us, but progress was slow. Very late in the course we had the opportunity
to sit down with Klaus in a kind of assisted programming session, where Klaus helped us with our problems as they occurred - 
this was very rewarding. After that we revised our goals with respect to this project and we found that even though we were now
able to prove things in Logiweb\texttrademark{} our initial goal was out of range because of the assembler like nature of our predicate calculus.
Instead we decided to take the first step towards a more high level interface to our predicate calculus.

\section{Conclusion}
This Logiweb\texttrademark{} page is an exam project on the course \emph{202 Logik} Spring 2006 at
the  Department of Computer Science, University of Copenhagen. The purpose with this project is to use
Logiweb\texttrademark{} \emph{to publish a machine checkable proof for a theorem of our choise} - which we have done
\footnote{This page has been verified and found correct by Logiweb\texttrademark{} and is
available at \url{http://www.diku.dk/hjemmesider/ansatte/grue/logiweb/20060417/home/mortenib/finalversion/fixed/}.}.
Since
both of us have backgrounds in mathematics and formal methods in computer science we started out having
high ambitions. As hinted we had to revise our goals along the way for several reasons. Instead of doing
a large and complicated proof we have decided to show how to use the Logiweb\texttrademark{} system to
\emph{define a theory} (a set of axioms) and how to \emph{define and prove lemmas in a theory} (both using axioms
as well as already proved lemmas). Along the way we have explained key parts of the Logiweb\texttrademark{} notation.
It is our hope that this Logiweb\texttrademark{} page will serve as a helping hand to 
future students on this course providing the \emph{getting started} manual that we have been missing so much.

We start out defining a theory called \emph{pred calc} containing one possible set of axioms and inference rules
for the predicate calculus. Since these axioms are very low level we define, inspired by Natural Deduction
(see \cite{huth}), a set of higher level (and more intuitive) proof rules which we prove. Finally we use these
higher level rules to prove lemma \ref{lem:mainresult}.

\section{Introduction}
This Logiweb\texttrademark{} page is formally correct. This means that it has been verified and found correct by the Logiweb\texttrademark{} proof engine.
Therefore we can say that it is correct modulo errors in the proof engine. Is the content correct then? Well yes, but only in the sense that the lemmas
we have proved are consequences of the axioms and proof rules we have introduced. There is no guarantee of soundness of our axioms and proof rules.

We have structured this document as follows. In section \ref{sec:predcalc} we define the axioms and proof rules
of predicate calculus. We conclude the section with two simple proofs namely the very (intuitively) obvious
lemma \emph{trivia} \ref{lem:trivia} and the lemma \emph{repeat} \ref{lem:repeat}. Then in section
\ref{sec:natded} we state and prove lemmas inspired by Natural Deduction. Finally in section \ref{sec:higherproof}
we use these lemmas to prove lemma \ref{lem:mainresult}. The appendix includes various Logiweb\texttrademark{} dependent
stuff like \emph{Tex definitions} and \emph{Priority table} but also our suggestions of how Logiweb\texttrademark{} could be improved.

\section{First order predicate calculus}\label{sec:predcalc}
Based on Mathworld\footnote{\url{http://mathworld.wolfram.com/First-OrderLogic.html}.} and thus on Kleene (2002) we define
first-order predicate calculus below. We note that the axioms 1 through 10 together with the inference rule
modus ponens (pcmp) constitutes the propositional calculus. Our definitions are not exactly like those found on Mathworld for two reasons. 
First we have made $\Rightarrow$ right associative in order to get rid of unnecessary parenthesis. This means that 
$\underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}$ really means
$\underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}$ below. Second we had to express formulations such as \emph{in which $x$ occurs free} in
a machine checkable way. 

The $
[
\mbox{pred calc}
\stackrel{
stmt
}{\rightarrow}
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon \neg \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {h}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}} \vee \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\lambda 
\mathsf{x}
.
Ded_0(
\lceil \underline{
\mathsf {a}}
\rceil 
,
\lceil \underline{
\mathsf {b}}
\rceil 
)
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\Rightarrow \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
]$ contains the following axioms:

\begin{enumerate}
\item $
[
\mbox{pc1}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
]
[
\mbox{pc1}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pc2}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {h}}
]
[
\mbox{pc2}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pc3}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
]
[
\mbox{pc3}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pc4}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
]
[
\mbox{pc4}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pc5}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}} \vee \underline{
\mathsf {f}}
]
[
\mbox{pc5}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pc6}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
]
[
\mbox{pc6}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pc7}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {g}}
]
[
\mbox{pc7}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pc8}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
]
[
\mbox{pc8}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pc9}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \underline{
\mathsf {f}}
]
[
\mbox{pc9}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pc10}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon \neg \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
]
[
\mbox{pc10}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pc11}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
]
[
\mbox{pc11}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pc12}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
]
[
\mbox{pc12}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\end{enumerate}

The proof rules in the $
[
\mbox{pred calc}
\stackrel{
stmt
}{\rightarrow}
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon \neg \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {h}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}} \vee \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\lambda 
\mathsf{x}
.
Ded_0(
\lceil \underline{
\mathsf {a}}
\rceil 
,
\lceil \underline{
\mathsf {b}}
\rceil 
)
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\Rightarrow \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
]$ are:

\begin{itemize}
\item $
[
\mbox{pcmp}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {g}}
]
[
\mbox{pcmp}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pcia}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\Rightarrow \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
]
[
\mbox{pcia}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pcie}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
]
[
\mbox{pcie}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
\mbox{pcdeduction}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\lambda 
\mathsf{x}
.
Ded_0(
\lceil \underline{
\mathsf {a}}
\rceil 
,
\lceil \underline{
\mathsf {b}}
\rceil 
)
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
]
[
\mbox{pcdeduction}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$
\end{itemize}

\subsection{A conservative extension}
The rule \emph{pcdeduction} is not really a part of Predicate Calculus according to Mathworld but it is a conservative extension
in the sense than we cannot prove anything using this rule that we cannot prove without it. We include it in order to make proofs shorter
and thus easier to understand for humans. As a curiosity we cannot prove that \emph{pcdeduction} is a conservative extension formally
\footnote{In a machine checkable way.}.

\subsection{A troublesome extension}
It seems fair to conclude $\underline{
\mathsf {b}}$ if both $\underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}$ and $\underline{
\mathsf {a}}$ are known.
This is the proof rule \emph{modus ponens}. Unfortunately Logiweb\texttrademark{} does not allow the use of modus ponens on anything other than lemmas
e.g. modus ponens cannot be used on line numbers in proofs. One of the aims of this project is to introduce and prove natural deduction like
proof rules enabling the use of pred calc on a higher level. Since we cannot use line numbers with modus ponens we cannot prove the implication
introduction rule (see \cite[p.~27]{huth}). Therefore we need to add the following rule as a proof rule in $
[
\mbox{pred calc}
\stackrel{
stmt
}{\rightarrow}
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon \neg \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {h}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}} \vee \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\lambda 
\mathsf{x}
.
Ded_0(
\lceil \underline{
\mathsf {a}}
\rceil 
,
\lceil \underline{
\mathsf {b}}
\rceil 
)
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\Rightarrow \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
]$.

\begin{itemize}
\item $
[
\mbox{pcunsound}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
]
[
\mbox{pcunsound}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$
\end{itemize}

We have been told that this rule makes the system unsound, but we have not seen and cannot find an example of this. We have been told
(by Klaus Grue via email) that it requires some special side conditions in order to be sound. Alas we have been unable to communicate with
Klaus Grue in the week up to our deadline. Therefore we have been unable to ameliorate this deficiency but we are convinced that we only use
the rule in sound ways. Given the right side conditions we expect that our proofs could be patched simply by adding these side conditions.

\subsection{Notation}
Some of the notation used above is most likely unfamiliar. So let's spend a few paragraphs explaining it before we continue.
The meaning of the axioms and proof rules above are of course given by their definition but in order to understand the definitions
we need to explain the basic syntax (or at least the part of it we use) in Logiweb\texttrademark{} definitions and proofs.
\begin{itemize}

\item{\textbf{The symbol $\Pi$}} is the for all meta quantifier.

\item{\textbf{The symbol $\vdash$}} is placed between two propositions. The meaning of $A \vdash B$ is that if $A$ can be proved then so can $B$.
$\vdash$ can be used sequentially in the way that $A \vdash B \vdash C$ means if $A$ can be proved, then if $B$ can be proved, then so can $C$.
That is if $A$ and $B$ can be proved then so can $C$.

\item{\textbf{The symbol $\triangleright$}} is placed between a rule and a line number.
It is the opposite of $\vdash$ in the sense that if $R$ is a rule saying that $A \vdash B$ and $L$ is a line concluding $A$, then
$R \triangleright L$ concludes $B$.

\item{\textbf{Explanation of $\gg$}}. A line in a proof consists of the symbol $\gg$ with the use of a rule on the left, and the conclusion on the right.
The example above would give the line $R \triangleright L \gg B$.

\item{\textbf{The meaning of $\Vdash$}} is almost the same as $\vdash$. If the condition on the left evaluates to true, then the proposition on the right can be proved.
The condition on the left of a $\Vdash$ is a so called side-condition. The only side-conditions we use are expressed using substitution and $\sharp$ (explained below).

\item{\textbf{The $\triangleright\!\!\triangleright$}} symbol is used much like $\triangleright$, but it is the opposite of $\Vdash$ instead of $\vdash$, thus the line number on the right 
of the symbol must conclude that the side-condition is fulfilled.

\item{\textbf{The side-condition $\left< A  \equiv B \mid C := D \right>$}} is fulfilled, if the proposition $B$ where any occurrence of the meta-variable $C$ is replaced
by the proposition $D$ is exactly equal to the proposition $A$. Another way to express this using a more common notation of substitution would be $A \equiv B[D/C]$. It is
important to note that this substitution avoids variable capture. An example of why variable capture would be unsound is the propositional formula
$\forall x \exists y: (x \lor y) \land (\lnot x \lor \lnot y)$. We see that this is a tautology since the choice of $y\equiv \lnot x$ satisfies the formula. But if we
substituted $y$ for $x$ in this formula then we would get an absurdity.

\item{\textbf{The side-condition $A \sharp B$}} is fulfilled if the meta-variable $A$ does not occur (free) in the proposition $B$.

\end{itemize}

\subsection{Some small proofs}
Having explained the syntax of definitions and proofs we continue with two simple but useful lemmas just to show
how it is done. Lemma \ref{lem:trivia} is proved using only axioms and proof rules while the proof of lemma \ref{lem:repeat} 
uses the result of lemma \ref{lem:trivia} as well.

\begin{Lem}\label{lem:trivia}
$
[
\mbox{trivia}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
]$
\end{Lem}

$
[
\mbox{trivia}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\mbox{pc2}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
; 
\mbox{pc1}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
; 
\mbox{pc1}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}[Repetition]\label{lem:repeat}
$
[
\mbox{repeat}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}}
]$
\end{Lem}

$
[
\mbox{repeat}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}}
\vdash 
\mbox{trivia}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\section{Natural deduction}\label{sec:natded}
The axioms and proof rules in $
[
\mbox{pred calc}
\stackrel{
stmt
}{\rightarrow}
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon \neg \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {h}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}} \vee \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\lambda 
\mathsf{x}
.
Ded_0(
\lceil \underline{
\mathsf {a}}
\rceil 
,
\lceil \underline{
\mathsf {b}}
\rceil 
)
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\Rightarrow \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
]$ constitutes a very low level proof system.
In order to ameliorate this we introduce and prove some higher level (and more intuitive) proof rules. These proof rules
are inspired by natural deduction as defined in \cite{huth}. We conclude this section by justifying why we have replaced two
rules from \cite{huth} with a new rule.

\begin{Lem}
$
[
\mbox{andintro}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
]$
\end{Lem}

$
[
\mbox{andintro}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash 
\mbox{pc3}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\gg \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {g}}
\rhd \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\gg \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{andelim1}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
]$
\end{Lem}

$
[
\mbox{andelim1}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\vdash 
\mbox{pc6}
\gg \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\rhd \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{andelim2}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {g}}
]$
\end{Lem}

$
[
\mbox{andelim2}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\vdash 
\mbox{pc7}
\gg \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {g}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\rhd \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {g}}
\gg \underline{
\mathsf {g}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{orintro1}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
]$
\end{Lem}

$
[
\mbox{orintro1}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash 
\mbox{pc4}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\gg \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{orintro2}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
]$
\end{Lem}

$
[
\mbox{orintro2}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {g}}
\vdash 
\mbox{pc5}
\gg \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {g}}
\rhd \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\gg \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{orelim}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {h}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {h}}
\vdash \underline{
\mathsf {h}}
]$
\end{Lem}

$
[
\mbox{orelim}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {h}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {h}}
\vdash 
\mbox{implyintro}
\rhd \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {h}}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {h}}
; 
\mbox{implyintro}
\rhd \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {h}}
\gg \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
; 
\mbox{pc8}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {h}}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\gg \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\rhd \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\gg \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\rhd \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\gg \underline{
\mathsf {h}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{implyintro}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
]$
\end{Lem}

$
[
\mbox{implyintro}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash 
\mbox{pcunsound}
\rhd \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\rhd \underline{
\mathsf {f}}
\gg \underline{
\mathsf {g}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{notintro}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {g}}
\vdash \neg \underline{
\mathsf {f}}
]$
\end{Lem}

$
[
\mbox{notintro}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {g}}
\vdash 
\mbox{implyintro}
\rhd \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
; 
\mbox{implyintro}
\rhd \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {g}}
\gg \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {g}}
; 
\mbox{pc9}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \underline{
\mathsf {f}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \underline{
\mathsf {f}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {g}}
\rhd \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \underline{
\mathsf {f}}
\gg \neg \underline{
\mathsf {f}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{notnotelim}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon \neg \neg \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}}
]$
\end{Lem}

$
[
\mbox{notnotelim}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon \neg \neg \underline{
\mathsf {f}}
\vdash 
\mbox{pc10}
\gg \neg \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
; 
\mbox{pcmp}
\rhd \neg \neg \underline{
\mathsf {f}}
\rhd \neg \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$


\begin{Lem}\label{lem:forallintro}
$
[
\mbox{forallintro}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}} \vee \neg \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {f}}
\vdash \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
]$
\end{Lem}

$
[
\mbox{forallintro}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}} \vee \neg \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {f}}
\vdash 
\mbox{lem}
\gg \underline{
\mathsf {g}} \vee \neg \underline{
\mathsf {g}}
; 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {g}} \vee \neg \underline{
\mathsf {g}}
\vdash 
\mbox{repeat}
\rhd \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {g}} \vee \neg \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\gg \underline{
\mathsf {g}} \vee \neg \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
; 
\mbox{pcia}
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}} \vee \neg \underline{
\mathsf {g}}
\rceil 
\rhd \underline{
\mathsf {g}} \vee \neg \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\gg \underline{
\mathsf {g}} \vee \neg \underline{
\mathsf {g}}
\Rightarrow \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {g}} \vee \neg \underline{
\mathsf {g}}
\rhd \underline{
\mathsf {g}} \vee \neg \underline{
\mathsf {g}}
\Rightarrow \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\gg \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Rem}
In lemma \ref{lem:forallintro} we use the side condition $
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}} \vee \neg \underline{
\mathsf {g}}
\rceil $. We would like to use the 
equivalent $
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil $ instead but we haven't been able to find a way to prove the former side condition
from the latter. Another example of reasoning about side conditions is the following. If we have
$
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle $ and $
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil $ then it follows that
$
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil $. Unfortunately we haven't heard of any ways to reason about side conditions therefore we are forced to assume side
conditions in lemmas whenever we need them even though they might be deductable.
\end{Rem}

\begin{Lem}{}\hspace{1cm}\\
$
[
\mbox{forallelim}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash \underline{
\mathsf {g}}
]$
\end{Lem}

$
[
\mbox{forallelim}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\mbox{pc11}
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\gg \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
; 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash 
\mbox{pcmp}
\rhd \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\rhd \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\gg \underline{
\mathsf {g}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash \underline{
\mathsf {g}}
\gg \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash \underline{
\mathsf {g}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}\hspace{1cm}\\
$
[
\mbox{existsintro}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\vdash \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
]$
\end{Lem}

$
[
\mbox{existsintro}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\mbox{pc12}
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\gg \underline{
\mathsf {g}}
\Rightarrow \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
; 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {g}}
\vdash 
\mbox{pcmp}
\rhd \underline{
\mathsf {g}}
\rhd \underline{
\mathsf {g}}
\Rightarrow \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\gg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {g}}
\vdash \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\gg \underline{
\mathsf {g}}
\vdash \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{existselim}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {g}}
]$
\end{Lem}

$
[
\mbox{existselim}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash 
\mbox{implyintro}
\rhd \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
; 
\mbox{pcie}
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\gg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
; 
\mbox{pcmp}
\rhd \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\rhd \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\gg \underline{
\mathsf {g}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\subsection{Derived lemmas}
Below we apply the lemmas above together with the defining rules of\\$
[
\mbox{pred calc}
\stackrel{
stmt
}{\rightarrow}
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon \neg \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {h}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}} \vee \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\lambda 
\mathsf{x}
.
Ded_0(
\lceil \underline{
\mathsf {a}}
\rceil 
,
\lceil \underline{
\mathsf {b}}
\rceil 
)
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\Rightarrow \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
]$ to prove some other fairly standard 
and very useful lemmas.

\begin{Lem}[Modus Tollens]
$
[
\mbox{mt}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \neg \underline{
\mathsf {g}}
\vdash \neg \underline{
\mathsf {f}}
]$
\end{Lem}

$
[
\mbox{mt}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \neg \underline{
\mathsf {g}}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\gg \underline{
\mathsf {g}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\gg \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
; 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash 
\mbox{repeat}
\rhd \neg \underline{
\mathsf {g}}
\gg \neg \underline{
\mathsf {g}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {g}}
\gg \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {g}}
; 
\mbox{notintro}
\rhd \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\rhd \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {g}}
\gg \neg \underline{
\mathsf {f}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{notnotintro}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}}
\vdash \neg \neg \underline{
\mathsf {f}}
]$
\end{Lem}

$
[
\mbox{notnotintro}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}}
\vdash 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {f}}
\vdash 
\mbox{repeat}
\rhd \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}}
\rhd \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\gg \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
; 
\mbox{trivia}
\gg \neg \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {f}}
; 
\mbox{pc9}
\gg \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {f}}
\Rightarrow \neg \neg \underline{
\mathsf {f}}
; 
\mbox{pcmp}
\rhd \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\rhd \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {f}}
\Rightarrow \neg \neg \underline{
\mathsf {f}}
\gg \neg \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {f}}
\Rightarrow \neg \neg \underline{
\mathsf {f}}
; 
\mbox{pcmp}
\rhd \neg \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {f}}
\rhd \neg \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {f}}
\Rightarrow \neg \neg \underline{
\mathsf {f}}
\gg \neg \neg \underline{
\mathsf {f}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}[Proof by Contradiction]
$
[
\mbox{pbc}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \neg \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \neg \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
]$
\end{Lem}

$
[
\mbox{pbc}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \neg \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \neg \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {g}}
\vdash 
\mbox{notintro}
\rhd \neg \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\rhd \neg \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {g}}
\gg \neg \neg \underline{
\mathsf {f}}
; 
\mbox{notnotelim}
\rhd \neg \neg \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}[Law of the Excluded Middle]\label{the:lem}\hspace{1cm}\\
$
[
\mbox{lem}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
]$
\end{Lem}

$
[
\mbox{lem}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {f}}
\colon \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\vdash 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}}
\vdash 
\mbox{orintro1}
\rhd \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
; 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}}
\vdash 
\mbox{repeat}
\rhd \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\gg \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
; 
\mbox{notintro}
\rhd \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\rhd \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\gg \neg \underline{
\mathsf {f}}
; 
\mbox{orintro2}
\rhd \neg \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {f}}
\colon \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\gg \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
; 
\forall \underline{
\mathsf {f}}
\colon \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\vdash 
\mbox{repeat}
\rhd \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\gg \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {f}}
\colon \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\gg \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
; 
\mbox{notintro}
\rhd \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\rhd \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\gg \neg \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
; 
\mbox{notnotelim}
\rhd \neg \neg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\subsection{A word on $\bot$}
The proof rules of natural deduction in \cite{huth} uses bottom.
Bottom represents the concept of unsoundness, that is it should be impossible to prove bottom in a sound logic.
The way to prove bottom would be to prove any absurdity, that is for any proposition $A$ to prove both $A$ and not $A$. In \cite{huth}
this is captured in the proof rule $\frac{\lnot A \quad A}{\bot}$.
In \cite{huth} bottom is used in two ways. First if you under the assumption of a proposition $A$ can prove bottom then you can conclude that $A$ is false,
that is not $A$ is true. In \cite{huth} this is captured by the proof rule $\frac{\begin{tiny}\begin{array}{c}A \\ \vdots \\ \bot\end{array}\end{tiny}}{\lnot A}$ (notelim).
This makes sense if we assume that the logical system is sound, because this means that it is free of absurdities, so if $A$ was true 
it would be impossible to prove an absurdity thus $A$ must be false.  Second the assumption of bottom can be used to conclude anything. In \cite{huth} this is
captured in the proof rule $\frac \bot A$ (botelim).

Since the predicate logic from Mathworld, which we have used as a basis for $
[
\mbox{pred calc}
\stackrel{
stmt
}{\rightarrow}
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon \neg \neg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {h}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \vee \underline{
\mathsf {h}}
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}} \vee \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\lambda 
\mathsf{x}
.
Ded_0(
\lceil \underline{
\mathsf {a}}
\rceil 
,
\lceil \underline{
\mathsf {b}}
\rceil 
)
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\mathrel {\oplus} 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {r}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {g}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {r}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {g}}
\mathrel {\oplus} 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {g}}
\Rightarrow \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\Rightarrow \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
]$, doesn't use or define the notion of bottom,
we cannot adopt the rules of natural deduction directly. We have chosen to solve this problem by replacing the problematic proof rules above with a new proof rule called 
\emph{notintro}. This way we can avoid the use of bottom alltogether while we preserve the rest of the system.

To justify our actions we hand proof the following metatheorem:

\begin{The}
Let Nat' be the system of proof rules introduced in section \ref{sec:natded} and let Nat be the same system without the rule notintro but with rules notelim and botelim added.
Let $F$ be fixed and define $\bot\equiv F \land \lnot F$\footnotemark. Then the following holds:
\begin{enumerate}
\item If $B$ can be proved in Nat then $B[F\land\lnot F/\bot]$ can be proved in Nat'.
\item If $B$ can be proved in Nat' then B can be proved in Nat.
\end{enumerate}
\end{The}
\footnotetext{$F$ must be fixed for all occurrences of bottom e.g. $\bot \lor \bot$ must be translated to $(F \land \lnot F) \lor (F \land \lnot F)$ and can't be translated to $(F \land \lnot F) \lor (G \land \lnot G)$.}
\begin{proof}

Both claims in this metatheorem are proved by induction on the derivation of the proof on the left hand side of the implication.
To save space we only consider the interesting cases. Thus we skip all of the rules the two systems have in common.
\\
\\
\textbf{Proof of 1:}\\
In this proof $A'\equiv A[F\land \lnot F/\bot]$.\\
\\

The rule $\frac{A \quad \lnot A}{\bot}$. \\
Given proofs of $A$ and $\lnot A$ we need to prove $F \land \lnot F$.
Using the induction hypothesis on the proofs of $A$ and $\lnot A$, we get proofs of $A'$ and $\lnot A'$ using our system of lemmas.
Now we have proofs of $A'$ and $\lnot A'$, which means that we can also prove $A'$ and $\lnot A'$ using $F$ or $\lnot F$ as assumptions.
Now we can construct the proof of $F \land \lnot F$ like this:
$$
\frac
{\frac
 {\frac
  {
   \begin{array}{c}
   \lnot F \\
   \vdots \\
   A'
   \end{array}
   \quad
   \begin{array}{c}
   \lnot F \\
   \vdots \\
   \lnot A'
   \end{array}
  }
  {\lnot \lnot F}
 }
 {F}
 \frac
 {
  \begin{array}{c}
  F \\
  \vdots \\
  A'
  \end{array}
  \quad
  \begin{array}{c}
  F \\
  \vdots \\
  \lnot A'
  \end{array}
 }
 {\lnot F}
}
{F \land \lnot F}
$$
%
The rule $\frac{\bot}{A}$. \\
Given proof of $F \land \lnot F$ we need to prove $A'$.
Using the induction hypothesis we get a proof of $F \land \lnot F$. Using andelim1 and andelim2 we obtain proofs of $F$ and $\lnot F$.
Finally (using weakening) we can construct proofs of $F$ and $\lnot F$ under the assumption of $\lnot A'$.
Now we can construct the proof of $A'$ as follows:
$$
\frac
{\frac
 {
  \frac
  {\begin{array}{c}
   \lnot A' \\
   \vdots \\
   F \land \lnot F
   \end{array}
  }
  {F}
  \quad
  \frac
  {\begin{array}{c}
   \lnot A' \\
   \vdots \\
   F \land \lnot F
   \end{array}
  }
  {\lnot F}
 }
 {\lnot \lnot A'}
}
{A'}
$$
%
The rule $\frac{A \vdash \bot}{\lnot A}$.
Using the induction hypothesis on the proof of $A \vdash \bot$ we obtain a proof of $A' \vdash F \land \lnot F$.
Using the andelim1 and andelim2 lemmas, we get proofs of $A' \vdash F$ and $A' \vdash \lnot F$.
Now we can construct the proof of $\lnot A'$ like this:
$$
\frac
{
 \frac
 {\begin{array}{c}
  A' \\
  \vdots \\
  F \land \lnot F
  \end{array}
 }
 {F}
 \quad
 \frac
 {\begin{array}{c}
  A' \\
  \vdots \\
  F \land \lnot F
  \end{array}
 }
 {\lnot F}
}
{\lnot A'}
$$
That concludes all the interesting rules. The other rules follow by using the induction hypothesis on the given proofs, and using the same rule to conclude the desired proposition.
\\
\\
\textbf{Proof of 2:}\\
There is only one interesting rule, and that is notintro.
Given the proofs of $A \vdash B$ and $A \vdash \lnot B$ we wish to prove $\lnot A$.
We construct the proof like this.
$$
\frac
{\frac
 {\begin{array}{c}
  A \\
  \vdots \\
  B
  \end{array}
  \begin{array}{c}
  A \\
  \vdots \\
  \lnot B
  \end{array}
 }
 {\bot}
}
{\lnot A}
$$
That concludes all the interesting rules. The other rules follow by using the induction hypothesis on the given proofs, and using the same rule to conclude the desired proposition.
% }}}
\end{proof}

\subsubsection{A practical lemma}
Above we saw that $\bot$ could be replaced with $F \land \lnot F$ and that the proof rule botelim allows us to conclude anything once we have $\bot$. This gives rise to the
following very usefull lemmas.

\begin{Lem}
$
[
\mbox{bottomelim}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \neg \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
]$
\end{Lem}

$
[
\mbox{bottomelim}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}} \wedge \neg \underline{
\mathsf {f}}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \neg \underline{
\mathsf {g}}
\vdash 
\mbox{andelim1}
\rhd \underline{
\mathsf {f}} \wedge \neg \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \neg \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\gg \neg \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
; 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \neg \underline{
\mathsf {g}}
\vdash 
\mbox{andelim2}
\rhd \underline{
\mathsf {f}} \wedge \neg \underline{
\mathsf {f}}
\gg \neg \underline{
\mathsf {f}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \neg \underline{
\mathsf {g}}
\vdash \neg \underline{
\mathsf {f}}
\gg \neg \underline{
\mathsf {g}}
\vdash \neg \underline{
\mathsf {f}}
; 
\mbox{notintro}
\rhd \neg \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\rhd \neg \underline{
\mathsf {g}}
\vdash \neg \underline{
\mathsf {f}}
\gg \neg \neg \underline{
\mathsf {g}}
; 
\mbox{notnotelim}
\rhd \neg \neg \underline{
\mathsf {g}}
\gg \underline{
\mathsf {g}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{lemnotintro}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}} \wedge \neg \underline{
\mathsf {g}}
\vdash \neg \underline{
\mathsf {f}}
]$
\end{Lem}

$
[
\mbox{lemnotintro}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}} \wedge \neg \underline{
\mathsf {g}}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}} \wedge \neg \underline{
\mathsf {g}}
\gg \underline{
\mathsf {g}} \wedge \neg \underline{
\mathsf {g}}
; 
\mbox{andelim1}
\rhd \underline{
\mathsf {g}} \wedge \neg \underline{
\mathsf {g}}
\gg \underline{
\mathsf {g}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\gg \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
; 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash 
\mbox{pcmp}
\rhd \underline{
\mathsf {f}}
\rhd \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}} \wedge \neg \underline{
\mathsf {g}}
\gg \underline{
\mathsf {g}} \wedge \neg \underline{
\mathsf {g}}
; 
\mbox{andelim2}
\rhd \underline{
\mathsf {g}} \wedge \neg \underline{
\mathsf {g}}
\gg \neg \underline{
\mathsf {g}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {g}}
\gg \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {g}}
; 
\mbox{notintro}
\rhd \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\rhd \underline{
\mathsf {f}}
\vdash \neg \underline{
\mathsf {g}}
\gg \neg \underline{
\mathsf {f}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$






\section{Application of natural deduction lemmas}\label{sec:higherproof}
In this section we set out to prove lemma \ref{lem:mainresult} which is the main
result of this project. The content of the lemma is simple, but the formal proof is quite
long. Therefore we have split it into six lemmas. Finally we prove an easy result
containing quantifiers in lemma \ref{lem:lastresult}. We have also tried to prove
$
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {h}}
\colon 
\forall \underline{
\mathsf {p}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {h}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {h}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {g}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {p}}
\Rightarrow \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash \neg \underline{
\mathsf {p}}
\Rightarrow \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)$

but we ran into problems when we tried to used side conditions within blocks. Either we got a false side condition or a metageneralization error. Therefore these
attempts have been removed from our final report.

\begin{Lem}
$
[
\mbox{hlplem1}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\vdash \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {p}}
]$
\end{Lem}
$
[
\mbox{hlplem1}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\vdash \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash 
\mbox{pcmp}
\rhd \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\rhd \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\gg \underline{
\mathsf {q}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {q}}
\rhd \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\gg \underline{
\mathsf {p}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{hlplem2}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\vdash \neg \underline{
\mathsf {p}}
\vdash \underline{
\mathsf {q}}
]$
\end{Lem}

$
[
\mbox{hlplem2}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\vdash \neg \underline{
\mathsf {p}}
\vdash 
\mbox{andintro}
\rhd \underline{
\mathsf {p}}
\rhd \neg \underline{
\mathsf {p}}
\gg \underline{
\mathsf {p}} \wedge \neg \underline{
\mathsf {p}}
; 
\mbox{bottomelim}
\rhd \underline{
\mathsf {p}} \wedge \neg \underline{
\mathsf {p}}
\gg \underline{
\mathsf {q}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{hlplem3}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \neg \underline{
\mathsf {p}}
\vdash \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}} \wedge \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
]$
\end{Lem}

$
[
\mbox{hlplem3}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \neg \underline{
\mathsf {p}}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\vdash 
\mbox{hlplem2}
\rhd \underline{
\mathsf {p}}
\rhd \neg \underline{
\mathsf {p}}
\gg \underline{
\mathsf {q}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\vdash \underline{
\mathsf {q}}
\gg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
; 
\mbox{andintro}
\rhd \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\rhd \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\gg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}} \wedge \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}
$
[
\mbox{hlplem4}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {p}}
]$
\end{Lem}

$
[
\mbox{hlplem4}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \neg \underline{
\mathsf {p}}
\vdash 
\mbox{hlplem3}
\rhd \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\rhd \neg \underline{
\mathsf {p}}
\gg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}} \wedge \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \neg \underline{
\mathsf {p}}
\vdash \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}} \wedge \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\gg \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}} \wedge \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
; 
\mbox{lemnotintro}
\rhd \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}} \wedge \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\gg \neg \neg \underline{
\mathsf {p}}
; 
\mbox{notnotelim}
\rhd \neg \neg \underline{
\mathsf {p}}
\gg \underline{
\mathsf {p}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$


\begin{Lem}
$
[
\mbox{hlplem5}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\vdash \underline{
\mathsf {p}}
]$
\end{Lem}

$
[
\mbox{hlplem5}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\vdash \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash 
\mbox{hlplem1}
\rhd \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\rhd \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\rhd \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\gg \underline{
\mathsf {p}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\vdash \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {p}}
\gg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\rhd \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\gg \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
; 
\mbox{pcmp}
\rhd \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\rhd \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\gg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
; 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash 
\mbox{pcmp}
\rhd \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\rhd \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\gg \underline{
\mathsf {p}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {p}}
\gg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {p}}
; 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash 
\mbox{hlplem4}
\rhd \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\gg \underline{
\mathsf {p}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {p}}
\gg \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {p}}
; 
\mbox{lem}
\gg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}} \vee \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
; 
\mbox{orelim}
\rhd \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}} \vee \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\rhd \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {p}}
\rhd \neg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {p}}
\gg \underline{
\mathsf {p}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}[Main result]\label{lem:mainresult}
$
[
\mbox{goal1}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {p}}
]$
\end{Lem}

$
[
\mbox{goal1}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\vdash 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\vdash 
\mbox{hlplem5}
\rhd \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\rhd \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\gg \underline{
\mathsf {p}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\vdash \underline{
\mathsf {p}}
\gg \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {p}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {p}}
\colon 
\forall \underline{
\mathsf {q}}
\colon \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\vdash \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {p}}
\gg \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {q}}
\Rightarrow \underline{
\mathsf {p}}
\Rightarrow \underline{
\mathsf {p}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}\hspace{1cm}\\
$
[
\mbox{hlplem6}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {h}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {h}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {g}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
]$
\end{Lem}

$
[
\mbox{hlplem6}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf {h}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {h}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {h}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {g}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash 
\mbox{forallelim}
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {h}}
\rceil 
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\langle 
\lceil \underline{
\mathsf {h}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {g}}
\rceil 
\rangle 
\rhd \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\gg \underline{
\mathsf {h}}
; 
\mbox{existsintro}
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {h}}
\rceil 
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\langle 
\lceil \underline{
\mathsf {h}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {g}}
\rceil 
\rangle 
\rhd \underline{
\mathsf {h}}
\gg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{Lem}\label{lem:lastresult}\hspace{1cm}\\
$
[
\mbox{goal2}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {h}}
\colon 
\forall \underline{
\mathsf {k}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {h}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {h}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {g}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash \neg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {k}}
]$
\end{Lem}

$
[
\mbox{goal2}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf {g}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {h}}
\colon 
\forall \underline{
\mathsf {k}}
\colon 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {h}}
\rceil 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {h}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {g}}
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash 
\mbox{hlplem6}
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {g}}
\rceil 
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\lceil \underline{
\mathsf{x}}
\rceil 
\#^0
\lceil \underline{
\mathsf {h}}
\rceil 
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\langle 
\lceil \underline{
\mathsf {h}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {f}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf {g}}
\rceil 
\rangle 
\rhd \forall \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\gg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
; 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {k}}
\colon \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash \neg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash 
\mbox{andintro}
\rhd \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\rhd \neg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\gg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right) \wedge \neg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
; 
\mbox{bottomelim}
\rhd \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right) \wedge \neg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\gg \underline{
\mathsf {k}}
; 
\mbox{pcdeduction}
\rhd 
\forall \underline{
\mathsf {f}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {k}}
\colon \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash \neg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\vdash \underline{
\mathsf {k}}
\gg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \neg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {k}}
; 
\mbox{pcmp}
\rhd \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\rhd \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \neg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {k}}
\gg \neg \exists \underline{
\mathsf{x}} . \left(\underline{
\mathsf {f}}\right)
\Rightarrow \underline{
\mathsf {k}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\begin{appendix}

\section{Ways Logiweb\texttrademark{} could be improved}
Working with Logiweb\texttrademark{} have given us some ideas of how the system could be improved and how it could be made more userfriendly.
Our ideas are summarized below:
\begin{itemize}
\item A getting started manual explaining the basic concepts and quirks of the system including simplified examples. Man pages together with
the base and check pages leaves a lot to be desired.

\item Sample pages / proofs for the current version of the pyk compiler (we have used a lot of time searching other peoples Logiweb\texttrademark{} pages to gain
knowledge but it has often been in vain because the syntax had changed).

\item Better error messages and / or an explanation of how to read them. Also it would be nice if error messages included the line number of the error.

\item It would be nice if \LaTeX{} errors and warnings could be displayed. Just knowing that there is an error leaves a lot of detective work to be done.

\item A pre-parser substituting \texttt{(} with \texttt{parenthesis}, \texttt{)} with \texttt{end parenthesis}, \texttt{,} with \texttt{comma} ect. would be nice.

\end{itemize}


\begin{thebibliography}{99}
%\addcontentsline{toc}{section}{\bibname}
\bibitem[LiCS]{huth} Logic in Computer Science - Modelling and Reasoning about Systems, Second Edition - 2004.\\
\emph{By Michael Huth \& Mark Ryan}\\
ISBN: 0-521-54310-X
\end{thebibliography}


\section{Pyk definitions}

\begin{flushleft}
$
[
\mbox{pred calc}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pred
\linebreak [0]\ \hskip0em plus2.0em{}calc
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc1}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc1
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc2}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc2
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc3}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc3
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc4}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc4
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc5}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc5
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc6}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc6
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc7}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc7
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc8}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc8
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc9}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc9
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc10}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc10
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc11}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc11
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc12}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc12
\mbox{''}
]
\linebreak[4] 
[
\mbox{pcmp}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pcmp
\mbox{''}
]
\linebreak[4] 
[
\mbox{pcunsound}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pcunsound
\mbox{''}
]
\linebreak[4] 
[
\mbox{pcia}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pcia
\mbox{''}
]
\linebreak[4] 
[
\mbox{pcie}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pcie
\mbox{''}
]
\linebreak[4] 
[
\mbox{pcdeduction}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pcdeduction
\mbox{''}
]
\linebreak[4] 
[
\mbox{trivia}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}trivia
\mbox{''}
]
\linebreak[4] 
[
\mbox{repeat}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}repeat
\mbox{''}
]
\linebreak[4] 
[
\mbox{andintro}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}andintro
\mbox{''}
]
\linebreak[4] 
[
\mbox{andelim1}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}andelim1
\mbox{''}
]
\linebreak[4] 
[
\mbox{andelim2}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}andelim2
\mbox{''}
]
\linebreak[4] 
[
\mbox{orintro1}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}orintro1
\mbox{''}
]
\linebreak[4] 
[
\mbox{orintro2}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}orintro2
\mbox{''}
]
\linebreak[4] 
[
\mbox{orelim}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}orelim
\mbox{''}
]
\linebreak[4] 
[
\mbox{notintro}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}notintro
\mbox{''}
]
\linebreak[4] 
[
\mbox{implyintro}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}implyintro
\mbox{''}
]
\linebreak[4] 
[
\mbox{notnotintro}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}notnotintro
\mbox{''}
]
\linebreak[4] 
[
\mbox{notnotelim}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}notnotelim
\mbox{''}
]
\linebreak[4] 
[
\mbox{mt}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}mt
\mbox{''}
]
\linebreak[4] 
[
\mbox{pbc}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pbc
\mbox{''}
]
\linebreak[4] 
[
\mbox{lem}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lem
\mbox{''}
]
\linebreak[4] 
[
\mbox{forallintro}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}forallintro
\mbox{''}
]
\linebreak[4] 
[
\mbox{forallelim}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}forallelim
\mbox{''}
]
\linebreak[4] 
[
\mbox{existsintro}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}existsintro
\mbox{''}
]
\linebreak[4] 
[
\mbox{existselim}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}existselim
\mbox{''}
]
\linebreak[4] 
[
\mbox{bottomelim}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}bottomelim
\mbox{''}
]
\linebreak[4] 
[
\mbox{lemnotintro}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemnotintro
\mbox{''}
]
\linebreak[4] 
[
\mbox{hlplem1}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}hlplem1
\mbox{''}
]
\linebreak[4] 
[
\mbox{hlplem2}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}hlplem2
\mbox{''}
]
\linebreak[4] 
[
\mbox{hlplem3}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}hlplem3
\mbox{''}
]
\linebreak[4] 
[
\mbox{hlplem4}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}hlplem4
\mbox{''}
]
\linebreak[4] 
[
\mbox{hlplem5}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}hlplem5
\mbox{''}
]
\linebreak[4] 
[
\mbox{goal1}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}goal1
\mbox{''}
]
\linebreak[4] 
[
\mbox{hlplem6}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}hlplem6
\mbox{''}
]
\linebreak[4] 
[
\mbox{goal2}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}goal2
\mbox{''}
]
\linebreak[4] 
[
\ast  \equiv 
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}setequiv
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[
\ast  = 
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}setequals
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[\neg 
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lnot
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[
\ast  \wedge 
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}land
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[
\ast  \vee 
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}lor
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[\forall 
\ast  . \left(
\ast \right)
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}forall
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}dot
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}end
\linebreak [0]\ \hskip0em plus2.0em{}forall
\mbox{''}
]
\linebreak[4] 
[\exists 
\ast  . \left(
\ast \right)
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}exists
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}dot
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}end
\linebreak [0]\ \hskip0em plus2.0em{}exists
\mbox{''}
]
\linebreak[4] 
[
\ast  \in 
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}setin
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[
\mbox{finalversion}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}finalversion
\mbox{''}
]
\linebreak[4] $
\end{flushleft}

\section{Tex definitions}
\begin{itemize}
\item $
[\neg 
\mathsf{x}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\mbox {$\backslash $}neg
\linebreak [0]\ \hskip0em plus2.0em{}
\#1.
\mbox{''}
]$
\item $
[
\mathsf{x} \wedge 
\mathsf{y}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}wedge
\linebreak [0]\ \hskip0em plus2.0em{}
\#2.
\mbox{''}
]$
\item $
[
\mathsf{x} \vee 
\mathsf{y}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}vee
\linebreak [0]\ \hskip0em plus2.0em{}
\#2.
\mbox{''}
]$
\item $
[
\mathsf{x}
\Rightarrow 
\mathsf{y}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}Rightarrow
\linebreak [0]\ \hskip0em plus2.0em{}
\#2.
\mbox{''}
]$
\item $
[\forall 
\mathsf{y} . \left(
\mathsf {b}\right)
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\mbox {$\backslash $}forall
\linebreak [0]\ \hskip0em plus2.0em{}
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}.
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}left(
\#2.
\mbox {$\backslash $}right)
\mbox{''}
]$
\item $
[\exists 
\mathsf{y} . \left(
\mathsf {b}\right)
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\mbox {$\backslash $}exists
\linebreak [0]\ \hskip0em plus2.0em{}
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}.
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}left(
\#2.
\mbox {$\backslash $}right)
\mbox{''}
]$
\item $
[
\mathsf{y} \in 
\mathsf {b}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}in
\linebreak [0]\ \hskip0em plus2.0em{}
\#2.
\mbox{''}
]$
\item $
[
\mathsf{y} \equiv 
\mathsf {b}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}equiv
\linebreak [0]\ \hskip0em plus2.0em{}
\#2.
\mbox{''}
]$
\item $
[
\mathsf{y} = 
\mathsf {b}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}
{=}
\linebreak [0]\ \hskip0em plus2.0em{}
\#2.
\mbox{''}
]$
\end{itemize}

\section{Priority table}

\begin {flushleft}$
[
\mbox{finalversion}
\stackrel{
\mathrm{prio}
}{\rightarrow}
\newline \mathbf {Preassociative} \newline 
[
\mbox{finalversion}
] , \linebreak [0] 
[
\mbox{base}
] , \linebreak [0] 
[
\mbox{bracket $
\ast $ end bracket}
] , \linebreak [0] 
[
\mbox{big bracket $
\ast $ end bracket}
] , \linebreak [0] 
[
\ \$
\ast \$\linebreak[0]\ 
] , \linebreak [0] 
[
\mathbf{flush\ left\ }[ 
\ast 
]
] , \linebreak [0] 
[
\mathsf{x}
] , \linebreak [0] 
[
\mathsf{y}
] , \linebreak [0] 
[
\mathsf{z}
] , \linebreak [0] 
[
[
\ast 
\bowtie
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\stackrel{
\ast 
}{\rightarrow}
\ast 
]
] , \linebreak [0] 
[
\mathrm{pyk}
] , \linebreak [0] 
[
\mathrm{tex}
] , \linebreak [0] 
[
\mathrm{name}
] , \linebreak [0] 
[
\mathrm{prio}
] , \linebreak [0] 
[
\ast 
] , \linebreak [0] 
[
\mathsf {T}
] , \linebreak [0] 
[
\mathrm {if}(
\ast 
,\linebreak [0]
\ast 
,\linebreak [0]
\ast 
)
] , \linebreak [0] 
[
[
\ast 
\stackrel {
\ast 
}{\Rightarrow }
\ast 
]
] , \linebreak [0] 
[
\mathrm {val}
] , \linebreak [0] 
[
\mathrm {claim}
] , \linebreak [0] 
[
\bot 
] , \linebreak [0] 
[
f(
\ast 
)
] , \linebreak [0] 
[
(
\ast 
){}^{I} 
] , \linebreak [0] 
[
\mathsf {F}
] , \linebreak [0] 
[
\underline {0}
] , \linebreak [0] 
[
\underline {1}
] , \linebreak [0] 
[
\underline {2}
] , \linebreak [0] 
[
\underline {3}
] , \linebreak [0] 
[
\underline {4}
] , \linebreak [0] 
[
\underline {5}
] , \linebreak [0] 
[
\underline {6}
] , \linebreak [0] 
[
\underline {7}
] , \linebreak [0] 
[
\underline {8}
] , \linebreak [0] 
[
\underline {9}
] , \linebreak [0] 
[
0
] , \linebreak [0] 
[
1
] , \linebreak [0] 
[
2
] , \linebreak [0] 
[
3
] , \linebreak [0] 
[
4
] , \linebreak [0] 
[
5
] , \linebreak [0] 
[
6
] , \linebreak [0] 
[
7
] , \linebreak [0] 
[
8
] , \linebreak [0] 
[
9
] , \linebreak [0] 
[
\mathsf {a}
] , \linebreak [0] 
[
\mathsf {b}
] , \linebreak [0] 
[
\mathsf {c}
] , \linebreak [0] 
[
\mathsf {d}
] , \linebreak [0] 
[
\mathsf {e}
] , \linebreak [0] 
[
\mathsf {f}
] , \linebreak [0] 
[
\mathsf {g}
] , \linebreak [0] 
[
\mathsf {h}
] , \linebreak [0] 
[
\mathsf {i}
] , \linebreak [0] 
[
\mathsf {j}
] , \linebreak [0] 
[
\mathsf {k}
] , \linebreak [0] 
[
\mathsf {l}
] , \linebreak [0] 
[
\mathsf {m}
] , \linebreak [0] 
[
\mathsf {n}
] , \linebreak [0] 
[
\mathsf {o}
] , \linebreak [0] 
[
\mathsf {p}
] , \linebreak [0] 
[
\mathsf {q}
] , \linebreak [0] 
[
\mathsf {r}
] , \linebreak [0] 
[
\mathsf {s}
] , \linebreak [0] 
[
\mathsf {t}
] , \linebreak [0] 
[
\mathsf {u}
] , \linebreak [0] 
[
\mathsf {v}
] , \linebreak [0] 
[
\mathsf {w}
] , \linebreak [0] 
[
(
\ast 
)^M
] , \linebreak [0] 
[
\mathrm {If}(
\ast 
,\linebreak [0]
\ast 
,\linebreak [0]
\ast 
)
] , \linebreak [0] 
[\mathrm {array}\{
\ast 
\}
\ast 
\mathrm {end\ array}
] , \linebreak [0] 
[
l
] , \linebreak [0] 
[
c
] , \linebreak [0] 
[
r
] , \linebreak [0] 
[
\mathrm {empty}
] , \linebreak [0] 
[
\langle 
\ast 
\,{|}
\ast 
{:=}\,
\ast 
\rangle 
] , \linebreak [0] 
[
{\cal M}(
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal U}}(
\ast 
)
] , \linebreak [0] 
[
{\cal U}(
\ast 
)
] , \linebreak [0] 
[
{\cal U}^M(
\ast 
)
] , \linebreak [0] 
[
\mathbf {apply}(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathbf {apply}_1(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
identifier( 
\ast 
)
] , \linebreak [0] 
[
identifier_{1}( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
array\mbox{-}\linebreak[0]plus( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
array\mbox{-}\linebreak[0]remove( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
array\mbox{-}\linebreak[0]put( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
array\mbox{-}\linebreak[0]add( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
bit( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
bit_1( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
rack
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {vector}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {bibliography}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {dictionary}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {body}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {codex}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {expansion}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {code}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {cache}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {diagnose}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {pyk}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {tex}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {texname}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {value}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {message}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {macro}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {definition}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {unpack}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {claim}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {priority}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {lambda}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {apply}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {true}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {if}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {quote}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {proclaim}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {define}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {introduce}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {hide}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {pre}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {post}\mbox {\tt \char34}
] , \linebreak [0] 
[
{\cal E}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal E}_2(
\ast 
,
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal E}_3(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal E}_4(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathbf {lookup}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathbf {abstract}(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\lceil 
\ast 
\rceil 
] , \linebreak [0] 
[
{\cal M}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal M}_2(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal M}^*(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathrm {macro}
] , \linebreak [0] 
[
s_0
] , \linebreak [0] 
[
\mathbf {zip}(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathbf {assoc}_1(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[(
\ast 
)^{\mathbf {p}}
] , \linebreak [0] 
[
\mbox{self}
] , \linebreak [0] 
[
[
\ast 
\mathrel {\ddot {=}}
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\mathrel {\dot {=}}
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\mathrel {\acute {=}}
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\stackrel {\mathrm {pyk}}{=} 
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\stackrel {\mathrm {tex}}{=} 
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\stackrel {\mathrm {name}}{=} 
\ast 
]
] , \linebreak [0] 
[
\mathbf{Priority\ table} [ 
\ast 
]
] , \linebreak [0] 
[
\tilde {{\cal M}}_1
] , \linebreak [0] 
[
\tilde {{\cal M}}_2(
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal M}}_3(
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal M}}_4(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal M}}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal Q}}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal Q}}_2(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal Q}}_3(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal Q}}^*(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
(
\ast 
)
] , \linebreak [0] 
[
\left( 
\ast 
\right) 
] , \linebreak [0] 
[
display(
\ast 
)
] , \linebreak [0] 
[
statement(
\ast 
)
] , \linebreak [0] 
[
[
\ast 
]^{\cdot}
] , \linebreak [0] 
[
[
\ast 
]^-
] , \linebreak [0] 
[
\mathbf{aspect}( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{aspect}( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\langle 
\ast 
\rangle 
] , \linebreak [0] 
[
\mathbf {tuple}_1( 
\ast 
) 
] , \linebreak [0] 
[
\mathbf {tuple}_2( 
\ast 
) 
] , \linebreak [0] 
[
let_2( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
let_1( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
[
\ast 
\stackrel {claim}{=}
\ast 
]
] , \linebreak [0] 
[
\mbox{checker}
] , \linebreak [0] 
[
\mathbf{check}( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{check}_2( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{check}_3( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{check}^*( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{check}^*_2( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\relax [ 
\ast 
\relax ]^{\cdot} 
] , \linebreak [0] 
[
\relax [ 
\ast 
\relax ]^{-} 
] , \linebreak [0] 
[
\relax [ 
\ast 
\relax ]^{\circ} 
] , \linebreak [0] 
[
msg
] , \linebreak [0] 
[
[
\ast 
\stackrel {msg}{=} 
\ast 
]
] , \linebreak [0] 
[
{<}stmt{>}
] , \linebreak [0] 
[
stmt
] , \linebreak [0] 
[
[
\ast 
\stackrel {stmt}{=}
\ast 
]
] , \linebreak [0] 
[
HeadNil'
] , \linebreak [0] 
[
HeadPair'
] , \linebreak [0] 
[
Transitivity'
] , \linebreak [0] 
[
{\makebox [0mm][l]{$\bot $}\,{\bot }}
] , \linebreak [0] 
[
Contra'
] , \linebreak [0] 
[
T'_{E}
] , \linebreak [0] 
[
L_{1}
] , \linebreak [0] 
[\underline{
\ast }
] , \linebreak [0] 
[{\cal A}
] , \linebreak [0] 
[{\cal B}
] , \linebreak [0] 
[{\cal C}
] , \linebreak [0] 
[{\cal D}
] , \linebreak [0] 
[{\cal E}
] , \linebreak [0] 
[{\cal F}
] , \linebreak [0] 
[{\cal G}
] , \linebreak [0] 
[{\cal H}
] , \linebreak [0] 
[{\cal I}
] , \linebreak [0] 
[{\cal J}
] , \linebreak [0] 
[{\cal K}
] , \linebreak [0] 
[{\cal L}
] , \linebreak [0] 
[{\cal M}
] , \linebreak [0] 
[{\cal N}
] , \linebreak [0] 
[{\cal O}
] , \linebreak [0] 
[{\cal P}
] , \linebreak [0] 
[{\cal Q}
] , \linebreak [0] 
[{\cal R}
] , \linebreak [0] 
[{\cal S}
] , \linebreak [0] 
[{\cal T}
] , \linebreak [0] 
[{\cal U}
] , \linebreak [0] 
[{\cal V}
] , \linebreak [0] 
[{\cal W}
] , \linebreak [0] 
[{\cal X}
] , \linebreak [0] 
[{\cal Y}
] , \linebreak [0] 
[{\cal Z}
] , \linebreak [0] 
[
\langle 
\ast 
\,{\protect\vert}
\ast 
{:=}\,
\ast 
\rangle 
] , \linebreak [0] 
[
\langle ^ { \ast } 
\ast 
\,{\protect\vert}
\ast 
{:=}\,
\ast 
\rangle 
] , \linebreak [0] 
[
\emptyset 
] , \linebreak [0] 
[
Remainder
] , \linebreak [0] 
[
( 
\ast 
)^{\bf v}
] , \linebreak [0] 
[
intro(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
intro(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
error(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
error_{2}(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
proof( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
proof_{2}( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{I}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\rhd}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\rhd}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{E}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{E}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{+}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{+}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{-}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{-}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\ast}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\ast}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{2}^{\ast}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\char64}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\char64}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\vdash}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\vdash}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\makebox [0mm][l]{\scriptsize $\vdash $}\,{\vdash }}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\makebox [0mm][l]{\scriptsize $\vdash $}\,{\vdash }}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{i.e.}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{i.e.}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{2}^{i.e.}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\forall}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\forall}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{;}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{;}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{2}^{;}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal T}( 
\ast 
)
] , \linebreak [0] 
[
claims( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
claims_2( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{<}proof{>}
] , \linebreak [0] 
[
proof
] , \linebreak [0] 
[
[ \mathbf{Lemma\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ \mathbf{Proof\ of\ }
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ 
\ast 
\mathbf{\ lemma\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ 
\ast 
\mathbf{\ antilemma\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ 
\ast 
\mathbf{\ rule\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ 
\ast 
\mathbf{\ antirule\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
\mbox{verifier}
] , \linebreak [0] 
[
{\cal V}_1( 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_2( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_3( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_4( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_5( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_6( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_7( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
Cut( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
Head_{\oplus} ( 
\ast 
)
] , \linebreak [0] 
[
Tail_{\oplus} ( 
\ast 
)
] , \linebreak [0] 
[
rule_1( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
rule( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
Rule\ tactic
] , \linebreak [0] 
[
Plus( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
[ \mathbf{Theory\ } 
\ast 
]
] , \linebreak [0] 
[
theory_2( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
theory_3( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
theory_4( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
HeadNil''
] , \linebreak [0] 
[
HeadPair''
] , \linebreak [0] 
[
Transitivity''
] , \linebreak [0] 
[
Contra''
] , \linebreak [0] 
[
HeadNil
] , \linebreak [0] 
[
HeadPair
] , \linebreak [0] 
[
Transitivity
] , \linebreak [0] 
[
Contra
] , \linebreak [0] 
[
T_E
] , \linebreak [0] 
[
ragged\ right
] , \linebreak [0] 
[
ragged\ right\ expansion\ 
] , \linebreak [0] 
[
parm(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
parm^*(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
inst(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
inst^*(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
occur(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
occur^*(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
unify(
\ast 
=
\ast 
,
\ast 
)
] , \linebreak [0] 
[
unify^*(
\ast 
=
\ast 
,
\ast 
)
] , \linebreak [0] 
[
unify_2(
\ast 
=
\ast 
,
\ast 
)
] , \linebreak [0] 
[L_a
] , \linebreak [0] 
[L_b
] , \linebreak [0] 
[L_c
] , \linebreak [0] 
[L_d
] , \linebreak [0] 
[L_e
] , \linebreak [0] 
[L_f
] , \linebreak [0] 
[L_g
] , \linebreak [0] 
[L_h
] , \linebreak [0] 
[L_i
] , \linebreak [0] 
[L_j
] , \linebreak [0] 
[L_k
] , \linebreak [0] 
[L_l
] , \linebreak [0] 
[L_m
] , \linebreak [0] 
[L_n
] , \linebreak [0] 
[L_o
] , \linebreak [0] 
[L_p
] , \linebreak [0] 
[L_q
] , \linebreak [0] 
[L_r
] , \linebreak [0] 
[L_s
] , \linebreak [0] 
[L_t
] , \linebreak [0] 
[L_u
] , \linebreak [0] 
[L_v
] , \linebreak [0] 
[L_w
] , \linebreak [0] 
[L_x
] , \linebreak [0] 
[L_y
] , \linebreak [0] 
[L_z
] , \linebreak [0] 
[L_A
] , \linebreak [0] 
[L_B
] , \linebreak [0] 
[L_C
] , \linebreak [0] 
[L_D
] , \linebreak [0] 
[L_E
] , \linebreak [0] 
[L_F
] , \linebreak [0] 
[L_G
] , \linebreak [0] 
[L_H
] , \linebreak [0] 
[L_I
] , \linebreak [0] 
[L_J
] , \linebreak [0] 
[L_K
] , \linebreak [0] 
[L_L
] , \linebreak [0] 
[L_M
] , \linebreak [0] 
[L_N
] , \linebreak [0] 
[L_O
] , \linebreak [0] 
[L_P
] , \linebreak [0] 
[L_Q
] , \linebreak [0] 
[L_R
] , \linebreak [0] 
[L_S
] , \linebreak [0] 
[L_T
] , \linebreak [0] 
[L_U
] , \linebreak [0] 
[L_V
] , \linebreak [0] 
[L_W
] , \linebreak [0] 
[L_X
] , \linebreak [0] 
[L_Y
] , \linebreak [0] 
[L_Z
] , \linebreak [0] 
[L_?
] , \linebreak [0] 
[
Reflexivity
] , \linebreak [0] 
[
Reflexivity_1
] , \linebreak [0] 
[
Commutativity
] , \linebreak [0] 
[
Commutativity_1
] , \linebreak [0] 
[
{<}tactic{>}
] , \linebreak [0] 
[
tactic
] , \linebreak [0] 
[
[
\ast 
\stackrel {tactic}{=}
\ast 
]
] , \linebreak [0] 
[
{\cal P}( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal P}^*( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
p_0
] , \linebreak [0] 
[
conclude_1 ( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
conclude_2 ( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
conclude_3 ( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
conclude_4 ( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mbox{check}
] , \linebreak [0] 
[
[
\ast 
\stackrel {\circ}{=}
\ast 
]
] , \linebreak [0] 
[
RootVisible(
\ast 
)
] , \linebreak [0] 
[
A
] , \linebreak [0] 
[
R
] , \linebreak [0] 
[
C
] , \linebreak [0] 
[
T
] , \linebreak [0] 
[
L
] , \linebreak [0] 
[
\{
\ast 
\}
] , \linebreak [0] 
[\overline{
\ast }
] , \linebreak [0] 
[
\mathit{a}
] , \linebreak [0] 
[
\mathit{b}
] , \linebreak [0] 
[
\mathit{c}
] , \linebreak [0] 
[
\mathit{d}
] , \linebreak [0] 
[
\mathit{e}
] , \linebreak [0] 
[
\mathit{f}
] , \linebreak [0] 
[
\mathit{g}
] , \linebreak [0] 
[
\mathit{h}
] , \linebreak [0] 
[
\mathit{i}
] , \linebreak [0] 
[
\mathit{j}
] , \linebreak [0] 
[
\mathit{k}
] , \linebreak [0] 
[
\mathit{l}
] , \linebreak [0] 
[
\mathit{m}
] , \linebreak [0] 
[
\mathit{n}
] , \linebreak [0] 
[
\mathit{o}
] , \linebreak [0] 
[
\mathit{p}
] , \linebreak [0] 
[
\mathit{q}
] , \linebreak [0] 
[
\mathit{r}
] , \linebreak [0] 
[
\mathit{s}
] , \linebreak [0] 
[
\mathit{t}
] , \linebreak [0] 
[
\mathit{u}
] , \linebreak [0] 
[
\mathit{v}
] , \linebreak [0] 
[
\mathit{w}
] , \linebreak [0] 
[
\mathit{x}
] , \linebreak [0] 
[
\mathit{y}
] , \linebreak [0] 
[
\mathit{z}
] , \linebreak [0] 
[
\langle 
\ast 
{\equiv} 
\ast 
| 
\ast 
{:=} 
\ast 
\rangle 
] , \linebreak [0] 
[
\langle 
\ast 
{\equiv}^0 
\ast 
| 
\ast 
{:=} 
\ast 
\rangle 
] , \linebreak [0] 
[
\langle 
\ast 
{\equiv}^1 
\ast 
| 
\ast 
{:=} 
\ast 
\rangle 
] , \linebreak [0] 
[
\langle 
\ast 
{\equiv}^* 
\ast 
| 
\ast 
{:=} 
\ast 
\rangle 
] , \linebreak [0] 
[
Ded(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_0(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_1(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_2(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_3(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_4(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_4^*(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_5(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_6(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_6^*(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_7(
\ast 
)
] , \linebreak [0] 
[
Ded_8(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_8^*(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
S
] , \linebreak [0] 
[
Neg
] , \linebreak [0] 
[
MP
] , \linebreak [0] 
[
Gen
] , \linebreak [0] 
[
Ded
] , \linebreak [0] 
[
S1
] , \linebreak [0] 
[
S2
] , \linebreak [0] 
[
S3
] , \linebreak [0] 
[
S4
] , \linebreak [0] 
[
S5
] , \linebreak [0] 
[
S6
] , \linebreak [0] 
[
S7
] , \linebreak [0] 
[
S8
] , \linebreak [0] 
[
S9
] , \linebreak [0] 
[
Repetition
] , \linebreak [0] 
[
A1'
] , \linebreak [0] 
[
A2'
] , \linebreak [0] 
[
A4'
] , \linebreak [0] 
[
A5'
] , \linebreak [0] 
[
Prop\ 3.2a
] , \linebreak [0] 
[
Prop\ 3.2b
] , \linebreak [0] 
[
Prop\ 3.2c
] , \linebreak [0] 
[
Prop\ 3.2d
] , \linebreak [0] 
[
Prop\ 3.2e_1
] , \linebreak [0] 
[
Prop\ 3.2e_2
] , \linebreak [0] 
[
Prop\ 3.2e
] , \linebreak [0] 
[
Prop\ 3.2f_1
] , \linebreak [0] 
[
Prop\ 3.2f_2
] , \linebreak [0] 
[
Prop\ 3.2f
] , \linebreak [0] 
[
Prop\ 3.2g_1
] , \linebreak [0] 
[
Prop\ 3.2g_2
] , \linebreak [0] 
[
Prop\ 3.2g
] , \linebreak [0] 
[
Prop\ 3.2h_1
] , \linebreak [0] 
[
Prop\ 3.2h_2
] , \linebreak [0] 
[
Prop\ 3.2h
] , \linebreak [0] 
[
Block_1(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Block_2(
\ast 
)
] , \linebreak [0] 
[
\mbox{pred calc}
] , \linebreak [0] 
[
\mbox{pc1}
] , \linebreak [0] 
[
\mbox{pc2}
] , \linebreak [0] 
[
\mbox{pc3}
] , \linebreak [0] 
[
\mbox{pc4}
] , \linebreak [0] 
[
\mbox{pc5}
] , \linebreak [0] 
[
\mbox{pc6}
] , \linebreak [0] 
[
\mbox{pc7}
] , \linebreak [0] 
[
\mbox{pc8}
] , \linebreak [0] 
[
\mbox{pc9}
] , \linebreak [0] 
[
\mbox{pc10}
] , \linebreak [0] 
[
\mbox{pc11}
] , \linebreak [0] 
[
\mbox{pc12}
] , \linebreak [0] 
[
\mbox{pcmp}
] , \linebreak [0] 
[
\mbox{pcunsound}
] , \linebreak [0] 
[
\mbox{pcia}
] , \linebreak [0] 
[
\mbox{pcie}
] , \linebreak [0] 
[
\mbox{pcdeduction}
] , \linebreak [0] 
[
\mbox{trivia}
] , \linebreak [0] 
[
\mbox{repeat}
] , \linebreak [0] 
[
\mbox{andintro}
] , \linebreak [0] 
[
\mbox{andelim1}
] , \linebreak [0] 
[
\mbox{andelim2}
] , \linebreak [0] 
[
\mbox{orintro1}
] , \linebreak [0] 
[
\mbox{orintro2}
] , \linebreak [0] 
[
\mbox{orelim}
] , \linebreak [0] 
[
\mbox{notintro}
] , \linebreak [0] 
[
\mbox{implyintro}
] , \linebreak [0] 
[
\mbox{notnotintro}
] , \linebreak [0] 
[
\mbox{notnotelim}
] , \linebreak [0] 
[
\mbox{mt}
] , \linebreak [0] 
[
\mbox{pbc}
] , \linebreak [0] 
[
\mbox{lem}
] , \linebreak [0] 
[
\mbox{forallintro}
] , \linebreak [0] 
[
\mbox{forallelim}
] , \linebreak [0] 
[
\mbox{existsintro}
] , \linebreak [0] 
[
\mbox{existselim}
] , \linebreak [0] 
[
\mbox{bottomelim}
] , \linebreak [0] 
[
\mbox{lemnotintro}
] , \linebreak [0] 
[
\mbox{hlplem1}
] , \linebreak [0] 
[
\mbox{hlplem2}
] , \linebreak [0] 
[
\mbox{hlplem3}
] , \linebreak [0] 
[
\mbox{hlplem4}
] , \linebreak [0] 
[
\mbox{hlplem5}
] , \linebreak [0] 
[
\mbox{goal1}
] , \linebreak [0] 
[
\mbox{hlplem6}
] , \linebreak [0] 
[
\mbox{goal2}
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\_\{
\ast 
\}
] , \linebreak [0] 
[
\ast 
/indexintro(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast 
/intro(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast 
/bothintro(
\ast 
,
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast 
/nameintro(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast '
] , \linebreak [0] 
[
\ast 
{[}
\ast 
{]}
] , \linebreak [0] 
[
\ast 
[ 
\ast 
{\rightarrow} 
\ast 
]
] , \linebreak [0] 
[
\ast 
[ 
\ast 
{\Rightarrow} 
\ast 
]
] , \linebreak [0] 
[
\ast 
0
] , \linebreak [0] 
[
\ast 
1
] , \linebreak [0] 
[
0 \mathrm {b}
] , \linebreak [0] 
[
\ast 
\mbox {-color}( 
\ast 
)
] , \linebreak [0] 
[
\ast 
\mbox {-color}^{\ast}( 
\ast 
)
] , \linebreak [0] 
[
\ast 
{}^H
] , \linebreak [0] 
[
\ast 
{}^T
] , \linebreak [0] 
[
\ast 
{}^U
] , \linebreak [0] 
[
\ast 
{}^h
] , \linebreak [0] 
[
\ast 
{}^t
] , \linebreak [0] 
[
\ast 
{}^s
] , \linebreak [0] 
[
\ast 
{}^c
] , \linebreak [0] 
[
\ast 
{}^d
] , \linebreak [0] 
[
\ast 
{}^a
] , \linebreak [0] 
[
\ast 
{}^C
] , \linebreak [0] 
[
\ast 
{}^M
] , \linebreak [0] 
[
\ast 
{}^B
] , \linebreak [0] 
[
\ast 
{}^{r}
] , \linebreak [0] 
[
\ast 
{}^{i}
] , \linebreak [0] 
[
\ast 
{}^{d}
] , \linebreak [0] 
[
\ast 
{}^{R}
] , \linebreak [0] 
[
\ast 
{}^{0}
] , \linebreak [0] 
[
\ast 
{}^{1}
] , \linebreak [0] 
[
\ast 
{}^{2}
] , \linebreak [0] 
[
\ast 
{}^{3}
] , \linebreak [0] 
[
\ast 
{}^{4}
] , \linebreak [0] 
[
\ast 
{}^{5}
] , \linebreak [0] 
[
\ast 
{}^{6}
] , \linebreak [0] 
[
\ast 
{}^{7}
] , \linebreak [0] 
[
\ast 
{}^{8}
] , \linebreak [0] 
[
\ast 
{}^{9}
] , \linebreak [0] 
[
\ast 
{} ^ { E }
] , \linebreak [0] 
[
\ast 
{} ^ {\cal V}
] , \linebreak [0] 
[
\ast 
{} ^ {\cal C}
] , \linebreak [0] 
[
\ast 
{} ^ {{\cal C} ^ { \ast }}
] , \linebreak [0] 
[
\ast 
{}^{hide}
]
; 
\newline \mathbf {Preassociative} \newline 
[
\mbox{``}
\ast 
\mbox{''}
] , \linebreak [0] 
[
] , \linebreak [0] 
[
(
\ast 
)^{\bf t}
] , \linebreak [0] 
[
\mbox{string}(
\ast 
)+
\ast 
] , \linebreak [0] 
[\mbox{string}(
\ast 
)\mathrel{++}
\ast 
] , \linebreak [0] 
[
\newline 
\ast 
] , \linebreak [0] 
[
\linebreak [0]\ \hskip0em plus2.0em{}
\ast 
] , \linebreak [0] 
[!
\ast 
] , \linebreak [0] 
[
\mbox {\tt \char34}
\ast 
] , \linebreak [0] 
[
\#
\ast 
] , \linebreak [0] 
[
\$
\ast 
] , \linebreak [0] 
[
\%
\ast 
] , \linebreak [0] 
[
\&
\ast 
] , \linebreak [0] 
[
\mbox {'}
\ast 
] , \linebreak [0] 
[(
\ast 
] , \linebreak [0] 
[)
\ast 
] , \linebreak [0] 
[
{*}
\ast 
] , \linebreak [0] 
[
{+}
\ast 
] , \linebreak [0] 
[,
\ast 
] , \linebreak [0] 
[
\mbox{-}
\ast 
] , \linebreak [0] 
[.
\ast 
] , \linebreak [0] 
[/
\ast 
] , \linebreak [0] 
[0
\ast 
] , \linebreak [0] 
[1
\ast 
] , \linebreak [0] 
[2
\ast 
] , \linebreak [0] 
[3
\ast 
] , \linebreak [0] 
[4
\ast 
] , \linebreak [0] 
[5
\ast 
] , \linebreak [0] 
[6
\ast 
] , \linebreak [0] 
[7
\ast 
] , \linebreak [0] 
[8
\ast 
] , \linebreak [0] 
[9
\ast 
] , \linebreak [0] 
[
{:}
\ast 
] , \linebreak [0] 
[;
\ast 
] , \linebreak [0] 
[
{<}
\ast 
] , \linebreak [0] 
[
{=}
\ast 
] , \linebreak [0] 
[
{>}
\ast 
] , \linebreak [0] 
[?
\ast 
] , \linebreak [0] 
[@
\ast 
] , \linebreak [0] 
[A
\ast 
] , \linebreak [0] 
[B
\ast 
] , \linebreak [0] 
[C
\ast 
] , \linebreak [0] 
[D
\ast 
] , \linebreak [0] 
[E
\ast 
] , \linebreak [0] 
[F
\ast 
] , \linebreak [0] 
[G
\ast 
] , \linebreak [0] 
[H
\ast 
] , \linebreak [0] 
[I
\ast 
] , \linebreak [0] 
[J
\ast 
] , \linebreak [0] 
[K
\ast 
] , \linebreak [0] 
[L
\ast 
] , \linebreak [0] 
[M
\ast 
] , \linebreak [0] 
[N
\ast 
] , \linebreak [0] 
[O
\ast 
] , \linebreak [0] 
[P
\ast 
] , \linebreak [0] 
[Q
\ast 
] , \linebreak [0] 
[R
\ast 
] , \linebreak [0] 
[S
\ast 
] , \linebreak [0] 
[T
\ast 
] , \linebreak [0] 
[U
\ast 
] , \linebreak [0] 
[V
\ast 
] , \linebreak [0] 
[W
\ast 
] , \linebreak [0] 
[X
\ast 
] , \linebreak [0] 
[Y
\ast 
] , \linebreak [0] 
[Z
\ast 
] , \linebreak [0] 
[[
\ast 
] , \linebreak [0] 
[
\mbox {$\backslash $}
\ast 
] , \linebreak [0] 
[]
\ast 
] , \linebreak [0] 
[
{\char94}
\ast 
] , \linebreak [0] 
[
\_
\ast 
] , \linebreak [0] 
[
\mbox {`}
\ast 
] , \linebreak [0] 
[a
\ast 
] , \linebreak [0] 
[b
\ast 
] , \linebreak [0] 
[c
\ast 
] , \linebreak [0] 
[d
\ast 
] , \linebreak [0] 
[e
\ast 
] , \linebreak [0] 
[f
\ast 
] , \linebreak [0] 
[g
\ast 
] , \linebreak [0] 
[h
\ast 
] , \linebreak [0] 
[i
\ast 
] , \linebreak [0] 
[j
\ast 
] , \linebreak [0] 
[k
\ast 
] , \linebreak [0] 
[l
\ast 
] , \linebreak [0] 
[m
\ast 
] , \linebreak [0] 
[n
\ast 
] , \linebreak [0] 
[o
\ast 
] , \linebreak [0] 
[p
\ast 
] , \linebreak [0] 
[q
\ast 
] , \linebreak [0] 
[r
\ast 
] , \linebreak [0] 
[s
\ast 
] , \linebreak [0] 
[t
\ast 
] , \linebreak [0] 
[u
\ast 
] , \linebreak [0] 
[v
\ast 
] , \linebreak [0] 
[w
\ast 
] , \linebreak [0] 
[x
\ast 
] , \linebreak [0] 
[y
\ast 
] , \linebreak [0] 
[z
\ast 
] , \linebreak [0] 
[
\{
\ast 
] , \linebreak [0] 
[|
\ast 
] , \linebreak [0] 
[
\}
\ast 
] , \linebreak [0] 
[
\char126 
\ast 
] , \linebreak [0] 
[
\mathbf{Preassociative}\,
\ast 
; 
\ast 
] , \linebreak [0] 
[
\mathbf{Postassociative}\,
\ast 
; 
\ast 
] , \linebreak [0] 
[
[
\ast 
] , \linebreak [0] 
\ast 
] , \linebreak [0] 
[
\mathrm{priority} \,
\ast 
\, \mathrm{end}
] , \linebreak [0] 
[
newline\ 
\ast 
] , \linebreak [0] 
[
macro\ newline\ 
\ast 
] , \linebreak [0] 
[
MacroIndent(
\ast 
)
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\mathbin {\mbox {'}}
\ast 
] , \linebreak [0] 
[
\ast 
\mathbin {\mbox {`}}
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
{}'
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\mathbin {\mbox {'}}
\ast 
] , \linebreak [0] 
[
\ast 
\mathbin {\mbox {`}}
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\cdot 
\ast 
] , \linebreak [0] 
[
\ast 
\cdot_0 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
+ 
\ast 
] , \linebreak [0] 
[
\ast 
\mathop{+_0} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathop{+_1} 
\ast 
] , \linebreak [0] 
[
\ast 
- 
\ast 
] , \linebreak [0] 
[
\ast 
\mathop{-_0} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathop{-_1} 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\cup \{ 
\ast 
\}
] , \linebreak [0] 
[
\ast 
\cup 
\ast 
] , \linebreak [0] 
[
\ast 
\backslash \{ 
\ast 
\}
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel { \dot { . \, . } }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { \underline { \dot { . \, . } } }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { \underline { : \, : } }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { \underline { {+} 2 \ast } }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { : \, : }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { {+} 2 \ast }
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
,\linebreak [0] 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\stackrel {B}{\approx }
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {D}{\approx }
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {C}{\approx }
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {P}{\approx }
\ast 
] , \linebreak [0] 
[
\ast 
\approx 
\ast 
] , \linebreak [0] 
[
\ast 
=
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {+}{\rightarrow }
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {t}{=}
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {t^*}{=}
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel{r}{=} 
\ast 
] , \linebreak [0] 
[
\ast 
\in_t 
\ast 
] , \linebreak [0] 
[
\ast 
\subseteq_T 
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel{T}{=} 
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel{s}{=} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {free\ in} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {free\ in}^{\ast} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {free\ for} 
\ast 
\mathrel {in} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {free\ for}^{\ast} 
\ast 
\mathrel {in} 
\ast 
] , \linebreak [0] 
[
\ast 
\in_c 
\ast 
] , \linebreak [0] 
[
\ast 
< 
\ast 
] , \linebreak [0] 
[
\ast 
<' 
\ast 
] , \linebreak [0] 
[
\ast 
\le' 
\ast 
] , \linebreak [0] 
[
\ast 
= 
\ast 
] , \linebreak [0] 
[
\ast 
\neq 
\ast 
] , \linebreak [0] 
[
\ast 
{}^{var}
] , \linebreak [0] 
[
\ast 
\#^0
\ast 
] , \linebreak [0] 
[
\ast 
\#^1
\ast 
] , \linebreak [0] 
[
\ast 
\#^*
\ast 
] , \linebreak [0] 
[
\ast  \equiv 
\ast 
] , \linebreak [0] 
[
\ast  = 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
{\neg }
\ast 
] , \linebreak [0] 
[\neg 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\wedge 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{\ddot{\wedge}} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{\tilde{\wedge}} 
\ast 
] , \linebreak [0] 
[
\ast 
\wedge_c 
\ast 
] , \linebreak [0] 
[
\ast  \wedge 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\vee 
\ast 
] , \linebreak [0] 
[
\ast 
\parallel 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{\ddot{\vee}} 
\ast 
] , \linebreak [0] 
[
\ast  \vee 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\exists 
\ast 
\colon 
\ast 
] , \linebreak [0] 
[
\forall 
\ast 
\colon 
\ast 
] , \linebreak [0] 
[
\forall_{obj} 
\ast 
\colon 
\ast 
] , \linebreak [0] 
[\forall 
\ast  . \left(
\ast \right)
] , \linebreak [0] 
[\exists 
\ast  . \left(
\ast \right)
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel{\ddot{\Rightarrow}} 
\ast 
] , \linebreak [0] 
[
\ast 
\Rightarrow 
\ast 
] , \linebreak [0] 
[
\ast 
\Leftrightarrow 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
:
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{spy}
\ast 
] , \linebreak [0] 
[
\ast 
!
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\left\{\protect \begin {array}{l}
\ast 
\\
\ast 
\protect \end {array}\right.
]
; 
\newline \mathbf {Preassociative} \newline 
[
\lambda 
\ast 
.
\ast 
] , \linebreak [0] 
[
\Lambda 
\ast 
. 
\ast 
] , \linebreak [0] 
[
\Lambda 
\ast 
] , \linebreak [0] 
[
{\bf if} \ 
\ast 
\ {\bf then} \ 
\ast 
\ {\bf else} \ 
\ast 
] , \linebreak [0] 
[
\mathbf{let\ } 
\ast 
= 
\ast 
\mathbf{\ in\ } 
\ast 
] , \linebreak [0] 
[
\mathbf{let\ } 
\ast 
\mathrel{\ddot{=}} 
\ast 
\mathrel{\ in\ } 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\#
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
{} ^ { I }
] , \linebreak [0] 
[
\ast 
{} ^ { \rhd }
] , \linebreak [0] 
[
\ast 
{} ^ { V } 
] , \linebreak [0] 
[
\ast 
{} ^ { + } 
] , \linebreak [0] 
[
\ast 
{} ^ { - } 
] , \linebreak [0] 
[
\ast 
{} ^ { \ast } 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\mathop {\char64} 
\ast 
] , \linebreak [0] 
[
\ast 
\rhd 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\ast 
] , \linebreak [0] 
[
\ast 
\gg 
\ast 
] , \linebreak [0] 
[
\ast 
\unrhd 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\vdash 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {i.e.} 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\forall 
\ast 
\colon 
\ast 
] , \linebreak [0] 
[
\Pi 
\ast 
\colon 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel {\oplus} 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
; 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\ proves\ 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\mathbf{\ proof\ of\ } 
\ast 
: 
\ast 
] , \linebreak [0] 
[
Line \, 
\ast 
: 
\ast 
\gg 
\ast 
; 
\ast 
] , \linebreak [0] 
[
Last\ line \, 
\ast 
\gg 
\ast 
\,\Box
] , \linebreak [0] 
[
Line \, 
\ast 
: Premise \gg 
\ast 
;
\ast 
] , \linebreak [0] 
[
Line \, 
\ast 
: \mbox{Side-condition} \gg 
\ast 
; 
\ast 
] , \linebreak [0] 
[
Arbitrary \gg 
\ast 
;
\ast 
] , \linebreak [0] 
[
Local \gg 
\ast 
= 
\ast 
; 
\ast 
] , \linebreak [0] 
[
Begin \, 
\ast 
 ; 
\ast 
 : End ; 
\ast 
] , \linebreak [0] 
[
Last\ block\ line \, 
\ast 
\gg 
\ast 
\,;
] , \linebreak [0] 
[
Arbitrary \gg 
\ast 
;
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel{|} 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel{\mathrm{,}}
\ast 
] , \linebreak [0] 
[
\ast 
{[}
\ast 
{]}
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\& 
\ast 
] , \linebreak [0] 
[
 \rightarrow 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\backslash \backslash 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{linebreak[4]} 
\ast 
] , \linebreak [0] 
[
\ast 
\backslash \backslash 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast  \in 
\ast 
]
; 
]$
\end {flushleft}

\end{appendix}

\end{document}
