{   Logiweb, a system for electronic distribution of mathematics
    Copyright (C) 2004 Klaus Grue

    This program is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program; if not, write to the Free Software
    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  021111307  USA

    Contact: Klaus Grue, DIKU, Universitetsparken 1, DK2100 Copenhagen,
    Denmark, grue@diku.dk, http://yoa.dk/, http://www.diku.dk/~grue/

    Logiweb is a system for distribution of mathematical definitions,
    lemmas, and proofs. For more on Logiweb, consult http://yoa.dk/.
}

PAGE logik rapport

BIBLIOGRAPHY

base:  "http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/GRD-2005-06-22-UTC-06-58-05-413682/vector/page.lgw",

peano: "http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano/GRD-2005-06-22-UTC-07-23-31-271829/vector/page.lgw"


PREASSOCIATIVE  base: bracket * end bracket,
test lemma,
test lemma two,
lemma prime a two star,
lemma prime a one star,
lemma double hyp,
corollary one point ten a,
corollary one point ten b,
lemma one point eight,
lemma prime l three two b,
lemma prime l three two c,
lemma prime l three two d,
lemma prime l three two f,
lemma prime l three two f base,
lemma prime l three two f hyp,
lemma prime l three two g,
lemma prime l three two g base,
lemma prime l three two g hyp,
lemma prime l three two h,
lemma prime l three two h base,
lemma prime l three two h hyp,
lemma prime l three two h swap,
tautology one
PREASSOCIATIVE peano: system s
PREASSOCIATIVE  base: * sub * end sub
PREASSOCIATIVE  base: unicode start of text * end unicode text
PREASSOCIATIVE  base: * bit nil
PREASSOCIATIVE  base: * apply *
PREASSOCIATIVE  base: * raw head
PREASSOCIATIVE peano: * peano succ
PREASSOCIATIVE  base: * times *
PREASSOCIATIVE peano: * peano times *
PREASSOCIATIVE  base: * plus *
PREASSOCIATIVE peano: * peano plus *
PREASSOCIATIVE  base: * term plus * end plus
POSTASSOCIATIVE base: * raw pair *
POSTASSOCIATIVE base: * comma *
PREASSOCIATIVE  base: * boolean equal *
PREASSOCIATIVE peano: * peano is *
PREASSOCIATIVE  base: not *
PREASSOCIATIVE peano: peano not *
PREASSOCIATIVE  base: * and *
PREASSOCIATIVE  base: * or *
PREASSOCIATIVE peano: peano all * indeed *
POSTASSOCIATIVE base: * macro imply *
PREASSOCIATIVE peano: * peano imply *
POSTASSOCIATIVE base: * guard *
PREASSOCIATIVE  base: * select * else * end select
PREASSOCIATIVE  base: lambda * dot *
PREASSOCIATIVE  base: * init
PREASSOCIATIVE  base: * at *
POSTASSOCIATIVE base: * infer *
PREASSOCIATIVE  base: all * indeed *
POSTASSOCIATIVE base: * rule plus *
POSTASSOCIATIVE base: * cut *
PREASSOCIATIVE  base: * proves *
PREASSOCIATIVE  base: locally define * as * end line *
POSTASSOCIATIVE base: * then *
PREASSOCIATIVE  base: * tab *
PREASSOCIATIVE  base: * row *

BODY

"File page.tex
\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
"[ math
  peano all peano t indeed peano all peano r indeed
  parenthesis
    peano t peano plus peano r peano is peano r peano plus peano t
  end parenthesis
end math ]"
}
}
\author {Kasper Frederiksen, tofu@diku.dk}
\maketitle
\tableofcontents
"[ ragged right expansion ]"

\clearpage

\section{Introduction} 

This report proves proposition "[ math lemma prime l three two h end
math ]" in \cite{mendelson}, page 156. That is:

\display{"[ math
in theory system prime s
  lemma
    lemma prime l three two h
  says
    peano all peano t indeed peano all peano r indeed
    parenthesis
      peano t peano plus peano r peano is peano r peano plus peano t
    end parenthesis
  end lemma
end math
]"}

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

The entire text has been verified as mathematically correct by the
LogiWeb system. The source code can be obtained from the online
version of this text:
\begin{center}
 \verb|http://www.diku.dk/hjemmesider/studerende/tofu/Logik/|
\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 compiled 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 "[ math system prime s end math]". 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 identical to their 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$ & "[ math false peano imply true end math ]" \\
$ \mathrm{ arbitrary variable }: A, B, C,... $ & $\to$ & "[ math meta a end math ]", "[ math meta b end math ]", "[ math meta c end math ]",$\ldots$\\
$ \mathrm{ specific terms }: a, b, c, ...    $ & $\to$ & "[ math peano a end math ]", "[ math peano b end math ]", "[ math peano c end math ]",$\ldots$\\
$ \forall a: a + 0 = a  $ & $\to$ & "[ math peano all peano a indeed parenthesis peano a peano plus peano zero peano is peano a end parenthesis end math ]" \\
$ \neg(1 \cdot 0 = 1)  $ & $\to$ & "[ math peano not parenthesis peano one peano times peano zero peano is peano one end parenthesis end math]"\\
\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: "[ math peano zero peano succ peano is peano one end math ]".

This peano page also defines the axioms and rules of the "[ math
system prime s end math]" 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 "[ bracket system prime s end bracket ]" is defined thus:

\display{"[ math theory system prime s end theory end math ]"}

\display{"[ math in theory system prime s rule axiom prime a one says all meta a indeed all meta b indeed meta a peano imply meta b peano imply meta a end rule end math ]"}

\display{"[ math in theory system prime s rule axiom prime a two says all meta a indeed all meta b indeed all meta c indeed parenthesis meta a peano imply meta b peano imply meta c end parenthesis peano imply parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply meta c end rule end math ]"}

\display{"[ math in theory system prime s rule axiom prime a three says all meta a indeed all meta b indeed parenthesis peano not meta b peano imply peano not meta a end parenthesis peano imply parenthesis peano not meta b peano imply meta a end parenthesis peano imply meta b end rule end math ]"}

\display{"[ math in theory system prime s rule axiom prime a four says all meta c indeed all meta a indeed all meta x indeed all meta b indeed peano sub quote meta a end quote is quote meta b end quote where quote meta x end quote is quote meta c end quote end sub endorse peano all meta x indeed meta b peano imply meta a end rule end math ]"}
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 like this:\\
"[ math axiom prime a four at peano t end math ]"
$\to$ 
"[ math peano all peano q indeed peano q peano is peano q peano imply peano t peano is peano t end math ]"

\display{"[ math in theory system prime s rule axiom prime a five says all meta x indeed all meta a indeed all meta b indeed peano nonfree quote meta x end quote in quote meta a end quote end nonfree endorse peano all meta x indeed parenthesis meta a peano imply meta b end parenthesis peano imply meta a peano imply peano all meta x indeed meta b end rule end math ]"}
This axiom is not used in this report.

\display{"[ math in theory system prime s rule rule prime mp says all meta a indeed all meta b indeed meta a peano imply meta b infer meta a infer meta b end rule end math ]"}

\display{"[ math in theory system prime s rule rule prime gen says all meta x indeed all meta a indeed meta a infer peano all meta x indeed meta a end rule end math ]"}
This is the generalization rule, that allows us to add a universal kvantor in front
of a proof line. 

\display{"[ math in theory system prime s rule axiom prime s one says all meta a indeed all meta b indeed all meta c indeed meta a peano is meta b peano imply meta a peano is meta c peano imply meta b peano is meta c end rule end math ]"}

\display{"[ math in theory system prime s rule axiom prime s two says all meta a indeed all meta b indeed meta a peano is meta b peano imply meta a peano succ peano is meta b peano succ end rule end math ]"}

\display{"[ math in theory system prime s rule axiom prime s three says all meta a indeed not peano zero peano is meta a peano succ end rule end math ]"}

\display{"[ math in theory system prime s rule axiom prime s four says all meta a indeed all meta b indeed meta a peano succ peano is meta b peano succ peano imply meta a peano is meta b end rule end math ]"}

