\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 newcommers to Logiweb\texttrademark and also because core Logiweb\texttrademark
is very low level. Being newcommers 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 total 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 oportunity
to sit down with Klaus in a kind of assisted programming session, where Klaus helped us with our problems as they occured - 
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 page is to use
Logiweb\texttrademark \emph{to publish a machine checkable proof for a theorem of our choise} - which we have done. 
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), \emph{define and prove lemmas in a theory} (both using axioms
aswell as allready 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 wich we prove. Finally we use these
higher level rules to prove the sequent: TODO.

\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 the sequent: TODO.

\section{First order predicate calculus}\label{sec:predcalc}
Based on mathworld\footnote{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 excately like those found on Mathworld for two reasons. 
First we have made $\Rightarrow$ right associative in order to get rid of unnecessary parenthisis. 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{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 \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\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}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \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}}
\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}}
\Rightarrow \underline{
\mathsf {g}} \vee \underline{
\mathsf {f}}
\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 \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 {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}} \wedge \underline{
\mathsf {g}}
\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 {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 {g}}
\Rightarrow \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\Rightarrow \forall \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{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)
]$ 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{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 \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\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}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \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}}
\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}}
\Rightarrow \underline{
\mathsf {g}} \vee \underline{
\mathsf {f}}
\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 \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 {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}} \wedge \underline{
\mathsf {g}}
\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 {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 {g}}
\Rightarrow \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\Rightarrow \forall \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{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)
]$ 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 acording to mathworld but it is a conservative extension
in the sence 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{Notation}
Some of the notation used above is most likely unfamilliar. 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 $\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 sence 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 fullfilled.

\item{\textbf{The side-condition $\left< A  \equiv B \mid C := D \right>$}} is fulfilled, if the proposition $A$ where any occurrence of the meta-variable $C$ is replaced
by the proposition $D$ is exactly equal to the proposition $B$. Another way to express this using a more common notation of substitution would be $B \equiv A[D/C]$.

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

\end{itemize}

\subsection{Some small proofs}
Having explained the syntax of definitons and proofs we continue with two simple, but usefull, 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} aswell.

\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}
$
[
\mbox{trivia2}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {f}}
]$
\end{Lem}

$
[
\mbox{trivia2}
\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 \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 \underline{
\mathsf {f}}
\gg \underline{
\mathsf {f}}
\vdash \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{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 \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\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}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \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}}
\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}}
\Rightarrow \underline{
\mathsf {g}} \vee \underline{
\mathsf {f}}
\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 \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 {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}} \wedge \underline{
\mathsf {g}}
\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 {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 {g}}
\Rightarrow \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\Rightarrow \forall \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{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)
]$ 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{pcded}
\rhd \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {h}}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {h}}
; 
\mbox{pcded}
\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{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{pcded}
\rhd \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\gg \underline{
\mathsf {f}}
\Rightarrow \underline{
\mathsf {g}}
; 
\mbox{pcded}
\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)
]$

$
[
\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.
\end{Rem}

\end{Lem}
\begin{Lem}
$
[
\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}
$
[
\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{pcded}
\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 theorems above to prove some other fairly standard rules.

\begin{Lem}
$
[
\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}
$
[
\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}
)
]$

\subsection{Law of the Excluded Middle}
In this section we prove the \emph{Law of the Excluded Middle}. 

\begin{The}\label{the:lem}
$
[
\mbox{lem}
\stackrel{
stmt
}{\rightarrow}
\mbox{pred calc}
\vdash 
\forall \underline{
\mathsf {f}}
\colon \underline{
\mathsf {f}} \vee \neg \underline{
\mathsf {f}}
]$
\end{The}

$
[
\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{hugh} 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{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 \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\vdash \underline{
\mathsf {f}}
\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}}
\Rightarrow \neg \underline{
\mathsf {g}}
\Rightarrow \neg \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}}
\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}}
\Rightarrow \underline{
\mathsf {g}} \vee \underline{
\mathsf {f}}
\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 \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 {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}} \wedge \underline{
\mathsf {g}}
\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 {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 {g}}
\Rightarrow \underline{
\mathsf {f}}
\vdash \underline{
\mathsf {g}}
\Rightarrow \forall \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{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)
]$, 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 sytem without the rule notintro but with rules notelim and botelim added.
Let $F$ be fixed and define $\bot\equiv F \land \lnot F$\footnotemark. The the following holds:
\begin{enumerate}
\item If $B$ can be proved in Nat' then B can be proved in Nat.
\item If $B$ can be proved in Nat then $B[\bot/F\land\lnot F]$ can be proved in Nat'.
\end{enumerate}
\end{The}
\footnotetext{$F$ must be fixed for all occurrences of bottom e.g. $\bot \land \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 is 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. Therefore we skil all of the lemmas the two systems have in common.
\\
\\
\textbf{Proof of 1:}\\
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 on the proof of $F \land \lnot F$, which means that we can also construct proofs of $F$ and $\lnot F$ using the andelim1 and andelim2 rules. Finally we can prove $F$ and $\lnot F$ under the assumption of $\lnot A$.
Now we can construct the proof of $A$ like this.
$$
\frac
{\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 \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}
We saw that $\bot$ could be replaced with $A \land \lnot A$ above and that the proof rule botelim allows us to conclude anything once we have $\bot$. This gives rise to the
following very usefull lemma.

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

TO HERE OK.

Finally we note that in first order predicate calculus metavariables used in functions $F$ and predicates $P$ are \emph{object metavariables}.
\subsection{Deduction lemma}

\begin{Lem}
$
[
\mbox{pcded}
\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}}
]
[
\mbox{pcded}
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$
\end{Lem}

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

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

\section{A nontrivial sequent}\label{sec:higherproof}
\begin{Lem}
$
[
\mbox{nontriv0}
\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{nontriv0}
\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{nontriv1}
\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{nontriv1}
\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{nontriv2}
\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{nontriv2}
\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{nontriv1}
\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{nontriv3}
\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{nontriv3}
\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{nontriv2}
\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{nontriv4}
\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{nontriv4}
\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}}
\vdash 
\mbox{nontriv0}
\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}}
\vdash \underline{
\mathsf {p}}
\gg \underline{
\mathsf {q}}
\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{nontriv3}
\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{orelim}
\rhd \underline{
\mathsf {q}}
\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{appendix}
\section{Pyk definitions}

