\documentclass [fleqn]{article}
\setlength {\overfullrule }{1mm}
\input{lgwinclude}

\usepackage{latexsym}
\usepackage{parskip}

\parindent=0pt               % Ingen indrykkning
\frenchspacing

%\usepackage{verbatim}

%\setlength{\parindent}{0em}
%\setlength{\parskip}{1ex}

% The font of each Logiweb construct is under tight control except that
% strings are typeset in whatever font is in effect at the time of
% typesetting. This is done to enhance the readability of strings in the
% TeX source generated by Logiweb. The default font for typesetting
% strings is \rm:
\everymath{\rm}

\usepackage{makeidx}
\usepackage{page}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}
\newlength{\bracketwidth}
\settowidth{\bracketwidth}{$[{}$}
\newcommand{\back}{\protect\makebox[-1.0\bracketwidth]{}}

\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 130 490 730}}
\hypersetup{pdftitle=Introduction to Logiweb}
\hypersetup{colorlinks=true}
\bibliographystyle{plain}

% \tex{something} writes something to page.otx for later inclusion
\newwrite\outex
\newtoks\toktex
\immediate\openout\outex=page.otx
\newcommand{\tex}[1]{\toktex={\item #1}\immediate\write\outex{\the\toktex}}

% \test{something} writes something to page.tst for later inclusion
\newwrite\outest
\immediate\openout\outest=page.tst
\newcommand{\test}[1]{\toktex={\item #1}\immediate\write\outest{\the\toktex}}

% Concerning \catcode`\@=11 : See the TeXbook, Appendix B (page 344).
% \afterheading suppresses indentation once, c.f. latex.ltx.
% \display{something} displays something as a displayed equation except
% that linebreaking is possible and displaymath is not turned on by default.
% The first paragraph after \display{something} is unindented.
% Glue below formulas may be wrong. The definition of \display misses
% something like \addvspace{\belowdisplayskip}.
\catcode`\@=11
\def\afterheading{\@afterheading}
\catcode`\@=12
\newcommand{\display}[1]{\begin{list}{}{\setlength{\leftmargin}{\mathindent}}
\item #1\end{list}

\afterheading}
\newcommand{\statement}[1]{\begin{list}{}{\setlength{\leftmargin}{0mm}}
\item #1\end{list}

\afterheading}

\begin {document}
\title {Logic - Peano Arithmetic\\
$\quad$\\
{\large
$
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}$
}
}
\author {Kasper Frederiksen}
\maketitle
\tableofcontents

\raggedright

\clearpage

\section{Introduction} 

This report proves proposition $L3.2(h)'$ in \cite{mendelson}, page 156. That is:

\display{$
[L3.2(h)'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
]$}

The successful proof of this lemma can be seen in section
\ref{res.lemma}.

This entire text has been verified as mathematically correct by the
LogiWeb system. The source code kan be obtained from the online
version of this text:
\begin{center}
 \verb|http://...|
\end{center}

\subsection{About LogiWeb} 

The LogiWeb system is being developed by Klaus Grue (DIKU) and is
fully defined on the LogiWeb {\bf base page}
\footnote{This report uses the version of base page that has the time stamp {\scriptsize \bf GRD-2005-06-22-UTC-06-58-05-413682}}
written by Klaus Grue:

\begin{center}
\verb|http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/latest/|
\end{center}

From a users point of view LogiWeb consists of two parts, a compiler
and a (web)server. The user will write his text using latex syntax
and whenever he wishes to express mathematics this will be written
amongst the ordinary text, but using \verb|pyk| syntax. When the
source file is complied two things happen. The pyk part of the file is
translated into latex and given to the latex compiler along with the
rest of the text, also the mathematics expressed by the pyk is
checked for correctness. 

The LogiWeb system allows the user to reference mathematical constructs
defined on other pages. The task of managing requests for these pages
falls to the LogiWeb server. The LogiWeb server on DIKU has a
graphical front end in the form of a webserver, that can be accessed
through the links given above.


\subsection{About the proof system} 

All proofs in this text have been completed in the axiomatic
arithmetic system called $
S'$. This
system is a Peano Arithmetic system and is fully defined on the {\bf
peano page} \footnote{This report uses the version of peano page that
has the time stamp {\scriptsize \bf GRD-2005-06-22-UTC-07-23-31-271829
}} written by Klaus Grue: \begin{center}
\verb|http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano/|
\end{center}

It should be noted that the peano page redefines all the arithmetic
and logical operators from base page in special ``peano
versions''. These new operators are identically these classical
counterparts. To avoid any confusion figure (\ref{aaa}) gives an
overview of the new operators.

\begin{figure}[h]
  \centering
\begin{tabular}{|ccc|}
\hline
$ False \Rightarrow True $ & $\to$ & $
\mathsf {F}
\mathrel{\dot{\Rightarrow}} 
\mathsf {T}$ \\
$ \mathrm{ arbitrary variable }: A, B, C,... $ & $\to$ & $\underline{
\mathsf {a}}$, $\underline{
\mathsf {b}}$, $\underline{
\mathsf {c}}$,$\ldots$\\
$ \mathrm{ specific terms }: a, b, c, ...    $ & $\to$ & $
\dot{
\mathsf {a}
}$, $
\dot{
\mathsf {b}
}$, $
\dot{
\mathsf {c}
}$,$\ldots$\\
$ \forall a: a + 0 = a  $ & $\to$ & $
\dot{\forall} 
\dot{
\mathsf {a}
}
\colon 
\dot{
\mathsf {a}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {a}
}$ \\
$ \neg(1 \cdot 0 = 1)  $ & $\to$ & $
\dot{\neg}\, 
\dot{0}
'
\mathop{\dot{\cdot}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
'$\\
\hline
\end{tabular}  
\caption{The new version of the operators}
  \label{aaa}
\end{figure}

Peano arithmetic is only defined on natural numbers, and the successor
operation is written like this: $
\dot{0}
'
\stackrel{p}{=} 
\dot{0}
'$.

This peano page also defines the axioms and rules of the $
S'$ system. These are identical to those defined
in \cite{mendelson}, chapters two and three. Below I repeat the theory
as it is defined on the peano page. Since the pyk syntax is not always
obvious I have included some comments.

System $[
S']$ is defined thus:

\display{$
[
S'
\stackrel{
stmt
}{\rightarrow}
\mathsf{x}
]$}

\display{$
[
A1'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
]
[
A1'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}

\display{$
[
A2'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
]
[
A2'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}

\display{$
[
A3'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\dot{\neg}\, \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} 
\dot{\neg}\, \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} 
\dot{\neg}\, \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
]
[
A3'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}

\display{$
[
A4'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {c}}
\colon 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\lceil \underline{
\mathsf {a}}
\rceil 
{\equiv}\langle 
\lceil \underline{
\mathsf {b}}
\rceil 
|
\lceil \underline{
\mathsf{x}}
\rceil 
:=
\lceil \underline{
\mathsf {c}}
\rceil 
\rangle
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\dot{\forall} \underline{
\mathsf{x}}
\colon \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
]
[
A4'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}
This axiom allows us to remove a universal kvantor and replace the quantified 
variable with a specific term, as long as this does not cause a variable clash.
When using the axiom, you must state which term you wish to substitute into
the place of the quantified variable. The axiom is used line this:
$
A4'
\mathop {\char64} 
\dot{
\mathsf {t}
}$
$\to$ 
$
\dot{\forall} 
\dot{
\mathsf {q}
}
\colon 
\dot{
\mathsf {q}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}$

\display{$
[
A5'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\dot{nonfree}(
\lceil \underline{
\mathsf{x}}
\rceil 
,
\lceil \underline{
\mathsf {a}}
\rceil 
)
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\dot{\forall} \underline{
\mathsf{x}}
\colon \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} \underline{
\mathsf{x}}
\colon \underline{
\mathsf {b}}
]
[
A5'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}
This axiom is not used in this report.

\display{$
[
MP'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
]
[
MP'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}

\display{$
[
Gen'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\vdash 
\dot{\forall} \underline{
\mathsf{x}}
\colon \underline{
\mathsf {a}}
]
[
Gen'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}
This is the generalization rule, that allows us to add a universal kvantor in front
of a proof line. 

\display{$
[
S1'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
\stackrel{p}{=} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\stackrel{p}{=} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\stackrel{p}{=} \underline{
\mathsf {c}}
]
[
S1'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}

\display{$
[
S2'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\stackrel{p}{=} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
'
\stackrel{p}{=} \underline{
\mathsf {b}}
'
]
[
S2'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}

\display{$
[
S3'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
\dot{0}
\stackrel{p}{=} \underline{
\mathsf {a}}
'
]
[
S3'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}

\display{$
[
S4'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
'
\stackrel{p}{=} \underline{
\mathsf {b}}
'
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\stackrel{p}{=} \underline{
\mathsf {b}}
]
[
S4'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}

\display{$
[
S5'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} \underline{
\mathsf {a}}
]
[
S5'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}

\display{$
[
S6'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\mathop{\dot{+}} \underline{
\mathsf {b}}
'
\stackrel{p}{=} \underline{
\mathsf {a}}
\mathop{\dot{+}} \underline{
\mathsf {b}}
'
]
[
S6'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}

\display{$
[
S7'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\mathop{\dot{\cdot}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
]
[
S7'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}

\display{$
[
S8'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\mathop{\dot{\cdot}} \underline{
\mathsf {b}}
'
\stackrel{p}{=} \underline{
\mathsf {a}}
\mathop{\dot{\cdot}} \underline{
\mathsf {b}}
\mathop{\dot{+}} \underline{
\mathsf {a}}
]
[
S8'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}

\display{$
[
S9'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
\forall \underline{
\mathsf{x}}
\colon \underline{
\mathsf {b}}
{\equiv}\langle \underline{
\mathsf {a}}
|\underline{
\mathsf{x}}
:=
\dot{0}
\rangle
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {c}}
{\equiv}\langle \underline{
\mathsf {a}}
|\underline{
\mathsf{x}}
:=\underline{
\mathsf{x}}
'
\rangle
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} \underline{
\mathsf{x}}
\colon \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} \underline{
\mathsf{x}}
\colon \underline{
\mathsf {a}}
]
[
S9'
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}
This is the induction axiom. What it basically says is ``base case'' $\Rightarrow$ ``induction step'' $\Rightarrow$ ``conclusion''.

\section{The Deduction Algorithm}

Mendelson introduces the {\bf Deduction Theorem} for first-order
theories in \cite{mendelson} page 74. The proof is stated in the form
of an algorithm that will turn a proof of the the lemma  
$
S'
\vdash \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {c}}$, 
in to a proof of the lemma 
$
S'
\vdash \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}$.

While it would be possible to implement this automatic proof converter in
pyk, as a part of this text, Klaus has advised that we not attempt
this. We are going to follow this advise. Instead we run the algorithm
by hand and type in the converted proofs.

A god description of the deduction algorithm can be found at:
\begin{center}
\verb|http://www.diku.dk/undervisning/2005s/235/deduction.html|
\end{center}


\section{Supporting Lemmas\label{support}} 

Before we start proving the lemmas in section \ref{main.lemmas}. Let
us first prove a number of lemmas that will help make the following
proofs shorter.

Pleas note that many of the lemmas in this section where included on
a when-needed basis. If, in section \ref{main.lemmas}, you notice a
situation where one of the following lemmas could have been used to
shorten the proof, then that is an ``older'' proof from before the
supporting lemma was included.

\subsection{Corollary $C1.10a$}
The lemma 
$
[C1.10a
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}corollary
\linebreak [0]\ \hskip0em plus2.0em{}one
\linebreak [0]\ \hskip0em plus2.0em{}point
\linebreak [0]\ \hskip0em plus2.0em{}ten
\linebreak [0]\ \hskip0em plus2.0em{}a
\mbox{''}
]$$
[C1.10a
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}C1.10a
\mbox{''}
]$
is taken from \cite{mendelson} page 38.

\display{$
[C1.10a
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
\forall \underline{
\mathsf {d}}
\colon \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\vdash \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
]$}

$
[C1.10a
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
\forall \underline{
\mathsf {d}}
\colon \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\vdash 
A1'
\gg \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
; 
MP'
\rhd \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\rhd \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
; 
A2'
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
; 
MP'
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
; 
MP'
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$


\subsection{Corollary $C1.10(b)$}
The lemma 
$
[C1.10(b)
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}corollary
\linebreak [0]\ \hskip0em plus2.0em{}one
\linebreak [0]\ \hskip0em plus2.0em{}point
\linebreak [0]\ \hskip0em plus2.0em{}ten
\linebreak [0]\ \hskip0em plus2.0em{}b
\mbox{''}
]$$
[C1.10(b)
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}C1.10(b)
\mbox{''}
]$
is taken from \cite{mendelson} page 38.

\display{$
[C1.10(b)
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
\forall \underline{
\mathsf {d}}
\colon \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\vdash \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
]$}

$
[C1.10(b)
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
\forall \underline{
\mathsf {d}}
\colon \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\vdash \underline{
\mathsf {c}}
\vdash 
A1'
\gg \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
; 
MP'
\rhd \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\rhd \underline{
\mathsf {c}}
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
; 
A2'
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
; 
MP'
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
; 
MP'
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {d}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\subsection{Lemma ${A1'}^*$}
The lemma 
$
[{A1'}^*
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}a
\linebreak [0]\ \hskip0em plus2.0em{}one
\linebreak [0]\ \hskip0em plus2.0em{}star
\mbox{''}
]$$
[{A1'}^*
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\{A1
\mbox {'}
\}
{\char94}
{*}
\mbox{''}
]$
is used during the deduction algorithm, when one wishes to add a hypothesis, $\underline{
\mathsf {h}}$, to a
line of a proof. This will shorten the proof by one line.

\display{$
[{A1'}^*
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
]$}

$
[{A1'}^*
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {a}}
\vdash 
A1'
\gg \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
; 
MP'
\rhd \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\rhd \underline{
\mathsf {a}}
\gg \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\subsection{Lemma ${A2'}^*$}
Use of the axiom $
A2'$ is often followed 
by a use of the modus ponens rule. If we instead use lemma 
$
[{A2'}^*
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}a
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}star
\mbox{''}
]$$
[{A2'}^*
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\{A2
\mbox {'}
\}
{\char94}
{*}
\mbox{''}
]$
, then the modus ponens is not necessary.

\display{$
[{A2'}^*
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {h}}
\colon 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
]$}

$
[{A2'}^*
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
\forall \underline{
\mathsf {h}}
\colon 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\vdash 
A2'
\gg \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
; 
MP'
\rhd \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\rhd \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\gg \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\subsection{Lemma $Double Hypothesis$}
The lemma
$
[Double Hypothesis
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}double
\linebreak [0]\ \hskip0em plus2.0em{}hyp
\mbox{''}
]$$
[Double Hypothesis
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}Double
\linebreak [0]\ \hskip0em plus2.0em{}Hypothesis
\mbox{''}
]$
is used during the deduction algorithm, when one wishes to add a hypothesis, $\underline{
\mathsf {h}}$, 
to a proof line of the form $\underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}$. This will shorten the proof
by one line.

\display{$
[Double Hypothesis
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
]$}

$
[Double Hypothesis
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {h}}
\colon \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\vdash {A1'}^*
\rhd \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\gg \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
; {A2'}^*
\rhd \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\gg \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {h}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\subsection{Lemma $L1.8$}
Lemma 
$
[L1.8
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}one
\linebreak [0]\ \hskip0em plus2.0em{}point
\linebreak [0]\ \hskip0em plus2.0em{}eight
\mbox{''}
]$$
[L1.8
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}L1.8
\mbox{''}
]$
from \cite{mendelson} page 36, is used to introduce the premise at the start of the deduction 
algorithm.

\display{
$
[L1.8
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
]$}

$
[L1.8
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
\forall \underline{
\mathsf {b}}
\colon 
A2'
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
; 
A1'
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
; 
MP'
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
; 
A1'
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
; 
MP'
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\subsection{Lemma $Tautology 1$}
The lemma that i call 
$
[Tautology 1
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}tautology
\linebreak [0]\ \hskip0em plus2.0em{}one
\mbox{''}
]$$
[Tautology 1
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}Tautology
\linebreak [0]\ \hskip0em plus2.0em{}1
\mbox{''}
]$
is an all-round useful lemma.

\display{$
[Tautology 1
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
]$}

$
[Tautology 1
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\vdash 
A2'
\gg \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
; 
MP'
\rhd \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\rhd \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\gg \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
; 
A1'
\gg \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
; 
MP'
\rhd \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\rhd \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
; 
A2'
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
; 
MP'
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
; 
A1'
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
; 
MP'
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\rhd \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {b}}
\gg \underline{
\mathsf {b}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {a}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {c}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\section{The Main Proofs \label{main.lemmas}}

The object of this report is the proof of $L3.2(h)'$ in section \ref{res.lemma}. In order to get that far
we must first prove a number of the lemmas that precede it in
\cite{mendelson}. Of these lemma $
L3.2(a)'$ has been proved by Klaus on the peano page and lemma L3.2(e)'
is not needed. Taking into account the support lemmas proved in
section \ref{support}, this leaves parts (b), (c), (d), (f), (g) and
of corse (h), still to be proven.

Of these lemmas (f), (g) and (h) are proved using induction, and that
means we will need the Deduction Algorithm.

All of these lemmas are proved in \cite{mendelson}, so the task of
this report has been to rewrite Mendelson's proofs in explicit form
and use the deduction algorithm where necessary.


\subsection{Lemma $L3.2(b)'$}

$
[L3.2(b)'
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}l
\linebreak [0]\ \hskip0em plus2.0em{}three
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}b
\mbox{''}
]$$
[L3.2(b)'
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}L3.2(b)
\mbox {'}
\mbox{''}
]$

\display{$
[L3.2(b)'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {t}}
\colon 
\forall \underline{
\mathsf {r}}
\colon \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {r}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
]$}

$
[L3.2(b)'
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
\forall \underline{
\mathsf {t}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
S1'
\gg \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {r}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
; 
L3.2(a)'
\gg \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {t}}
; C1.10(b)
\rhd \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {r}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\rhd \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\gg \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {r}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\subsection{Lemma $L3.2(c)'$}

$
[L3.2(c)'
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}l
\linebreak [0]\ \hskip0em plus2.0em{}three
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}c
\mbox{''}
]$$
[L3.2(c)'
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}L3.2(c)
\mbox {'}
\mbox{''}
]$

\display{$
[L3.2(c)'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {t}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {s}}
\colon \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {r}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {s}}
]$}


$
[L3.2(c)'
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
\forall \underline{
\mathsf {t}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {s}}
\colon 
S1'
\gg \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {s}}
; L3.2(b)'
\gg \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {r}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
; C1.10a
\rhd \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {r}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\rhd \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\gg \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {r}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\subsection{Lemma $L3.2(d)'$}

$
[L3.2(d)'
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}l
\linebreak [0]\ \hskip0em plus2.0em{}three
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}d
\mbox{''}
]$$
[L3.2(d)'
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}L3.2(d)
\mbox {'}
\mbox{''}
]$

\display{$
[L3.2(d)'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\forall \underline{
\mathsf {t}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {s}}
\colon \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {s}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {s}}
]$}

$
[L3.2(d)'
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
\forall \underline{
\mathsf {t}}
\colon 
\forall \underline{
\mathsf {r}}
\colon 
\forall \underline{
\mathsf {s}}
\colon L3.2(c)'
\gg \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {s}}
; Tautology 1
\rhd \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\gg \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {s}}
; L3.2(b)'
\gg \underline{
\mathsf {s}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {s}}
; C1.10a
\rhd \underline{
\mathsf {s}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\rhd \underline{
\mathsf {t}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\gg \underline{
\mathsf {s}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {s}}
; Tautology 1
\rhd \underline{
\mathsf {s}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\gg \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {s}}
\stackrel{p}{=} \underline{
\mathsf {t}}
\mathrel{\dot{\Rightarrow}} \underline{
\mathsf {r}}
\stackrel{p}{=} \underline{
\mathsf {s}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$


\subsection{Lemma $L3.2(f)'$}
To prove 
$
[L3.2(f)'
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}l
\linebreak [0]\ \hskip0em plus2.0em{}three
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}f
\mbox{''}
]$$
[L3.2(f)'
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}L3.2(f)
\mbox {'}
\mbox{''}
]$
using induction, we will need to prove the base case
$
[{L3.2(f)'}_{BASE}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}l
\linebreak [0]\ \hskip0em plus2.0em{}three
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}f
\linebreak [0]\ \hskip0em plus2.0em{}base
\mbox{''}
]$$
[{L3.2(f)'}_{BASE}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\{L3.2(f)
\mbox {'}
\}
\_
\{BASE
\}
\mbox{''}
]$ (section \ref{f.base})
and the induction step
$
[{L3.2(f)'}_{HYP}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}l
\linebreak [0]\ \hskip0em plus2.0em{}three
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}f
\linebreak [0]\ \hskip0em plus2.0em{}hyp
\mbox{''}
]$$
[{L3.2(f)'}_{HYP}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\{L3.2(f)
\mbox {'}
\}
\_
\{HYP
\}
\mbox{''}
]$ (section \ref{f.hyp}).

\display{$
[L3.2(f)'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
]$}

$
[L3.2(f)'
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash {L3.2(f)'}_{BASE}
\gg 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{0}
; {L3.2(f)'}_{HYP}
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
S9'
\gg 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{0}
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
MP'
\rhd 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{0}
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\rhd 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{0}
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
MP'
\rhd 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\rhd 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\subsubsection{The base case of $L3.2(f)'$\label{f.base}}

\display{$
[{L3.2(f)'}_{BASE}
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{0}
]$}


$
[{L3.2(f)'}_{BASE}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
S5'
\gg 
\dot{0}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
; L3.2(b)'
\gg 
\dot{0}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{0}
; 
MP'
\rhd 
\dot{0}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{0}
\rhd 
\dot{0}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\gg 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{0}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\subsubsection{The induction step of $L3.2(f)'$\label{f.hyp}}

\display{$
[{L3.2(f)'}_{HYP}
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
]$}

$
[{L3.2(f)'}_{HYP}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash L1.8
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
S6'
\gg 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
A1'
\gg 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
MP'
\rhd 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\rhd 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
S2'
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
A1'
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; {A2'}^*
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; L3.2(d)'
\gg 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
Hypothesize
\rhd 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; {A2'}^*
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; {A2'}^*
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
Gen'
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$


\subsection{Lemma $L3.2(g)'$}
To prove 
$
[L3.2(g)'
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}l
\linebreak [0]\ \hskip0em plus2.0em{}three
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}g
\mbox{''}
]$$
[L3.2(g)'
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}L3.2(g)
\mbox {'}
\mbox{''}
]$
using induction, we will need to prove the base case
$
[{L3.2(g)'}_{BASE}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}l
\linebreak [0]\ \hskip0em plus2.0em{}three
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}g
\mbox{''}
]$$
[{L3.2(g)'}_{BASE}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\{L3.2(g)
\mbox {'}
\}
\_
\{BASE
\}
\mbox{''}
]$(section \ref{g.base})
and the induction step
$
[{L3.2(g)'}_{HYP}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}l
\linebreak [0]\ \hskip0em plus2.0em{}three
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}g
\linebreak [0]\ \hskip0em plus2.0em{}hyp
\mbox{''}
]$$
[{L3.2(g)'}_{HYP}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\{L3.2(g)
\mbox {'}
\}
\_
\{HYP
\}
\mbox{''}
]$(section \ref{g.hyp}).

\display{$
[L3.2(g)'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
]$}

$
[L3.2(g)'
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash {L3.2(g)'}_{BASE}
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
; {L3.2(g)'}_{HYP}
\gg 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; 
S9'
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
MP'
\rhd 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\rhd 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\gg 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
MP'
\rhd 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\rhd 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
Gen'
\rhd 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$


\subsubsection{Base case of $L3.2(g)'$\label{g.base}}

\display{$
[{L3.2(g)'}_{BASE}
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
]$}

$
[{L3.2(g)'}_{BASE}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
S5'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
; 
S5'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
; 
S2'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
; L3.2(d)'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
; 
Gen'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\subsubsection{Induction step of $L3.2(g)'$\label{g.hyp}}

\display{$
[{L3.2(g)'}_{HYP}
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
]$}

$
[{L3.2(g)'}_{HYP}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash L1.8
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
S6'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; {A1'}^*
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
S2'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; {A1'}^*
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; {A2'}^*
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; L3.2(c)'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; {A1'}^*
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; {A2'}^*
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; {A2'}^*
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; 
S6'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; {A1'}^*
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
S2'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; {A1'}^*
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; {A2'}^*
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; L3.2(d)'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; {A1'}^*
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; {A2'}^*
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; {A2'}^*
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
; 
Gen'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\gg 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$


\subsection{Lemma $L3.2(h)'$\label{res.lemma}}
To prove
$
[L3.2(h)'
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}l
\linebreak [0]\ \hskip0em plus2.0em{}three
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}h
\mbox{''}
]$$
[L3.2(h)'
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}L3.2(h)
\mbox {'}
\mbox{''}
]$
using induction, we will need to prove the base case
$
[{L3.2(h)'}_{BASE}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}l
\linebreak [0]\ \hskip0em plus2.0em{}three
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}h
\linebreak [0]\ \hskip0em plus2.0em{}base
\mbox{''}
]$$
[{L3.2(h)'}_{BASE}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\{L3.2(h)
\mbox {'}
\}
\_
\{BASE
\}
\mbox{''}
]$(section \ref{h.base})
and the induction step
$
[{L3.2(h)'}_{HYP}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}l
\linebreak [0]\ \hskip0em plus2.0em{}three
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}h
\linebreak [0]\ \hskip0em plus2.0em{}hyp
\mbox{''}
]$$
[{L3.2(h)'}_{HYP}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\{L3.2(h)
\mbox {'}
\}
\_
\{HYP
\}
\mbox{''}
]$(section \ref{h.hyp}).

\display{$
[L3.2(h)'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
]$}

$
[L3.2(h)'
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash {L3.2(h)'}_{BASE}
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; {L3.2(h)'}_{HYP}
\gg 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
S9'
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
MP'
\rhd 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\rhd 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\gg 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
MP'
\rhd 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\rhd 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\gg 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
Gen'
\rhd 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\subsubsection{Base case of $L3.2(h)'$\label{h.base}}

\display{$
[{L3.2(h)'}_{BASE}
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
]$}

$
[{L3.2(h)'}_{BASE}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
S5'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
; L3.2(f)'
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
A4'
\mathop {\char64} 
\dot{
\mathsf {t}
}
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
MP'
\rhd 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\rhd 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; L3.2(c)'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\gg 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\rhd 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
Gen'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{0}
\stackrel{p}{=} 
\dot{0}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\subsubsection{Induction step of $L3.2(h)'$\label{h.hyp}}

For proving the induction step, we will need the lemma
$
[L3.2h_{SWAP}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lemma
\linebreak [0]\ \hskip0em plus2.0em{}prime
\linebreak [0]\ \hskip0em plus2.0em{}l
\linebreak [0]\ \hskip0em plus2.0em{}three
\linebreak [0]\ \hskip0em plus2.0em{}two
\linebreak [0]\ \hskip0em plus2.0em{}h
\linebreak [0]\ \hskip0em plus2.0em{}hyp
\mbox{''}
]$$
[L3.2h_{SWAP}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}L3.2h
\_
\{SWAP
\}
\mbox{''}
]$.

\display{$
[L3.2h_{SWAP}
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\vdash 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
]$}
$
[L3.2h_{SWAP}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\vdash 
Gen'
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
A4'
\mathop {\char64} 
\dot{
\mathsf {q}
}
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
MP'
\rhd 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\rhd 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
Gen'
\rhd 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
A4'
\mathop {\char64} 
\dot{
\mathsf {t}
}
\gg 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
MP'
\rhd 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\rhd 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
Gen'
\rhd 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{\forall} 
\dot{
\mathsf {q}
}
\colon 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
A4'
\mathop {\char64} 
\dot{
\mathsf {r}
}
\gg 
\dot{\forall} 
\dot{
\mathsf {q}
}
\colon 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
MP'
\rhd 
\dot{\forall} 
\dot{
\mathsf {q}
}
\colon 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\rhd 
\dot{\forall} 
\dot{
\mathsf {q}
}
\colon 
\dot{
\mathsf {q}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {q}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$\\
$\quad$\\
Now we are ready to prove the induction step.
$\quad$\\

\display{$
[{L3.2(h)'}_{HYP}
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
]$}

$
[{L3.2(h)'}_{HYP}
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S'
\vdash L1.8
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
S6'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; {A1'}^*
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
S2'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; Double Hypothesis
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; L3.2(c)'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; Double Hypothesis
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; {A2'}^*
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; L3.2(d)'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; Double Hypothesis
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; L3.2(g)'
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
A4'
\mathop {\char64} 
\dot{
\mathsf {t}
}
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
A4'
\mathop {\char64} 
\dot{
\mathsf {t}
}
\gg 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
MP'
\rhd 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\rhd 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
A4'
\mathop {\char64} 
\dot{
\mathsf {r}
}
\gg 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; 
MP'
\rhd 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\rhd 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
; L3.2h_{SWAP}
\rhd 
\dot{
\mathsf {t}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\gg 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; {A1'}^*
\rhd 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
; {A2'}^*
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
MP'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
'
\gg 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
; 
Gen'
\rhd 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\gg 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\mathrel{\dot{\Rightarrow}} 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
'
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
'
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\section{Conclusion}
We have now successfully proved the lemma:
\begin{center}
$
[L3.2(h)'
\stackrel{
stmt
}{\rightarrow}
S'
\vdash 
\dot{\forall} 
\dot{
\mathsf {t}
}
\colon 
\dot{\forall} 
\dot{
\mathsf {r}
}
\colon 
\dot{
\mathsf {t}
}
\mathop{\dot{+}} 
\dot{
\mathsf {r}
}
\stackrel{p}{=} 
\dot{
\mathsf {r}
}
\mathop{\dot{+}} 
\dot{
\mathsf {t}
}
]$
\end{center}

In retrospect some of the proofs could have been made shorter/simpler,
but this does not alter the fact that the LogiWeb system has verified that 
this text is correct.

\clearpage

\appendix

\section{The name of the page}

This defines the name of the page:

\display{$
[
\mbox{logik rapport}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}logik
\linebreak [0]\ \hskip0em plus2.0em{}rapport
\mbox{''}
]$}

\section{The Bibliography}
\begin{thebibliography}{99}
\bibitem[Mendelson, 2001]{mendelson} E. Mendelson,\\
  Introduction to Mathematical Logic, fourth edition.\\
  Chapman and Hall 2001.
\end{thebibliography}

\end{document}