\display{"[ math in theory system prime s rule axiom prime s five says all meta a indeed meta a peano plus peano zero peano is meta a end rule end math ]"}

\display{"[ math in theory system prime s rule axiom prime s six says all meta a indeed all meta b indeed meta a peano plus meta b peano succ peano is parenthesis meta a peano plus meta b end parenthesis peano succ end rule end math ]"}

\display{"[ math in theory system prime s rule axiom prime s seven says all meta a indeed meta a peano times peano zero peano is peano zero end rule end math ]"}

\display{"[ math in theory system prime s rule axiom prime s eight says all meta a indeed all meta b indeed meta a peano times parenthesis meta b peano succ end parenthesis peano is parenthesis meta a peano times meta b end parenthesis peano plus meta a end rule end math ]"}

\display{"[ math in theory system prime s rule axiom prime s nine says all meta a indeed all meta b indeed all meta c indeed all meta x indeed macro newline peano sub meta b is meta a where meta x is peano zero end sub endorse peano sub meta c is meta a where meta x is meta x peano succ end sub endorse macro newline meta b peano imply peano all meta x indeed parenthesis meta a peano imply meta c end parenthesis peano imply peano all meta x indeed meta a end rule end math ]"}
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  
"[ math system prime s infer parenthesis meta b infer meta c end parenthesis end math ]", 
in to a proof of the lemma 
"[ math system prime s infer meta b peano imply meta c end math ]".

While it would be possible to implement this automatic proof converter in
pyk, as a part of this text, Klaus has advised that we do 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 were 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 "[ math corollary one point ten a end math ]"}
The lemma 
"[ intro corollary one point ten a
   index "C1.10a"
   pyk   "corollary one point ten a"
   tex   "C1.10a"
   end intro ]"
is taken from \cite{mendelson} page 38.

\display{"[ math
  in theory system prime s
   lemma
     corollary one point ten a
   says
     all meta b indeed all meta c indeed all meta d indeed
     parenthesis
     meta b peano imply meta c 
       infer
     meta c peano imply meta d
       infer
     meta b peano imply meta d
     end parenthesis
   end lemma
  end math
]"}

"[ 
  math system prime s
   proof of
     corollary one point ten a
   reads
     arbitrary meta b end line
     arbitrary meta c end line
     arbitrary meta d end line
     line ell a premise 
       meta b peano imply meta c
     end line
     line ell b premise
       meta c peano imply meta d
     end line
     line ell c because axiom prime a one indeed
       parenthesis meta c peano imply meta d end parenthesis
       peano imply
       parenthesis
         meta b peano imply parenthesis meta c peano imply meta d end parenthesis
       end parenthesis
     end line
     line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed
       meta b peano imply parenthesis meta c peano imply meta d end parenthesis
     end line
     line ell e because axiom prime a two indeed
       parenthesis meta b peano imply parenthesis meta c peano imply meta d end parenthesis end parenthesis
       peano imply
       parenthesis
         parenthesis meta b peano imply meta c end parenthesis
         peano imply
         parenthesis meta b peano imply meta d end parenthesis 
       end parenthesis
     end line
     line ell f because rule prime mp modus ponens ell e modus ponens ell d indeed
       parenthesis meta b peano imply meta c end parenthesis
       peano imply
       parenthesis meta b peano imply meta d end parenthesis
     end line
     because rule prime mp modus ponens ell f modus ponens ell a indeed
       meta b peano imply meta d 
     qed
   end math 
]"


\subsection{Corollary "[ math corollary one point ten b end math ]"}
The lemma 
"[ intro corollary one point ten b
   index "C1.10(b)"
   pyk   "corollary one point ten b"
   tex   "C1.10(b)"
end intro ]"
is taken from \cite{mendelson} page 38.

\display{"[ math
  in theory system prime s lemma corollary one point ten b
  says
  all meta b indeed all meta c indeed all meta d indeed
  parenthesis
  meta b peano imply parenthesis meta c peano imply meta d end parenthesis
  infer meta c
  infer meta b peano imply meta d
  end parenthesis
  end lemma
  end math
]"}

"[
math system prime s
  proof of
    corollary one point ten b
  reads
     arbitrary meta b end line
     arbitrary meta c end line
     arbitrary meta d end line
     line ell a premise 
       meta b peano imply parenthesis meta c peano imply meta d end parenthesis
     end line
     line ell b premise
       meta c 
     end line
     line ell c because axiom prime a one indeed
       meta c peano imply parenthesis meta b peano imply meta c end parenthesis
     end line
     line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed
       meta b peano imply meta c
     end line
     line ell e because axiom prime a two indeed
       parenthesis
         meta b peano imply parenthesis meta c peano imply meta d end parenthesis 
       end parenthesis
       peano imply
       parenthesis
         parenthesis meta b peano imply meta c end parenthesis
         peano imply
         parenthesis meta b peano imply meta d end parenthesis
       end parenthesis
     end line
     line ell f because rule prime mp modus ponens ell e modus ponens ell a indeed
       parenthesis meta b peano imply meta c end parenthesis
       peano imply
       parenthesis meta b peano imply meta d end parenthesis
     end line
     because rule prime mp modus ponens ell f modus ponens ell d indeed
       meta b peano imply meta d 
     qed
end math
]"

\subsection{Lemma "[ math lemma prime a one star end math ]"}
The lemma 
"[
intro lemma prime a one star
  index "{A1'}^*"
  pyk   "lemma prime a one star"
  tex   "{A1'}^*"
end intro
]"
is used during the deduction algorithm, when one wishes to add a hypothesis, "[ math meta h end math ]", to a
line of a proof. This will shorten the proof by one line.

\display{"[ math
in theory system prime s
  lemma 
    lemma prime a one star
  says
    all meta a indeed all meta h indeed
    parenthesis
      meta a infer meta h peano imply meta a
    end parenthesis
  end lemma
end math
]"}

"[ math
system prime s proof of 
  lemma prime a one star
reads
  arbitrary meta a end line
  arbitrary meta h end line
  line ell a premise 
    meta a
  end line
  line ell b because axiom prime a one indeed
    meta a peano imply parenthesis meta h peano imply meta a end parenthesis
  end line
  because rule prime mp modus ponens ell b modus ponens ell a indeed
    meta h peano imply meta a
  qed
end math
]"

\subsection{Lemma "[ math lemma prime a two star end math ]"}
Use of the axiom "[ math axiom prime a two end math ]" is often followed 
by a use of the modus ponens rule. If we instead use lemma 
"[
intro lemma prime a two star
  index "{A2'}^*"
  pyk   "lemma prime a two star"
  tex   "{A2'}^*"
end intro
]"
, then the modus ponens is not necessary.

\display{"[ math
in theory system prime s
  lemma 
    lemma prime a two star
  says
    all meta h indeed all meta a indeed all meta b indeed
    parenthesis 
      meta h peano imply parenthesis meta a peano imply meta b end parenthesis
    end parenthesis
    infer
    parenthesis
      parenthesis meta h peano imply meta a end parenthesis
      peano imply
      parenthesis meta h peano imply meta b end parenthesis
    end parenthesis
  end lemma
end math
]"}

"[
math
  system prime s proof of
    lemma prime a two star
  reads
  arbitrary meta h end line
  arbitrary meta a end line
  arbitrary meta b end line
  line ell a premise
    meta h peano imply parenthesis meta a peano imply meta b end parenthesis
  end line
  line ell b because axiom prime a two indeed
    parenthesis 
      meta h peano imply parenthesis meta a peano imply meta b end parenthesis
    end parenthesis
    peano imply
    parenthesis
      parenthesis meta h peano imply meta a end parenthesis
      peano imply
      parenthesis meta h peano imply meta b end parenthesis
    end parenthesis
  end line
  because rule prime mp modus ponens ell b modus ponens ell a indeed
    parenthesis meta h peano imply meta a end parenthesis
    peano imply
    parenthesis meta h peano imply meta b end parenthesis
  qed