\begin{flushleft}
$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}aa
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}ab
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}ac
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}ad
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}ae
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}af
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}ag
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}ah
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}ai
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}aj
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}ak
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}al
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}am
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}an
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}ao
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}ap
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}aq
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}ar
\mbox{''}
]
\linebreak[4] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}ell
\linebreak [0]\ \hskip0em plus2.0em{}as
\mbox{''}
]
\linebreak[4] 
[
\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{pcded}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pcded
\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{trivia2}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}trivia2
\mbox{''}
]
\linebreak[4] 
[
\mbox{iatest}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}iatest
\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{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{repeat}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}repeat
\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{nontriv0}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}nontriv0
\mbox{''}
]
\linebreak[4] 
[
\mbox{nontriv1}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}nontriv1
\mbox{''}
]
\linebreak[4] 
[
\mbox{nontriv2}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}nontriv2
\mbox{''}
]
\linebreak[4] 
[
\mbox{nontriv3}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}nontriv3
\mbox{''}
]
\linebreak[4] 
[
\mbox{nontriv4}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}nontriv4
\mbox{''}
]
\linebreak[4] 
[
\mbox{nontriv5}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}nontriv5
\mbox{''}
]
\linebreak[4] 
[
\mbox{nontriv6}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}nontriv6
\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{problemtwo}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}problemtwo
\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{Extra proof line numbers}
$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

$
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwprooflinep
\mbox {$\backslash $}endcsname
\linebreak [0]\ \hskip0em plus2.0em{}L
\_o
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}else
\newline 
\mbox {$\backslash $}if
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}relax
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}csname
\linebreak [0]\ \hskip0em plus2.0em{}lgwello
\mbox {$\backslash $}endcsname
\newline 
\mbox {$\backslash $}global
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}advance
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}by
\linebreak [0]\ \hskip0em plus2.0em{}1
\newline 
\mbox {$\backslash $}xdef
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\{L
\mbox {$\backslash $}ifnum
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
{<}10
\linebreak [0]\ \hskip0em plus2.0em{}0
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}number
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwproofline
\linebreak [0]\ \hskip0em plus2.0em{}
\}
\newline 
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}lgwello
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}fi
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox{''}
]$

\section{Priority table}

\begin {flushleft}$
[
\mbox{problemtwo}
\stackrel{
\mathrm{prio}
}{\rightarrow}
\newline \mathbf {Preassociative} \newline 
[
\mbox{problemtwo}
] , \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] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \linebreak [0] 
[
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi 
] , \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{pcded}
] , \linebreak [0] 
[
\mbox{pcia}
] , \linebreak [0] 
[
\mbox{pcie}
] , \linebreak [0] 
[
\mbox{pcdeduction}
] , \linebreak [0] 
[
\mbox{trivia}
] , \linebreak [0] 
[
\mbox{trivia2}
] , \linebreak [0] 
[
\mbox{iatest}
] , \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{notnotintro}
] , \linebreak [0] 
[
\mbox{notnotelim}
] , \linebreak [0] 
[
\mbox{mt}
] , \linebreak [0] 
[
\mbox{pbc}
] , \linebreak [0] 
[
\mbox{repeat}
] , \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{nontriv0}
] , \linebreak [0] 
[
\mbox{nontriv1}
] , \linebreak [0] 
[
\mbox{nontriv2}
] , \linebreak [0] 
[
\mbox{nontriv3}
] , \linebreak [0] 
[
\mbox{nontriv4}
] , \linebreak [0] 
[
\mbox{nontriv5}
] , \linebreak [0] 
[
\mbox{nontriv6}
]
; 
\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}

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

\end{appendix}

\end{document}