end math
]"

\subsection{Lemma "[ math lemma double hyp end math ]"}
The lemma
"[
intro lemma double hyp
  index "Double Hypothesis"
  pyk   "lemma double hyp"
  tex   "Double Hypothesis"
end intro
]"
is used during the deduction algorithm, when one wishes to add a hypothesis, "[ math meta h end math ]", 
to a proof line of the form "[ math meta a peano imply meta b end math ]". This will shorten the proof
by one line.

\display{"[ math
in theory system prime s
  lemma
    lemma double hyp
  says
  all meta a indeed all meta b indeed all meta h indeed
  parenthesis
    meta a peano imply meta b
    infer 
    parenthesis
      parenthesis meta h peano imply meta a end parenthesis
      peano imply
      parenthesis meta h peano imply meta b end parenthesis
    end parenthesis
  end parenthesis
  end lemma
end math
]"}

"[ 
math system prime s proof of
  lemma double hyp
reads
  arbitrary meta a end line
  arbitrary meta b end line
  arbitrary meta h end line
  line ell a premise
    meta a peano imply meta b
  end line
  line ell b because lemma prime a one star modus ponens ell a indeed
    meta h
    peano imply
    parenthesis meta a peano imply meta b end parenthesis
  end line
  because lemma prime a two star modus ponens ell b indeed
    parenthesis meta h peano imply meta a end parenthesis
    peano imply
    parenthesis meta h peano imply meta b end parenthesis
  qed
end math
]"

\subsection{Lemma "[ math lemma one point eight end math ]"}
Lemma 
"[ intro lemma one point eight
   index "L1.8"
   pyk   "lemma one point eight"
   tex   "L1.8"
   end intro ]"
from \cite{mendelson} page 36, is used to introduce the premise at the start of the deduction 
algorithm.

\display{
"[ math 
  in theory system prime s
   lemma 
       lemma one point eight 
   says 
       all meta b indeed parenthesis meta b peano imply meta b end parenthesis
   end lemma 
   end math 
]"}

"[ math
     system prime s
   proof of 
     lemma one point eight
   reads
     arbitrary meta b end line
     line ell a because axiom prime a two indeed 
       parenthesis meta b peano imply parenthesis parenthesis meta b peano imply meta b end parenthesis peano imply meta b end parenthesis end parenthesis 
         peano imply 
       parenthesis parenthesis meta b peano imply parenthesis meta b peano imply meta b end parenthesis end parenthesis peano imply parenthesis meta b peano imply meta b end parenthesis end parenthesis
     end line
     line ell b because axiom prime a one indeed 
       meta b peano imply parenthesis parenthesis meta b peano imply meta b end parenthesis peano imply meta b end parenthesis
     end line
     line ell c because rule prime mp modus ponens ell a modus ponens ell b indeed 
       parenthesis meta b peano imply parenthesis meta b peano imply meta b end parenthesis end parenthesis
         peano imply
       parenthesis meta b peano imply meta b end parenthesis
     end line
     line ell d because axiom prime a one indeed
       meta b peano imply parenthesis meta b peano imply meta b end parenthesis
     end line
     because rule prime mp modus ponens ell c modus ponens ell d indeed 
       meta b peano imply meta b 
     qed
   end math ]"

\subsection{Lemma "[ math tautology one end math ]"}
The lemma that I call 
"[
intro tautology one
  index "Tautology 1"
  pyk   "tautology one"
  tex   "Tautology 1"
end intro
]"
is an all-round useful lemma.

\display{"[ math 
  in theory system prime s lemma tautology one 
    says 
      all meta a indeed
      all meta b indeed
      all meta c indeed
      parenthesis
        parenthesis 
          meta a peano imply parenthesis meta b peano imply meta c end parenthesis 
        end parenthesis 
        infer
        parenthesis 
          meta b peano imply parenthesis meta a peano imply meta c end parenthesis 
        end parenthesis
      end parenthesis
    end lemma 
  end math 
]"}

"[
math system prime s
  proof of
    tautology one
  reads
  arbitrary meta a end line
  arbitrary meta b end line
  arbitrary meta c end line
  line ell a premise 
    meta a peano imply parenthesis meta b peano imply meta c end parenthesis 
  end line
  line ell b because axiom prime a two indeed 
    parenthesis
      meta a peano imply parenthesis meta b peano imply meta c end parenthesis
    end parenthesis
    peano imply
    parenthesis
      parenthesis meta a peano imply meta b end parenthesis
      peano imply
      parenthesis meta a peano imply meta c end parenthesis
    end parenthesis
  end line
  line ell c because rule prime mp modus ponens ell b modus ponens ell a indeed
    parenthesis meta a peano imply meta b end parenthesis
    peano imply 
    parenthesis meta a peano imply meta c end parenthesis
  end line
  line ell d because axiom prime a one indeed
    parenthesis 
      parenthesis meta a peano imply meta b end parenthesis
      peano imply 
      parenthesis meta a peano imply meta c end parenthesis
    end parenthesis
    peano imply
    parenthesis
      meta b
      peano imply
      parenthesis
        parenthesis
          meta a peano imply meta b
        end parenthesis
        peano imply
        parenthesis
          meta a peano imply meta c
        end parenthesis
      end parenthesis
    end parenthesis
  end line
  line ell e because rule prime mp modus ponens ell d modus ponens ell c indeed
    meta b
    peano imply
    parenthesis
      parenthesis
        meta a peano imply meta b
      end parenthesis
      peano imply
      parenthesis
        meta a peano imply meta c
      end parenthesis
    end parenthesis
  end line
  line ell f because axiom prime a two indeed
    parenthesis
    meta b
    peano imply
    parenthesis
      parenthesis
        meta a peano imply meta b
      end parenthesis
      peano imply
      parenthesis
        meta a peano imply meta c
      end parenthesis
    end parenthesis
    end parenthesis
    peano imply
    parenthesis
      parenthesis
        meta b
        peano imply
          parenthesis
            meta a peano imply meta b
          end parenthesis
        end parenthesis
      peano imply
      parenthesis
        meta b
        peano imply
          parenthesis
            meta a peano imply meta c
          end parenthesis
      end parenthesis
    end parenthesis
  end line
  line ell g because rule prime mp modus ponens ell f modus ponens ell e indeed 
    parenthesis
      meta b
      peano imply
        parenthesis
          meta a peano imply meta b
        end parenthesis
      end parenthesis
    peano imply
    parenthesis
      meta b
      peano imply
        parenthesis
          meta a peano imply meta c
        end parenthesis
    end parenthesis
  end line
  line ell h because axiom prime a one indeed 
    meta b 
    peano imply 
    parenthesis meta a peano imply meta b end parenthesis
  end line
  because rule prime mp modus ponens ell g modus ponens ell h indeed
    meta b
    peano imply
    parenthesis meta a peano imply meta c end parenthesis
  qed

end math
]"

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

The purpose of this report is the proof of "[ math lemma prime l three
two h end math ]" 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 "[ math lemma prime l three two a end
math ]" 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 course (h), still to be proven.

Of these lemmas (f), (g) and (h) are proved using induction, which
means that 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 "[ math lemma prime l three two b end math ]"}

"[ intro lemma prime l three two b 
   index "L3.2(b)'"
   pyk "lemma prime l three two b"
   tex "L3.2(b)'"
   end intro ]"

\display{"[ 
  math in theory system prime s lemma lemma prime l three two b
  says 
    all meta t indeed
    all meta r indeed
    meta t peano is meta r peano imply meta r peano is meta t 
  end lemma end math 
]"}

"[
math system prime s
  proof of 
    lemma prime l three two b
  reads
    arbitrary meta t end line
    arbitrary meta r end line
    line ell a because axiom prime s one indeed
      meta t peano is meta r 
      peano imply
      parenthesis
       meta t peano is meta t
        peano imply
       meta r peano is meta t
      end parenthesis
    end line
    line ell b because lemma prime l three two a indeed
      meta t peano is meta t
    end line
    because corollary one point ten b modus ponens ell a modus ponens ell b indeed
      meta t peano is meta r 
      peano imply 
      meta r peano is meta t
    qed
end math
]"



\subsection{Lemma "[ math lemma prime l three two c end math ]"}

"[
intro lemma prime l three two c
 index "L3.2(c)'"
 pyk   "lemma prime l three two c"
 tex   "L3.2(c)'"
end intro
]"

\display{"[
math 
 in theory system prime s
  lemma
   lemma prime l three two c
  says
   all meta t indeed
   all meta r indeed
   all meta s indeed
   meta t peano is meta r
     peano imply
   parenthesis
     meta r peano is meta s peano imply meta t peano is meta s
   end parenthesis
  end lemma
end math
]"}


"[
math system prime s
  proof of
    lemma prime l three two c
  reads
    arbitrary meta t end line
    arbitrary meta r end line
    arbitrary meta s end line
    line ell a because axiom prime s one indeed
      meta r peano is meta t
      peano imply
      parenthesis
        meta r peano is meta s peano imply meta t peano is meta s
      end parenthesis
    end line
    line ell b because lemma prime l three two b indeed 
      meta t peano is meta r peano imply meta r peano is meta t
    end line
    because corollary one point ten a modus ponens ell b modus ponens ell a indeed
      meta t peano is meta r
      peano imply
      parenthesis
        meta r peano is meta s peano imply meta t peano is meta s
      end parenthesis
    qed 
end math
]"



\subsection{Lemma "[ math lemma prime l three two d end math ]"}

"[
intro lemma prime l three two d
  index "L3.2(d)'"
  pyk   "lemma prime l three two d"
  tex   "L3.2(d)'"
end intro
]"

\display{"[ math 
in theory system prime s
  lemma
    lemma prime l three two d
  says
  all meta t indeed
  all meta r indeed
  all meta s indeed
  meta r peano is meta t
  peano imply
    parenthesis
      meta s peano is meta t
      peano imply
      meta r peano is meta s
    end parenthesis
  end lemma
end math
]"}

"[ math 
system prime s
  proof of  
    lemma prime l three two d
  reads
    arbitrary meta t end line
    arbitrary meta r end line
    arbitrary meta s end line
    line ell a because lemma prime l three two c indeed
      meta r peano is  meta t
      peano imply
      parenthesis
        meta t peano is meta s
        peano imply
        meta r peano is meta s
      end parenthesis
    end line
    line ell b because tautology one modus ponens ell a indeed
      meta t peano is meta s
      peano imply
      parenthesis
        meta r peano is  meta t
        peano imply
        meta r peano is meta s
      end parenthesis
    end line 
    line ell c because lemma prime l three two b indeed
      meta s peano is meta t peano imply meta t peano is meta s
    end line
    line ell d because corollary one point ten a modus ponens ell c modus ponens ell b indeed
      meta s peano is meta t
      peano imply
      parenthesis
        meta r peano is  meta t
        peano imply
        meta r peano is meta s
      end parenthesis
    end line
    because tautology one modus ponens ell d indeed
      meta r peano is  meta t
      peano imply
      parenthesis
        meta s peano is meta t
        peano imply
        meta r peano is meta s
      end parenthesis
    qed 
end math
]"


\subsection{Lemma "[ math lemma prime l three two f end math ]"}
To prove 
"[
intro lemma prime l three two f
  index "L3.2(f)'"
  pyk   "lemma prime l three two f"
  tex   "L3.2(f)'"
end intro
]"
using induction, we will need to prove the base case
"[
intro lemma prime l three two f base
  index "{L3.2(f)'}_{BASE}"
  pyk   "lemma prime l three two f base"
  tex   "{L3.2(f)'}_{BASE}"
end intro
]" (section \ref{f.base})
and the induction step
"[
intro lemma prime l three two f hyp
  index "{L3.2(f)'}_{HYP}"
  pyk   "lemma prime l three two f hyp"
  tex   "{L3.2(f)'}_{HYP}"
end intro
]" (section \ref{f.hyp}).

\display{"[ math
in theory system prime s
  lemma
    lemma prime l three two f
  says
    peano all peano t indeed 
    parenthesis
      peano t peano is peano zero peano plus peano t
    end parenthesis
  end lemma
end math
]"}

"[
math system prime s proof of
  lemma prime l three two f
reads
  line ell a because lemma prime l three two f base indeed
    peano zero peano is peano zero peano plus peano zero
  end line
  line ell b because lemma prime l three two f hyp indeed
    peano all peano t indeed 
    parenthesis
      peano t peano is peano zero peano plus peano t
      peano imply
      peano t peano succ peano is peano zero peano plus peano t peano succ
    end parenthesis
  end line
  line ell c because axiom prime s nine indeed
    parenthesis
      peano zero peano is peano zero peano plus peano zero 
    end parenthesis
    peano imply 
    parenthesis
      parenthesis
        peano all peano t indeed
        parenthesis
          peano t            peano is peano zero peano plus peano t
          peano imply
          peano t peano succ peano is peano zero peano plus peano t peano succ
        end parenthesis
      end parenthesis
      peano imply
      parenthesis
        peano all peano t indeed
        parenthesis
          peano t peano is peano zero peano plus peano t
        end parenthesis
      end parenthesis
    end parenthesis
  end line
  line ell d because rule prime mp modus ponens ell c modus ponens ell a indeed
    parenthesis
      peano all peano t indeed
      parenthesis
        peano t            peano is peano zero peano plus peano t
        peano imply
        peano t peano succ peano is peano zero peano plus peano t peano succ
      end parenthesis
    end parenthesis
    peano imply
    parenthesis
      peano all peano t indeed
      parenthesis
        peano t peano is peano zero peano plus peano t
      end parenthesis
    end parenthesis
  end line
  because rule prime mp modus ponens ell d modus ponens ell b indeed
      peano all peano t indeed
      parenthesis
        peano t peano is peano zero peano plus peano t
      end parenthesis
  qed
end math
]"

\subsubsection{The base case of "[ math lemma prime l three two f end math ]"\label{f.base}}

\display{"[ math
in theory system prime s
  lemma
    lemma prime l three two f base
  says
    peano zero peano is peano zero peano plus peano zero
  end lemma
end math
]"}


"[
math system prime s proof of
  lemma prime l three two f base
reads
  line ell a because axiom prime s five indeed
    peano zero peano plus peano zero peano is peano zero
  end line
  line ell b because lemma prime l three two b indeed
    peano zero peano plus peano zero peano is peano zero
    peano imply
    peano zero peano is peano zero peano plus peano zero
  end line
  because rule prime mp modus ponens ell b modus ponens ell a indeed
    peano zero peano is peano zero peano plus peano zero
  qed
end math
]"

\subsubsection{The induction step of "[ math lemma prime l three two f end math ]"\label{f.hyp}}

\display{"[ math
in theory system prime s
  lemma 
    lemma prime l three two f hyp
  says
  peano all peano t indeed 
  parenthesis
    peano t peano is peano zero peano plus peano t
    peano imply
    peano t peano succ peano is peano zero peano plus peano t peano succ
  end parenthesis
  end lemma
end math
]"}

"[
math system prime s proof of
  lemma prime l three two f hyp
reads
  line ell a because lemma one point eight indeed
    peano t peano is peano zero peano plus peano t
    peano imply
    peano t peano is peano zero peano plus peano t
  end line
  line ell b because axiom prime s six indeed 
    peano zero peano plus peano t peano succ 
    peano is
    parenthesis peano zero peano plus peano t end parenthesis peano succ
  end line
  line ell c because axiom prime a one indeed
    parenthesis
      peano zero peano plus peano t peano succ
      peano is
      parenthesis peano zero peano plus peano t end parenthesis peano succ
    end parenthesis
    peano imply
    parenthesis
      peano t peano is peano zero peano plus peano t
      peano imply
      parenthesis
        peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
      end parenthesis
    end parenthesis
  end line
  line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed
    peano t peano is peano zero peano plus peano t
    peano imply
    parenthesis
      peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
    end parenthesis
  end line
  line ell e because axiom prime s two indeed
    peano t peano is parenthesis peano zero peano plus peano t end parenthesis
    peano imply
    peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
  end line
  line ell f because axiom prime a one indeed
    parenthesis
      peano t peano is parenthesis peano zero peano plus peano t end parenthesis
      peano imply
      peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
    end parenthesis
    peano imply
    parenthesis
      peano t peano is peano zero peano plus peano t
      peano imply
      parenthesis
        peano t peano is parenthesis peano zero peano plus peano t end parenthesis
        peano imply
        peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
      end parenthesis
    end parenthesis    
  end line
  line ell g because rule prime mp modus ponens ell f modus ponens ell e indeed
    peano t peano is peano zero peano plus peano t
    peano imply
    parenthesis
      peano t peano is parenthesis peano zero peano plus peano t end parenthesis
      peano imply
      peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
    end parenthesis
  end line
  line ell h because lemma prime a two star modus ponens ell g indeed
    parenthesis 
      peano t peano is peano zero peano plus peano t 
      peano imply
      peano t peano is peano zero peano plus peano t 
    end parenthesis
    peano imply
    parenthesis 
      peano t peano is peano zero peano plus peano t 
      peano imply
      peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
    end parenthesis
  end line
  line ell i because rule prime mp modus ponens ell h modus ponens ell a indeed
    peano t peano is peano zero peano plus peano t 
    peano imply
    peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
  end line
  line ell j because lemma prime l three two d indeed 
    peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
    peano imply
    parenthesis
      peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
      peano imply
      peano t peano succ peano is peano zero peano plus peano t peano succ
    end parenthesis
  end line
  line ell k because hypothesize modus ponens ell j indeed
    peano t peano is peano zero peano plus peano t
    peano imply
    parenthesis
      peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
      peano imply
      parenthesis
        peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
        peano imply
        peano t peano succ peano is peano zero peano plus peano t peano succ
      end parenthesis
    end parenthesis
  end line
  line ell l because lemma prime a two star modus ponens ell k indeed
    parenthesis
      peano t peano is peano zero peano plus peano t
      peano imply
      peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
    end parenthesis
    peano imply
    parenthesis
      peano t peano is peano zero peano plus peano t
      peano imply
      parenthesis
        peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
        peano imply
        peano t peano succ peano is peano zero peano plus peano t peano succ
      end parenthesis
    end parenthesis
  end line
  line ell m because rule prime mp modus ponens ell l modus ponens ell i indeed
    peano t peano is peano zero peano plus peano t
    peano imply
    parenthesis
      peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
      peano imply
      peano t peano succ peano is peano zero peano plus peano t peano succ
    end parenthesis
  end line
  line ell n because lemma prime a two star modus ponens ell m indeed
    parenthesis
      peano t peano is peano zero peano plus peano t
      peano imply
      peano zero peano plus peano t peano succ peano is parenthesis peano zero peano plus peano t end parenthesis peano succ
    end parenthesis
      peano imply
    parenthesis
      peano t peano is peano zero peano plus peano t
      peano imply
      peano t peano succ peano is peano zero peano plus peano t peano succ
    end parenthesis
  end line
  line ell o because rule prime mp modus ponens ell n modus ponens ell d indeed
    peano t peano is peano zero peano plus peano t
    peano imply
    peano t peano succ peano is peano zero peano plus peano t peano succ
  end line
  because rule prime gen modus ponens ell o indeed 
    peano all peano t indeed 
    parenthesis
      peano t peano is peano zero peano plus peano t
      peano imply
      peano t peano succ peano is peano zero peano plus peano t peano succ
    end parenthesis
  qed
end math
]"


\subsection{Lemma "[ math lemma prime l three two g end math ]"}
To prove 
"[
intro lemma prime l three two g
  index "L3.2(g)'"
  pyk   "lemma prime l three two g"
  tex   "L3.2(g)'"
end intro
]"
using induction, we will need to prove the base case
"[
intro lemma prime l three two g base
  index "{L3.2(g)'}_{BASE}"
  pyk   "lemma prime l three two g"
  tex   "{L3.2(g)'}_{BASE}"
end intro
]"(section \ref{g.base})
and the induction step
"[
intro lemma prime l three two g hyp
  index "{L3.2(g)'}_{HYP}"
  pyk   "lemma prime l three two g hyp"
  tex   "{L3.2(g)'}_{HYP}"
end intro
]"(section \ref{g.hyp}).

\display{"[ math
in theory system prime s
  lemma
    lemma prime l three two g
  says
    peano all peano t indeed peano all peano r indeed
    parenthesis
      peano t peano succ peano plus peano r peano is 
      parenthesis peano t peano plus peano r end parenthesis peano succ
    end parenthesis
  end lemma
end math
]"}

"[
math system prime s proof of
  lemma prime l three two g
reads
line ell a because lemma prime l three two g base indeed
  peano all peano t indeed
  parenthesis
    peano t peano succ peano plus peano zero 
    peano is
    parenthesis
      peano t peano plus peano zero
    end parenthesis peano succ
  end parenthesis
end line
line ell b because lemma prime l three two g hyp indeed
  peano all peano r indeed 
  parenthesis
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
    peano imply
    peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ  end parenthesis peano succ
  end parenthesis
end line
line ell c because axiom prime s nine indeed


  peano all peano t indeed
  parenthesis
    peano t peano succ peano plus peano zero peano is parenthesis peano t peano plus peano zero end parenthesis peano succ
  end parenthesis


  peano imply


  parenthesis

    peano all peano r indeed 
      parenthesis

        parenthesis
          peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
        end parenthesis

        peano imply

        parenthesis
          peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ
        end parenthesis

      end parenthesis

      peano imply

      parenthesis
        peano all peano r indeed
        parenthesis
          peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
        end parenthesis
      end parenthesis

  end parenthesis


end line
line ell d because rule prime mp modus ponens ell c modus ponens ell a indeed
  peano all peano r indeed 
    parenthesis

      parenthesis
        peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
      end parenthesis

      peano imply

      parenthesis
        peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ
      end parenthesis

    end parenthesis

    peano imply

     parenthesis
      peano all peano r indeed
      parenthesis
        peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
      end parenthesis
    end parenthesis
end line
line ell e because rule prime mp modus ponens ell d modus ponens ell b indeed
  peano all peano r indeed
  parenthesis
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
  end parenthesis
end line
because rule prime gen modus ponens ell e indeed
  peano all peano t indeed
  peano all peano r indeed
  parenthesis
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
  end parenthesis
qed
end math
]"


\subsubsection{Base case of "[ math lemma prime l three two g end math ]"\label{g.base}}

\display{"[ math
in theory system prime s
  lemma
    lemma prime l three two g base
  says
    peano all peano t indeed
    parenthesis
      peano t peano succ peano plus peano zero 
      peano is
      parenthesis
        peano t peano plus peano zero
      end parenthesis peano succ
    end parenthesis
  end lemma
end math
]"}

"[ math
system prime s proof of
  lemma prime l three two g base
reads
  line ell a because axiom prime s five indeed
    peano t peano succ peano plus peano zero peano is peano t peano succ
  end line
  line ell b because axiom prime s five indeed
    peano t peano plus peano zero peano is peano t
  end line
  line ell c because axiom prime s two indeed
    peano t peano plus peano zero peano is peano t 
    peano imply
    parenthesis
      peano t peano plus peano zero
    end parenthesis peano succ
    peano is peano t peano succ
  end line
  line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed
    parenthesis
      peano t peano plus peano zero
    end parenthesis peano succ
    peano is peano t peano succ
  end line
  line ell e because lemma prime l three two d indeed
    parenthesis peano t peano succ peano plus peano zero end parenthesis peano is peano t peano succ
    peano imply
    parenthesis 
      parenthesis peano t peano plus peano zero end parenthesis peano succ
      peano is peano t peano succ
      peano imply
      parenthesis peano t peano succ peano plus peano zero end parenthesis
      peano is
      parenthesis peano t peano plus peano zero end parenthesis peano succ
    end parenthesis
  end line
  line ell f because rule prime mp modus ponens ell e modus ponens ell a indeed
    parenthesis peano t peano plus peano zero end parenthesis peano succ
    peano is 
    peano t peano succ
    peano imply
    parenthesis peano t peano succ peano plus peano zero end parenthesis
    peano is
    parenthesis peano t peano plus peano zero end parenthesis peano succ
  end line
  line ell g because rule prime mp modus ponens ell f modus ponens ell d indeed
    peano t peano succ peano plus peano zero peano is 
    parenthesis
      peano t peano plus peano zero
    end parenthesis peano succ
  end line
  because rule prime gen modus ponens ell g indeed
    peano all peano t indeed parenthesis
      peano t peano succ peano plus peano zero peano is 
      parenthesis
        peano t peano plus peano zero
      end parenthesis peano succ
    end parenthesis
  qed
end math
]"

\subsubsection{Induction step of "[ math lemma prime l three two g end math ]"\label{g.hyp}}

\display{"[ math
in theory system prime s 
  lemma 
    lemma prime l three two g hyp
  says
    peano all peano r indeed 
    parenthesis
      parenthesis
        peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
      end parenthesis
      peano imply
      parenthesis
        peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ  end parenthesis peano succ
      end parenthesis
    end parenthesis
  end lemma
end math
]"}

"[ math
system prime s proof of 
  lemma prime l three two g hyp
reads
  locally define meta h as
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
  end line
  line ell a because lemma one point eight indeed
    meta h
    peano imply
    meta h
  end line
  line ell b because axiom prime s six indeed
    peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ
  end line
  line ell c because lemma prime a one star modus ponens ell b indeed
    meta h peano imply
    peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ
  end line
  line ell d because axiom prime s two indeed
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
    peano imply
    parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
  end line
  line ell e because lemma prime a one star modus ponens ell d indeed
    meta h peano imply
    parenthesis
      peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
      peano imply
      parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
    end parenthesis
  end line
  line ell f because lemma prime a two star modus ponens ell e indeed
    parenthesis
      meta h 
      peano imply
      peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
    end parenthesis
    peano imply
    parenthesis
      meta h 
      peano imply
      parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
    end parenthesis
  end line
  line ell g because rule prime mp modus ponens ell f modus ponens ell a indeed 
    meta h 
    peano imply
    parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
  end line 
  line ell h because lemma prime l three two c indeed
    peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ
    peano imply
    parenthesis
      parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
      peano imply
      peano t peano succ peano plus peano r peano succ peano is   parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
    end parenthesis
  end line
  line ell i because lemma prime a one star modus ponens ell h indeed 
    meta h peano imply
    parenthesis
      peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ
      peano imply
      parenthesis
        parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
        peano imply
        peano t peano succ peano plus peano r peano succ peano is   parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
      end parenthesis
    end parenthesis
  end line
  line ell j because lemma prime a two star modus ponens ell i indeed
    parenthesis
      meta h peano imply
      peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano succ peano plus peano r end parenthesis peano succ
    end parenthesis
      peano imply
    parenthesis
      meta h peano imply
      parenthesis
        parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
        peano imply
        peano t peano succ peano plus peano r peano succ peano is   parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
      end parenthesis
    end parenthesis
  end line
  line ell k because rule prime mp modus ponens ell j modus ponens ell c indeed
    meta h peano imply
    parenthesis
      parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
      peano imply
      peano t peano succ peano plus peano r peano succ peano is   parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
    end parenthesis
  end line
  line ell l because lemma prime a two star modus ponens ell k indeed
    parenthesis
      meta h peano imply
      parenthesis peano t peano succ peano plus peano r end parenthesis peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
    end parenthesis
    peano imply
    parenthesis
       meta h peano imply
       peano t peano succ peano plus peano r peano succ peano is   parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
    end parenthesis    
  end line
  line ell m because rule prime mp modus ponens ell l modus ponens ell g indeed
     meta h peano imply
     peano t peano succ peano plus peano r peano succ peano is   parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
  end line
  line ell n because axiom prime s six indeed
    peano t peano plus peano r peano succ 
    peano is 
    parenthesis 
      peano t peano plus peano r 
    end parenthesis peano succ
  end line
  line ell o because lemma prime a one star modus ponens ell n indeed
    meta h peano imply 
    peano t peano plus peano r peano succ 
    peano is 
    parenthesis 
      peano t peano plus peano r 
    end parenthesis peano succ
  end line
  line ell p because axiom prime s two indeed
    peano t peano plus peano r peano succ 
    peano is
    parenthesis 
      peano t peano plus peano r
    end parenthesis peano succ
  peano imply
    parenthesis 
      peano t peano plus peano r peano succ
    end parenthesis peano succ
    peano is
    parenthesis parenthesis 
      peano t peano plus peano r
    end parenthesis peano succ end parenthesis peano succ
  end line
  line ell q because lemma prime a one star modus ponens ell p indeed
    meta h peano imply
    parenthesis
      peano t peano plus peano r peano succ 
      peano is
      parenthesis 
        peano t peano plus peano r
      end parenthesis peano succ
    peano imply
      parenthesis 
        peano t peano plus peano r peano succ
      end parenthesis peano succ
      peano is
      parenthesis parenthesis 
        peano t peano plus peano r
      end parenthesis peano succ end parenthesis peano succ
    end parenthesis
  end line
  line ell r because lemma prime a two star indeed
     parenthesis
      meta h peano imply
      peano t peano plus peano r peano succ 
      peano is
      parenthesis 
        peano t peano plus peano r
      end parenthesis peano succ
     end parenthesis
   peano imply 
     parenthesis
     meta h peano imply
      parenthesis 
        peano t peano plus peano r peano succ
      end parenthesis peano succ
      peano is
      parenthesis parenthesis 
        peano t peano plus peano r
      end parenthesis peano succ end parenthesis peano succ
     end parenthesis
  end line
  line ell s because rule prime mp modus ponens ell r modus ponens ell o indeed
    meta h peano imply
    parenthesis 
      peano t peano plus peano r peano succ
    end parenthesis peano succ
    peano is
    parenthesis parenthesis 
      peano t peano plus peano r
    end parenthesis peano succ end parenthesis peano succ
  end line
 line ell t because lemma prime l three two d indeed
   peano t peano succ peano plus peano r peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
   peano imply
   parenthesis 
     parenthesis peano t peano plus peano r peano succ end parenthesis peano succ 
     peano is
     parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
     peano imply 
     peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ
   end parenthesis
 end line 
 line ell u because lemma prime a one star modus ponens ell t indeed
   meta h peano imply
   parenthesis
     peano t peano succ peano plus peano r peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
     peano imply
     parenthesis 
       parenthesis peano t peano plus peano r peano succ end parenthesis peano succ 
       peano is
       parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
       peano imply 
       peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ
     end parenthesis
   end parenthesis
 end line
 line ell v because lemma prime a two star modus ponens ell u indeed
   parenthesis
     meta h peano imply
     peano t peano succ peano plus peano r peano succ peano is parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
   end parenthesis

   peano imply

   parenthesis
     meta h peano imply
     parenthesis 
       parenthesis peano t peano plus peano r peano succ end parenthesis peano succ 
       peano is
       parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
       peano imply 
       peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ
     end parenthesis
   end parenthesis
 end line
 line ell w because rule prime mp modus ponens ell v modus ponens ell m indeed
   meta h peano imply
   parenthesis 
     parenthesis peano t peano plus peano r peano succ end parenthesis peano succ 
     peano is
     parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
     peano imply 
     peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ
   end parenthesis
 end line
 line ell x because lemma prime a two star modus ponens ell w indeed 
   parenthesis 
     meta h 
     peano imply
     parenthesis peano t peano plus peano r peano succ end parenthesis peano succ 
     peano is
     parenthesis parenthesis peano t peano plus peano r end parenthesis peano succ end parenthesis peano succ
   end parenthesis
   peano imply 
   parenthesis
     meta h peano imply
     peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ
   end parenthesis
 end line
 line ell y because rule prime mp modus ponens ell x modus ponens ell s indeed
   meta h peano imply
   peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ
 end line
{
 line ell z because rule prime gen modus ponens ell y indeed
   peano all peano t indeed
   parenthesis
     meta h peano imply
     peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ
   end parenthesis
 end line
}
 because rule prime gen modus ponens ell y { ell z } indeed
   peano all peano r indeed { peano all peano t indeed }
   parenthesis
     meta h peano imply
     peano t peano succ peano plus peano r peano succ peano is parenthesis peano t peano plus peano r peano succ end parenthesis peano succ
   end parenthesis
 qed
end math
]"


\subsection{Lemma "[ math lemma prime l three two h end math ]"\label{res.lemma}}
To prove
"[
intro lemma prime l three two h
  index "L3.2(h)'"
  pyk   "lemma prime l three two h"
  tex   "L3.2(h)'"
end intro
]"
using induction, we will need to prove the base case
"[
intro lemma prime l three two h base
  index "{L3.2(h)'}_{BASE}"
  pyk   "lemma prime l three two h base"
  tex   "{L3.2(h)'}_{BASE}"
end intro
]"(section \ref{h.base})
and the induction step
"[
intro lemma prime l three two h hyp
  index "{L3.2(h)'}_{HYP}"
  pyk   "lemma prime l three two h hyp"
  tex   "{L3.2(h)'}_{HYP}"
end intro
]"(section \ref{h.hyp}).

\display{"[ math
in theory system prime s
  lemma
    lemma prime l three two h
  says
    peano all peano t indeed peano all peano r indeed
    parenthesis
      peano t peano plus peano r peano is peano r peano plus peano t
    end parenthesis
  end lemma
end math
]"}

"[ math
system prime s proof of
  lemma prime l three two h
reads
line ell a because lemma prime l three two h base indeed
  peano all peano t indeed
  parenthesis
    peano t peano plus peano zero peano is peano zero peano plus peano t
  end parenthesis
end line
line ell b because lemma prime l three two h hyp indeed
  peano all peano r indeed
  parenthesis
    peano t peano plus peano r            peano is peano r            peano plus peano t
    peano imply
    peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t
  end parenthesis
end line
line ell c because axiom prime s nine indeed
  peano all peano t indeed
  parenthesis
    peano t peano plus peano zero peano is peano zero peano plus peano t
  end parenthesis

  peano imply

  parenthesis

    parenthesis
      peano all peano r indeed
      parenthesis

        peano t peano plus peano r            peano is peano r             peano plus peano t
        peano imply
        peano t peano plus peano r peano succ peano is peano r peano succ  peano plus peano t

      end parenthesis

    end parenthesis

    peano imply

    peano all peano r indeed
    parenthesis
      peano t peano plus peano r peano is peano r peano plus peano t
    end parenthesis

  end parenthesis
end line
line ell d because rule prime mp modus ponens ell c modus ponens ell a indeed

    peano all peano r indeed
    parenthesis

      peano t peano plus peano r            peano is peano r             peano plus peano t
      peano imply
      peano t peano plus peano r peano succ peano is peano r peano succ  peano plus peano t

    end parenthesis

    peano imply

    peano all peano r indeed
    parenthesis
      peano t peano plus peano r peano is peano r peano plus peano t
    end parenthesis

end line
line ell e because rule prime mp modus ponens ell d modus ponens ell b indeed
  peano all peano r indeed
  parenthesis
    peano t peano plus peano r peano is peano r peano plus peano t
  end parenthesis
end line
because rule prime gen modus ponens ell e indeed
  peano all peano t indeed peano all peano r indeed
  parenthesis
    peano t peano plus peano r peano is peano r peano plus peano t
  end parenthesis
qed
end math
]"

\subsubsection{Base case of "[ math lemma prime l three two h end math ]"\label{h.base}}

\display{"[ math
in theory system prime s
  lemma
    lemma prime l three two h base
  says
    peano all peano t indeed
    parenthesis
      peano t peano plus peano zero peano is peano zero peano plus peano t
    end parenthesis
  end lemma
end math
]"}

"[ math 
system prime s proof of 
  lemma prime l three two h base
reads
line ell a because axiom prime s five indeed
  peano t peano plus peano zero peano is peano t
end line
line ell b because lemma prime l three two f indeed
  peano all peano t indeed 
  parenthesis
    peano t peano is peano zero peano plus peano t
  end parenthesis
end line
line ell c because axiom prime a four at peano t indeed
  parenthesis
    peano all peano t indeed 
    parenthesis  peano t peano is peano zero peano plus peano t end parenthesis
  end parenthesis

  peano imply

  parenthesis    peano t peano is peano zero peano plus peano t end parenthesis
end line
line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed
  peano t peano is peano zero peano plus peano t
end line
line ell e because lemma prime l three two c indeed
    peano t peano plus peano zero  peano is peano t
    peano imply
  parenthesis
    peano t                        peano is  peano zero peano plus peano t
   peano imply
    peano t peano plus peano zero  peano is  peano zero peano plus peano t
  end parenthesis
end line
line ell f because rule prime mp modus ponens ell e modus ponens ell a indeed
  peano t                        peano is  peano zero peano plus peano t
 peano imply
  peano t peano plus peano zero  peano is  peano zero peano plus peano t
end line
line ell g because rule prime mp modus ponens ell f modus ponens ell d indeed
  peano t peano plus peano zero  peano is  peano zero peano plus peano t
end line
because rule prime gen modus ponens ell g indeed
  peano all peano t indeed
  parenthesis
    peano t peano plus peano zero  peano is  peano zero peano plus peano t
  end parenthesis
qed
end math
]"

\subsubsection{Induction step of "[ math lemma prime l three two h end math ]"\label{h.hyp}}

For proving the induction step, we will need the lemma
"[ 
intro lemma prime l three two h swap
  index "L3.2h_{SWAP}"
  pyk   "lemma prime l three two h hyp"
  tex   "L3.2h_{SWAP}"
end intro
]".

\display{"[ math
in theory system prime s
  lemma 
    lemma prime l three two h swap
  says
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
    infer
    peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ
  end lemma
end math
]"}
"[ math 
system prime s proof of 
  lemma prime l three two h swap
reads
  line ell a premise 
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
  end line 
  line ell b because rule prime gen modus ponens ell a indeed
    peano all peano t indeed
    parenthesis
      peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
    end parenthesis
  end line
  line ell c because axiom prime a four at peano q indeed
    peano all peano t indeed
    parenthesis
      peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
    end parenthesis
    peano imply 
    peano q peano succ peano plus peano r peano is parenthesis peano q peano plus peano r end parenthesis peano succ
  end line
  line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed
    peano q peano succ peano plus peano r peano is parenthesis peano q peano plus peano r end parenthesis peano succ
  end line
  line ell e because rule prime gen modus ponens ell d indeed
    peano all peano r indeed
    parenthesis
      peano q peano succ peano plus peano r peano is parenthesis peano q peano plus peano r end parenthesis peano succ
    end parenthesis
  end line
  line ell f because axiom prime a four at peano t indeed
    peano all peano r indeed
    parenthesis
      peano q peano succ peano plus peano r peano is parenthesis peano q peano plus peano r end parenthesis peano succ
    end parenthesis
    peano imply
    peano q peano succ peano plus peano t peano is parenthesis peano q peano plus peano t end parenthesis peano succ
  end line
  line ell g because rule prime mp modus ponens ell f modus ponens ell e indeed
    peano q peano succ peano plus peano t peano is parenthesis peano q peano plus peano t end parenthesis peano succ
  end line
  line ell h because rule prime gen modus ponens ell g indeed
    peano all peano q indeed
    parenthesis
      peano q peano succ peano plus peano t peano is parenthesis peano q peano plus peano t end parenthesis peano succ
    end parenthesis
  end line
  line ell i because axiom prime a four at peano r indeed

    peano all peano q indeed
    parenthesis
      peano q peano succ peano plus peano t peano is parenthesis peano q peano plus peano t end parenthesis peano succ
    end parenthesis

    peano imply

    peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ

  end line
  because rule prime mp modus ponens ell i modus ponens ell h indeed
    peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ
  qed 
end math 
]"\\
$\quad$\\
Now we are ready to prove the induction step.
$\quad$\\

\display{"[ math
in theory system prime s
  lemma 
    lemma prime l three two h hyp
  says
    peano all peano r indeed
    parenthesis
      peano t peano plus peano r            peano is peano r            peano plus peano t
      peano imply
      peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t
    end parenthesis
  end lemma
end math
]"}

"[ math 
system prime s proof of 
  lemma prime l three two h hyp
reads
locally define meta h as
  peano t peano plus peano r peano is peano r peano plus peano t
end line
line ell a because lemma one point eight indeed
  meta h peano imply meta h
end line
line ell b because axiom prime s six indeed
  peano t peano plus peano r peano succ peano is 
  parenthesis
    peano t peano plus peano r
  end parenthesis peano succ
end line
line ell c because lemma prime a one star modus ponens ell b indeed
  meta h peano imply
  peano t peano plus peano r peano succ peano is 
  parenthesis
    peano t peano plus peano r
  end parenthesis peano succ
end line
line ell d because axiom prime s two indeed
  peano t peano plus peano r  peano is  peano r peano plus peano t 
  peano imply
  parenthesis
   peano t peano plus peano r  
  end parenthesis peano succ
  peano is  
  parenthesis 
    peano r peano plus peano t 
  end parenthesis peano succ
end line
line ell e because lemma double hyp modus ponens ell d indeed
  parenthesis
    meta h peano imply
    peano t peano plus peano r  peano is  peano r peano plus peano t 
  end parenthesis
  peano imply
  parenthesis
    meta h peano imply
    parenthesis
      parenthesis
       peano t peano plus peano r  
      end parenthesis peano succ
      peano is  
      parenthesis 
        peano r peano plus peano t 
      end parenthesis peano succ
    end parenthesis
  end parenthesis
end line
line ell e because rule prime mp modus ponens ell e modus ponens ell a indeed
  meta h peano imply
  parenthesis
    parenthesis
     peano t peano plus peano r  
    end parenthesis peano succ
    peano is  
    parenthesis 
      peano r peano plus peano t 
    end parenthesis peano succ
  end parenthesis
end line
line ell f because lemma prime l three two c indeed
  peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ
  peano imply
  parenthesis
    parenthesis
      peano t peano plus peano r
    end parenthesis peano succ
    peano is
    parenthesis
      peano r peano plus peano t
    end parenthesis peano succ
    peano imply
      peano t peano plus peano r peano succ
    peano is
    parenthesis
      peano r peano plus peano t
    end parenthesis peano succ
  end parenthesis
end line
line ell g because lemma double hyp modus ponens ell f indeed
    parenthesis
      meta h peano imply
      peano t peano plus peano r peano succ peano is parenthesis peano t peano plus peano r end parenthesis peano succ
    end parenthesis

    peano imply

    parenthesis
      meta h peano imply
      parenthesis
        parenthesis
          peano t peano plus peano r
        end parenthesis peano succ
        peano is
        parenthesis
          peano r peano plus peano t
        end parenthesis peano succ
        peano imply
          peano t peano plus peano r peano succ
        peano is
        parenthesis
          peano r peano plus peano t
        end parenthesis peano succ
      end parenthesis
    end parenthesis
end line
line ell h because rule prime mp modus ponens ell g modus ponens ell c indeed
      meta h peano imply
      parenthesis
        parenthesis
          peano t peano plus peano r
        end parenthesis peano succ
        peano is
        parenthesis
          peano r peano plus peano t
        end parenthesis peano succ
        peano imply
          peano t peano plus peano r peano succ
        peano is
        parenthesis
          peano r peano plus peano t
        end parenthesis peano succ
      end parenthesis
end line
line ell i because lemma prime a two star modus ponens ell h indeed

      parenthesis
        meta h peano imply
        parenthesis
          peano t peano plus peano r
        end parenthesis peano succ
        peano is
        parenthesis
          peano r peano plus peano t
        end parenthesis peano succ
      end parenthesis

        peano imply

      parenthesis
        meta h peano imply
        peano t peano plus peano r peano succ
        peano is
        parenthesis
          peano r peano plus peano t
        end parenthesis peano succ
      end parenthesis
end line
line ell j because rule prime mp modus ponens ell i modus ponens ell e indeed
        meta h peano imply
        peano t peano plus peano r peano succ
        peano is
        parenthesis
          peano r peano plus peano t
        end parenthesis peano succ
end line
line ell k because lemma prime l three two d indeed
  peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ
  peano imply
  parenthesis
    peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ
    peano imply
    peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t
  end parenthesis
end line
line ell l because lemma double hyp modus ponens ell k indeed

  parenthesis
    meta h peano imply
    peano t peano plus peano r peano succ peano is parenthesis peano r peano plus peano t end parenthesis peano succ
  end parenthesis

  peano imply

  parenthesis
    meta h peano imply
    parenthesis
      peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ
      peano imply
      peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t
    end parenthesis
  end parenthesis

end line
line ell m because rule prime mp modus ponens ell l modus ponens ell j indeed
    meta h peano imply
    parenthesis
      peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ
      peano imply
      peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t
    end parenthesis
end line
line ell n because lemma prime l three two g indeed
  peano all peano t indeed peano all peano r indeed
  parenthesis
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
  end parenthesis
end line
line ell o because axiom prime a four at peano t indeed
  peano all peano t indeed peano all peano r indeed
  parenthesis
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
  end parenthesis

  peano imply

  peano all peano r indeed
  parenthesis
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
  end parenthesis
end line
line ell o because axiom prime a four at peano t indeed
  peano all peano t indeed peano all peano r indeed
  parenthesis
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
  end parenthesis

  peano imply

  peano all peano r indeed
  parenthesis
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
  end parenthesis
end line
line ell p because rule prime mp modus ponens ell o modus ponens ell n indeed
  peano all peano r indeed
  parenthesis
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
  end parenthesis
end line
line ell q because axiom prime a four at peano r indeed

  peano all peano r indeed
  parenthesis
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
  end parenthesis

  peano imply

  parenthesis
    peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
  end parenthesis

end line
line ell r because rule prime mp modus ponens ell q modus ponens ell p indeed
  peano t peano succ peano plus peano r peano is parenthesis peano t peano plus peano r end parenthesis peano succ
end line
line ell big r because lemma prime l three two h swap modus ponens ell r indeed
  peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ
end line
line ell s because lemma prime a one star modus ponens ell big r indeed
  meta h peano imply
  peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ
end line
line ell t because lemma prime a two star modus ponens ell m indeed
    parenthesis
      meta h peano imply
      peano r peano succ peano plus peano t peano is parenthesis peano r peano plus peano t end parenthesis peano succ
    end parenthesis
    peano imply
    parenthesis
      meta h peano imply
      peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t
    end parenthesis
end line
line ell u because rule prime mp modus ponens ell t modus ponens ell s indeed
  meta h peano imply
  peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t
end line
because rule prime gen modus ponens ell u indeed
  peano all peano r indeed
  parenthesis
    meta h peano imply
    peano t peano plus peano r peano succ peano is peano r peano succ peano plus peano t
  end parenthesis
qed 
end math
]"

\section{Conclusion}
We have now successfully proved the lemma:
\begin{center}
"[ math
in theory system prime s
  lemma
    lemma prime l three two h
  says
    peano all peano t indeed peano all peano r indeed
    parenthesis
      peano t peano plus peano r peano is peano r peano plus peano t
    end parenthesis
  end lemma
end math
]"
\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{"[ math pyk define logik rapport as "logik rapport" end define end math ]"}

\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}
End of file
File page.sty
% thebibliography environment from
% /usr/share/texmf/tex/latex/base/book.cls
% with \chapter removed

End of file
latex page
latex page
latex page"