\documentclass [fleqn]{article}

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

\usepackage{url}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 130 490 730}}
\hypersetup{pdftitle=Logiweb sequent calculus - Appendix}
\hypersetup{colorlinks=true}



\begin {document}
\title {Logiweb sequent calculus, Appendix}
\author {Klaus Grue}
\date {\today}
\maketitle
\tableofcontents



\section{Introduction}

The present appendix is part of the {\em Logiweb page} available at

\begin{raggedright}
\begin{sloppypar}
\noindent \url{\lgwCheckUrl body/tex/page.pdf}.
\end{sloppypar}
\end{raggedright}

The hex number which contains a RIPEMD-160 \cite{dobbertin96} hash key and a time stamp identifies the present paper uniquely on Logiweb. The part before the hex number is the address of a {\em Logiweb relay} which redirects the users browser to the paper. That part can be replaced by the address of any Logiweb relay. The part after the hex number indicates the address of the body of the paper relative to the official, binary representation (2/ is shorthand for ../../).

Actually, the present page is rendered as three pdf files present at \href{\lgwCheckUrl body/tex/page.pdf}{2\linebreak [0]/\linebreak [0]body\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]page.pdf}, \href{\lgwCheckUrl body/tex/appendix.pdf}{2\linebreak [0]/\linebreak [0]body\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]appendix.pdf}, and \href{\lgwCheckUrl body/tex/chores.pdf}{2\linebreak [0]/\linebreak [0]body\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]chores.pdf} where appendix.pdf is the present appendix. Many proofs and definitions are deferred to the present appendix to spare the reader of the main paper in the page.pdf file. The chores.pdf file defines how to render each construct in \TeX. A good place to start browsing is \href{\lgwCheckUrl index.html}{2\linebreak [0]/\linebreak [0]index.html}.

Each Logiweb page has a Logiweb bibliography which lists previously published pages which the present page relies on. The present Logiweb page references the \href{\lgwBaseUrl index.html}{base} page at

\begin{raggedright}
\begin{sloppypar}
\noindent \url{\lgwBaseUrl body/tex/page.pdf}.
\end{sloppypar}
\end{raggedright}

\noindent which defines the proof system used to verify the present page (c.f. \href{\lgwCheckUrl bibliography/tex/page.pdf}{2\linebreak [0]/\linebreak [0]bibliography\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]page.pdf}).

As mentioned in the main paper, the user friendliness of the Logiweb sequent calculus is achieved by using the Turing complete macro expansion facility of Logiweb. To see the proofs present in the main paper after macro expansion, consult \href{\lgwCheckUrl expansion/tex/page.pdf}{2\linebreak [0]/\linebreak [0]expansion\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]page.pdf}. To see the proofs of the present appendix after macro expansion, consult \href{\lgwCheckUrl expansion/tex/appendix.pdf}{2\linebreak [0]/\linebreak [0]expansion\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]appendix.pdf}.



\section{Notation}

\subsection{Hiding construct}

$
[
\mathsf{x}
{}^{hide}
\bowtie
\mbox{``}hide
\mbox{''}
]$ proclaims $
\mathsf{x}
{}^{hide}$ to denote hiding. We introduce it here to have a visible hiding construct instead of the invisible `unicode start of text' operator normally used for hiding, c.f.\ the \href{\lgwBaseUrl index.html}{base} page. The use of hiding in $
[
\mathsf{x}
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}_4(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
,
\lceil 
[
\mathsf{x}
\mathrel {\ddot {=}}
\mathsf{y}
]
\rceil 
)
]
{}^{hide}$ later in this appendix is play for the gallery since the $
\mathsf{x}$ is introduced on the \href{\lgwBaseUrl index.html}{base} page and since macro definitions only have effect when they occur on the home page of the construct being macro defined.



\subsection{Metaquantification}\label{section:Metaquantification}

The following macro definition makes e.g.\ $
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {d}}$ expand into $
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {d}}$. Note that $
\forall 
\mathsf{x}
\colon 
\mathsf{y}$ is meta quantification as defined on the \href{\lgwBaseUrl index.html}{base} page which, unfortunately, is rendered exactly like object quantification in the present document. Such notational clashes are unavoidable in mathematics in general but becomes extremely visible in a system like Logiweb where referenced papers are only a click away. To avoid confusion between the two, identically looking quantifiers, we only use the meta quantifier from the base page in the macro definition below and otherwise use $
\forall_{obj} 
\mathsf{x}
\colon 
\mathsf{y}$ to denote object quantification. The $
\mathsf{x}$ operator used in the definition protects against macro expansion. The left hand side of the macro definition is protected against macro expansion as is the `recursive' call of the macro that occurs in the right hand side.

\vspace{1ex}

\noindent $
[
\Pi 
\mathsf{x}
\colon 
\mathsf{y}
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}(
\mathrm {If}(
{\neg }
\mathsf {t}
{}^{1}
\stackrel{r}{=} 
\lceil 
\mathsf{x}
,\linebreak [0] 
\mathsf{y}
\rceil 
,\linebreak [0]
\tilde {{\cal Q}}(
\mathsf {t}
,
\lceil 
\forall 
\mathsf{x}
\colon 
\mathsf{y}
\rceil 
,
\lceil 
\mathsf{x}
\rceil 
\mathrel { : \, : }
\mathsf {t}
{}^{1}
\mathrel { : \, : }
\lceil 
\mathsf{y}
\rceil 
\mathrel { : \, : }
\mathsf {t}
{}^{2}
\mathrel { : \, : }
\mathsf {T}
)
,\linebreak [0]
\tilde {{\cal Q}}(
\mathsf {t}
,
\lceil 
\forall 
\mathsf{x}
\colon 
\Pi 
\mathsf{y}
\colon 
\mathsf{z}
\rceil 
,
\lceil 
\mathsf{x}
\rceil 
\mathrel { : \, : }
\mathsf {t}
{}^{1}
{}^{1}
\mathrel { : \, : }
\lceil 
\mathsf{y}
\rceil 
\mathrel { : \, : }
\mathsf {t}
{}^{1}
{}^{2}
\mathrel { : \, : }
\lceil 
\mathsf{z}
\rceil 
\mathrel { : \, : }
\mathsf {t}
{}^{2}
\mathrel { : \, : }
\mathsf {T}
)
)
,
\mathsf {s}
,
\mathsf {c}
)
]$

\vspace{1ex}

\noindent The definition above is a general macro definition as opposed to more restricted macro definitions like $
[
Arbitrary \gg 
\mathsf {i}
;
\mathsf {p}
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}_4(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
,
\lceil 
[
Arbitrary \gg 
\mathsf {i}
;
\mathsf {p}
\mathrel {\ddot {=}}
\Pi 
\mathsf {i}
\colon 
\mathsf {p}
]
\rceil 
)
]$ which just define a left hand side to expand into a right hand side. The $
[
\mathsf{x}
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}_4(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
,
\lceil 
[
\mathsf{x}
\mathrel {\ddot {=}}
\mathsf{y}
]
\rceil 
)
]
{}^{hide}$ construct itself is defined by a general macro definition and happens to expand into a general macro definition, so the $
[
\mathsf{x}
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}_4(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
,
\lceil 
[
\mathsf{x}
\mathrel {\ddot {=}}
\mathsf{y}
]
\rceil 
)
]
{}^{hide}$ construct is just syntactic sugar.

A general macro definition assigns a `macro' aspect to the principal operator of the right hand side. The definition ignores the parameters of the principal operator. Instead, the right hand side of the general macro definition must take three arguments, $
\mathsf {t}$, $
\mathsf {s}$, and $
\mathsf {c}$. When a macro aspect is invoked, it is applied to the term $
\mathsf {t}$ to be expanded, a `macro state' $
\mathsf {s}$, and a `Logiweb cache' $
\mathsf {c}$.

The macro state should itself be a function of three parameters $
\mathsf {t}$, $
\mathsf {s}$, and $
\mathsf {c}$ and it is the function to be invoked when continuing the macro expansion. A macro like the macro protection macro $
\mathsf{x}$ protects its argument $
\mathsf{x}$ against macro expansion by returning it instead of calling $
\mathsf {s}$ on it. The construct above calls the general macro expansion invokation function $
\tilde {{\cal M}}(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
)$ which simply applies $
\mathsf {s}$ to $
\mathsf {t}$, $
\mathsf {s}$, and $
\mathsf {c}$. So the definition above does something to $
\mathsf {t}$ and then continues macro expansion.

The Logiweb cache $
\mathsf {c}$ is the cache of the home page of $
\mathsf {t}$, i.e.\ the page on which $
\mathsf {t}$ occurs. The cache contains, among other, all definitions present on the home page and all pages transitively referenced by the home page. It also contains other things like compiled versions of all value defined constructs. This is badly needed for efficiency reasons because macro expansion is done not by the Logiweb computing engine itself but by a self-interpretter which is run by the Logiweb engine and simulates the Logiweb engine. This self-interpretter, which resides inside the macro state $
\mathsf {s}$, fetches compiled versions of constructs from the cache $
\mathsf {c}$ for efficiency reasons.

The term $
\mathsf {t}$ has the structure described in Section \ref{section:LogiwebTerms}. $
\mathsf {t}
{}^{2}$ is the second subtree of $
\mathsf {t}$ and $
\mathsf {t}
{}^{1}
{}^{2}$ is the second subtree of the first subtree of $
\mathsf {t}$. $
\mathsf {t}
\stackrel{r}{=} 
\mathsf {t}'$ is true when $
\mathsf {t}$ and $
\mathsf {t}'$ have the same principal operator.

The $
\tilde {{\cal Q}}(
\mathsf {t}
,
\mathsf {p}
,
\mathsf {a}
)$ construct expands the pattern $
\mathsf {p}$ according to the association list $
\mathsf {a}$. Some day, when the author has some spare time, a new version of $
\tilde {{\cal Q}}(
\mathsf {t}
,
\mathsf {p}
,
\mathsf {a}
)$ will be implemented in which the association list is replaced by a facility like the `comma' in Lisp backquotes.

The construct $
\tilde {{\cal Q}}(
\mathsf {t}
,
\mathsf {p}
,
\mathsf {a}
)$ not only expands the pattern $
\mathsf {p}$ according to the association list $
\mathsf {a}$, it also extracts the `debugging information' of the principal operator of $
\mathsf {t}$ and installs that debugging information in all operators that come from the pattern $
\mathsf {p}$. The debugging information indicates the exact location of the construct before macro expansion.

The $
\lceil 
\mathsf {t}
\rceil $ construct evaluates to the Logiweb representation of the term $
\mathsf {t}$.



\subsection{The `Arbitrary' proof constructor}

The `Arbitrary' proof constructor defined on the \href{\lgwBaseUrl index.html}{base} page does not take advantage of the meta quantification macro above. For that reason we introduce a new construct for introducing arbitrary meta variables:

$
[
Arbitrary \gg 
\mathsf {i}
;
\mathsf {p}
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}_4(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
,
\lceil 
[
Arbitrary \gg 
\mathsf {i}
;
\mathsf {p}
\mathrel {\ddot {=}}
\Pi 
\mathsf {i}
\colon 
\mathsf {p}
]
\rceil 
)
]$

Actually, the definition above was used as an example of a simple macro in Section \ref{section:Metaquantification}. When the same aspect of the same construct is defined more than once (e.g.\ the macro aspect of $
\forall 
\mathsf {i}
\colon 
\mathsf {p}$), only the first definition has effect. But the Logiweb compiler prints a warning if the same aspect of the same construct have definitions that contradict each other. The repeated definition of $
\forall 
\mathsf {i}
\colon 
\mathsf {p}$ above gives no warnings since the two definitions have identical right hand sides.



\subsection{Macro indentation}

The following construct increases the left margin. Should be used in inline math mode only. Should be replaced by automatic indentation inside blocks as soon as possible.

$
[
MacroIndent(
\mathsf{x}
)
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}_4(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
,
\lceil 
[
MacroIndent(
\mathsf{x}
)
\mathrel {\ddot {=}}
\mathsf{x}
]
\rceil 
)
]$



\subsection{Protected macro expansion}

The following construct is a general macro definition construct which both protects its left hand side against macro expansion and renders its left hand side using the tex name aspect. To see the definitions of the tex and tex name aspects of $
[
\mathsf{x}
\stackrel{
\mathrm {macro}
}{\rightarrow}
\mathsf{y}
]
{}^{hide}$ consult the \href{\lgwCheckUrl body/tex/chores.pdf}{chores} part of the present Logiweb page.

$
[
[
\mathsf{x}
\stackrel {\circ}{=}
\mathsf{y}
]
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}_4(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
,
\lceil 
[
[
\mathsf{x}
\stackrel {\circ}{=}
\mathsf{y}
]
\mathrel {\ddot {=}}
[(
\mathsf{x}
)^{\mathbf {p}}
\stackrel{
\mathrm {macro}
}{\rightarrow}
\mathsf{y}
]
]
\rceil 
)
]$



\subsection{Object quantification}

The following is a repetion of Section \ref{section:Metaquantification} but concerns object quantification. It allows to write $
\forall_{obj} 
\mathsf{x}
\colon 
\forall_{obj} 
\mathsf{y}
\colon 
\forall_{obj} 
\mathsf{z}
\colon 
\mathsf {u}$ for $
\forall_{obj} 
\mathsf{x}
\colon 
\forall_{obj} 
\mathsf{y}
\colon 
\forall_{obj} 
\mathsf{z}
\colon 
\mathsf {u}$.

\vspace{1ex}

\noindent $
[
\forall 
\mathsf{x}
\colon 
\mathsf{y}
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}(
\mathrm {If}(
{\neg }
\mathsf {t}
{}^{1}
\stackrel{r}{=} 
\lceil 
\mathsf{x}
,\linebreak [0] 
\mathsf{y}
\rceil 
,\linebreak [0]
\tilde {{\cal Q}}(
\mathsf {t}
,
\lceil 
\forall_{obj} 
\mathsf{x}
\colon 
\mathsf{y}
\rceil 
,
\lceil 
\mathsf{x}
\rceil 
\mathrel { : \, : }
\mathsf {t}
{}^{1}
\mathrel { : \, : }
\lceil 
\mathsf{y}
\rceil 
\mathrel { : \, : }
\mathsf {t}
{}^{2}
\mathrel { : \, : }
\mathsf {T}
)
,\linebreak [0]
\tilde {{\cal Q}}(
\mathsf {t}
,
\lceil 
\forall_{obj} 
\mathsf{x}
\colon 
\forall 
\mathsf{y}
\colon 
\mathsf{z}
\rceil 
,
\lceil 
\mathsf{x}
\rceil 
\mathrel { : \, : }
\mathsf {t}
{}^{1}
{}^{1}
\mathrel { : \, : }
\lceil 
\mathsf{y}
\rceil 
\mathrel { : \, : }
\mathsf {t}
{}^{1}
{}^{2}
\mathrel { : \, : }
\lceil 
\mathsf{z}
\rceil 
\mathrel { : \, : }
\mathsf {t}
{}^{2}
\mathrel { : \, : }
\mathsf {T}
)
)
,
\mathsf {s}
,
\mathsf {c}
)
]$



\subsection{Proof constructs}

The $
\mathsf {b}
; 
\mathsf {p}$ construct puts a parenthesis around the block $
\mathsf {b}$ and places a cut operator between $
\mathsf {b}$ and $
\mathsf {p}$. The construct is complicated by the line number $
\mathsf {l}$ which should be macro defined locally to denote the conclusion of the block $
\mathsf {b}$. This is non-trivial since the conclusion is the last line prefixed by all premises, side-conditions, and meta-quantifiers introduced in earlier lines.

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item $
[
Begin \, 
\mathsf {b}
 ; 
\mathsf {l}
 : End ; 
\mathsf {p}
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
Block_1(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
)
]$

\item $
[
Block_1(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf {t}
!
\mathsf {s}
!
\mathsf {c}
!
let_1( 
\lambda 
\mathsf {b}
.
let_1( 
\lambda 
\mathsf{x}
.
let_1( 
\lambda 
\mathsf {q}
.
let_1( 
\lambda 
\mathsf {q}
.
\tilde {{\cal Q}}(
\mathsf {t}
,
\lceil 
\mathsf {b}
; 
\mathsf {q}
\rceil 
,
\lceil 
\mathsf {b}
\rceil 
\mathrel { : \, : }
\mathsf {b}
\mathrel { : \, : }
\lceil 
\mathsf {q}
\rceil 
\mathrel { : \, : }
\mathsf {q}
\mathrel { : \, : }
\mathsf {T}
)
, 
\tilde {{\cal M}}(
\mathsf {q}
,
\mathsf {s}
,
\mathsf {c}
)
)
, 
\tilde {{\cal Q}}(
\mathsf {t}
,
\lceil 
\mathbf{let\ } 
\mathsf {l}
\mathrel{\ddot{=}} 
\mathsf{x}
\mathrel{\ in\ } 
\mathsf {p}
\rceil 
,
\lceil 
\mathsf {l}
\rceil 
\mathrel { : \, : }
\mathsf {t}
{}^{2}
\mathrel { : \, : }
\lceil 
\mathsf {p}
\rceil 
\mathrel { : \, : }
\mathsf {t}
{}^{3}
\mathrel { : \, : }
\lceil 
\mathsf{x}
\rceil 
\mathrel { : \, : }
\mathsf{x}
\mathrel { : \, : }
\mathsf {T}
)
)
, 
Block_2(
\mathsf {b}
)
)
, 
\tilde {{\cal M}}(
\mathsf {t}
{}^{1}
,
\mathsf {s}
,
\mathsf {c}
)
)
]$

\item $
[
Block_2(
\mathsf {b}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathrm {If}(
\mathsf {b}
\stackrel{r}{=} 
\lceil 
\mathsf{x}
\vdash 
\mathsf{y}
\rceil 
,\linebreak [0]
\tilde {{\cal Q}}(
\mathsf {b}
,
\lceil 
\mathsf{x}
\vdash 
\mathsf{y}
\rceil 
,
\lceil 
\mathsf{x}
\rceil 
\mathrel { : \, : }
\mathsf {b}
{}^{1}
\mathrel { : \, : }
\lceil 
\mathsf{y}
\rceil 
\mathrel { : \, : }
Block_2(
\mathsf {b}
{}^{2}
)
\mathrel { : \, : }
\mathsf {T}
)
,\linebreak [0]
\mathrm {If}(
\mathsf {b}
\stackrel{r}{=} 
\lceil 
\mathsf{x}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\mathsf{y}
\rceil 
,\linebreak [0]
\tilde {{\cal Q}}(
\mathsf {b}
,
\lceil 
\mathsf{x}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\mathsf{y}
\rceil 
,
\lceil 
\mathsf{x}
\rceil 
\mathrel { : \, : }
\mathsf {b}
{}^{1}
\mathrel { : \, : }
\lceil 
\mathsf{y}
\rceil 
\mathrel { : \, : }
Block_2(
\mathsf {b}
{}^{2}
)
\mathrel { : \, : }
\mathsf {T}
)
,\linebreak [0]
\mathrm {If}(
\mathsf {b}
\stackrel{r}{=} 
\lceil 
\forall 
\mathsf{x}
\colon 
\mathsf{y}
\rceil 
,\linebreak [0]
\tilde {{\cal Q}}(
\mathsf {b}
,
\lceil 
\forall 
\mathsf{x}
\colon 
\mathsf{y}
\rceil 
,
\lceil 
\mathsf{x}
\rceil 
\mathrel { : \, : }
\mathsf {b}
{}^{1}
\mathrel { : \, : }
\lceil 
\mathsf{y}
\rceil 
\mathrel { : \, : }
Block_2(
\mathsf {b}
{}^{2}
)
\mathrel { : \, : }
\mathsf {T}
)
,\linebreak [0]
\mathrm {If}(
\mathsf {b}
\stackrel{r}{=} 
\lceil 
\mathsf{x}
; 
\mathsf{y}
\rceil 
,\linebreak [0]
Block_2(
\mathsf {b}
{}^{2}
)
,\linebreak [0]
\mathrm {If}(
\mathsf {b}
\stackrel{r}{=} 
\lceil 
\mathsf{x}
\gg 
\mathsf{y}
\rceil 
,\linebreak [0]
\mathsf {b}
{}^{2}
,\linebreak [0]
{\makebox [0mm][l]{$\bot $}\,{\bot }}
)
)
)
)
)
]$

\item $
[
Last\ block\ line \, 
\mathsf {a}
\gg 
\mathsf {i}
\,;
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}_4(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
,
\lceil 
[
Last\ block\ line \, 
\mathsf {a}
\gg 
\mathsf {i}
\,;
\mathrel {\ddot {=}}
(
\mathsf {a}
\gg 
\mathsf {i}
)
]
\rceil 
)
]$

\end{list}



\subsection{Modus ponens at the object level}

We shall apply modus ponens to two arguments so often that this idiom deserves its own macro:

$
[
\mathsf{x}
\unrhd 
\mathsf{y}
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}_4(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
,
\lceil 
[
\mathsf{x}
\unrhd 
\mathsf{y}
\mathrel {\ddot {=}}
MP
\rhd 
\mathsf{x}
\rhd 
\mathsf{y}
]
\rceil 
)
]$



\section{Side conditions}

\subsection{Logiweb terms}\label{section:LogiwebTerms}

Metavariables, object terms, statements, and sequent terms are all implemented as Logiweb terms which essentially have the following syntax:

\newcommand{\literal}[1]{\mbox{``#1''}}
\[\begin{array}{lll}

pdigit & ::= & \literal{1} \mathrel{|} \literal{2} \mathrel{|} \literal{3} \mathrel{|} \literal{4} \mathrel{|} \literal{5} \mathrel{|} \literal{6} \mathrel{|} \literal{7} \mathrel{|} \literal{8} \mathrel{|} \literal{9} \\

digit & ::= & \literal{0} \mathrel{|} pdigit \\

positive & ::= & pdigit \mathrel{|} positive \ digit \\

cardinal & ::= & \literal{0} \mathrel{|} positive \\

reference & ::= & cardinal \\

identifier & ::= & cardinal \\

symbol & ::= & \literal{(} \ reference \literal{\mbox {\tt \char32 }} \ identifier \ \literal{)} \\

arglist & ::= & \literal{)} \mathrel{|} \literal{\mbox {\tt \char32 }} \ term \ arglist \\

term & ::= & \literal{(} \ symbol \ arglist \\

\end{array}\]

\noindent The only thing omitted from the syntax is a third element of symbols which contains debugging information. For details on debugging information, consult the \href{\lgwBaseUrl index.html}{base} page.

Each Logiweb page introduces one or more new constructs. As an example, the present page introduces the binary operation $
\mathsf{x}
\Rightarrow 
\mathsf{y}$.

Each Logiweb page has a unique reference, and each construct introduced by a page has an identifier which is unique within the page. Hence, reference and identifier together determine a construct uniquely.



\subsection{Deduction}

\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}

\item $
[
Ded(
\mathsf {p}
,
\mathsf {c}
)
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}_4(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
,
\lceil 
[
Ded(
\mathsf {p}
,
\mathsf {c}
)
\mathrel {\ddot {=}}
\lambda 
\mathsf{x}
.
Ded_0(
\lceil 
\mathsf {p}
\rceil 
,
\lceil 
\mathsf {c}
\rceil 
)
]
\rceil 
)
]$ \newline True if the premise $
\mathsf {p}$ implies the conclusion $
\mathsf {c}$ according to the deduction rule. The construct quotes its arguments and pass them on to $
Ded_0(
\mathsf {p}
,
\mathsf {c}
)$. The quoting and the $
\lambda 
\mathsf{x}
.\cdots$ makes $
\lambda 
\mathsf{x}
.
Ded_0(
\lceil 
\mathsf {p}
\rceil 
,
\lceil 
\mathsf {c}
\rceil 
)$ suited as a side condition. The present side condition ignores $
\mathsf{x}$. But when a side condition is invoked, it is applied to the cache of the home page of the side condition (the page on which the side condition occurs). That way the side condition gets access to all definitions present on the home page and all pages transitively referenced by the home page. As an example, that has allowed to define an `axiom of definition' in another theory on another Logiweb page in which all value definitions automatically become axiom schemes.

\item $
[
Ded_0(
\mathsf {p}
,
\mathsf {c}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf {c}
!
\mathrm {If}(
Ded_8(
\mathsf {p}
,
\mathsf {T}
)
,\linebreak [0]
Ded_1(
Ded_7(
\mathsf {p}
)
,
\mathsf {c}
,
\mathsf {T}
)
,\linebreak [0]
\mathsf {F}
)
]$ \newline True if the premise $
\mathsf {p}$ implies the conclusion $
\mathsf {c}$ according to the deduction rule. The function checks the premise for meta-closedness, strips meta-quantifiers from $
\mathsf {p}$ and then calls $
Ded_1(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {s}
)$ with an empty list $
\mathsf {s}$ of side conditions. The $
\mathsf{x}
!
\mathsf{y}$ construct evaluates and discards $
\mathsf{x}$ and then returns $
\mathsf{y}$. It is included to ensure strictness of $
Ded_0(
\mathsf {p}
,
\mathsf {c}
)$ which in turn increases the efficiency. Some day the present author will define a `strict value definition' operator so that users don't have to add $
\mathsf{x}
!
\mathsf{y}$ operators manually. The $
\mathsf{x}
!
\mathsf{y}$ construct takes zero CPU-time when used in functions that are `fit' for optimization. See the \href{\lgwBaseUrl index.html}{base} page for details on `fitness' analysis.

\item $
[
Ded_1(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {s}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathrm {If}(
\mathsf {c}
\stackrel{r}{=} 
\lceil 
\mathsf{x}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\mathsf{y}
\rceil 
,\linebreak [0]
Ded_1(
\mathsf {p}
,
\mathsf {c}
{}^{2}
,
\mathsf {c}
{}^{1}
\mathrel { : \, : }
\mathsf {s}
)
,\linebreak [0]
Ded_2(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {s}
)
)
]$ \newline Move side conditions from the conclusion $
\mathsf {c}$ to the list $
\mathsf {s}$. $
\mathsf{x}
\stackrel{r}{=} 
\mathsf{y}$ is true if the terms $
\mathsf{x}$ and $
\mathsf{y}$ have the same root (i.e.\ the same principal operator) so $
\mathsf {c}
\stackrel{r}{=} 
\lceil 
\mathsf{x}
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\mathsf{y}
\rceil $ is true if the principal operator of $
\mathsf {c}$ is an endorsement. $
\mathsf {c}
{}^{1}$ and $
\mathsf {c}
{}^{2}$ are the first and second argument, respectively, of the endorsement.

\item $
[
Ded_2(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {s}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf {s}
!
\mathsf {p}
\stackrel{r}{=} 
\lceil 
\mathsf{x}
\vdash 
\mathsf{y}
\rceil 
\wedge 
\mathsf {c}
\stackrel{r}{=} 
\lceil 
\mathsf{x}
\Rightarrow 
\mathsf{y}
\rceil 
\left\{\protect \begin {array}{l}
Ded_3(
\mathsf {p}
{}^{1}
,
\mathsf {c}
{}^{1}
,
\mathsf {s}
,
\mathsf {T}
)
\wedge 
Ded_2(
\mathsf {p}
{}^{2}
,
\mathsf {c}
{}^{2}
,
\mathsf {s}
)
\\
Ded_4(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {s}
,
Ded_6(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {T}
,
\mathsf {T}
)
)
\protect \end {array}\right.
]$ \newline This function is true if the premise $
\mathsf {p}$ is equal to the conclusion $
\mathsf {c}$ except that inferences are replaced by implications. $
\mathrm {If}(
\mathsf{x}
,\linebreak [0]
\mathsf{y}
,\linebreak [0]
\mathsf{z}
)$ and $
\mathsf{x}
\left\{\protect \begin {array}{l}
\mathsf{y}
\\
\mathsf{z}
\protect \end {array}\right.$ express the same conditional construct. Choosing between the two is a purely stylistic choice.

\item $
[
Ded_3(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {s}
,
\mathsf {b}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathrm {If}(
{\neg }
\mathsf {c}
\stackrel{r}{=} 
\lceil 
\forall_{obj} 
\mathsf{x}
\colon 
\mathsf{y}
\rceil 
,\linebreak [0]
Ded_4(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {s}
,
\mathsf {b}
)
,\linebreak [0]
\mathrm {If}(
\mathsf {p}
\stackrel{r}{=} 
\lceil 
\forall_{obj} 
\mathsf{x}
\colon 
\mathsf{y}
\rceil 
\wedge 
\mathsf {p}
{}^{1}
\stackrel {t}{=}
\mathsf {c}
{}^{1}
,\linebreak [0]
Ded_4(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {s}
,
\mathsf {b}
)
,\linebreak [0]
Ded_3(
\mathsf {p}
,
\mathsf {c}
{}^{2}
,
\mathsf {s}
,
\mathsf {c}
{}^{1}
\mathrel { : \, : }
\mathsf {c}
{}^{1}
\mathrel { : \, : }
\mathsf {b}
)
)
)
]$ \newline $
Ded_3(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {s}
,
\mathsf {b}
)$ moves quantified variables from the premise $
\mathsf {p}$ to the association list $
\mathsf {b}$ of `bindings'. Each quantified variable $
\mathsf{x}$ is added to $
\mathsf {b}$ as the pair $
\mathsf{x}
\mathrel { : \, : }
\mathsf{x}$ indicating the $
\mathsf{x}$ should be replaced by $
\mathsf{x}$ (which is a way of saying that the variable cannot be instantiated). Moving of bound variables stops when there are no more bound variables to move or when the premise and conclusion happen to quantify the same variable. In both cases we have reached a point where premise and conclusion should be identical except for instantaition of variables. $
\mathsf{x}
\stackrel {t}{=}
\mathsf{y}$ is true if the terms $
\mathsf{x}$ and $
\mathsf{y}$ are identical. Logiweb terms contain debugging information which indicates the precise location each operator before macro expansion. $
\mathsf{x}
\stackrel {t}{=}
\mathsf{y}$ ignores this debugging information when it tests two terms for identity.

\item $
[
Ded_4(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {s}
,
\mathsf {b}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf {s}
!
\mathsf {b}
!
\mathrm {If}(
\mathsf {p}
\stackrel{r}{=} 
\lceil \overline{
\mathsf{x}}
\rceil 
,\linebreak [0]
\mathbf {lookup}(
\mathsf {p}
,
\mathsf {b}
,
\mathsf {T}
)
\stackrel {t}{=}
\mathsf {c}
,\linebreak [0]
\mathrm {If}(
{\neg }
\mathsf {p}
\stackrel{r}{=} 
\mathsf {c}
,\linebreak [0]
\mathsf {F}
,\linebreak [0]
\mathrm {If}(
\mathsf {p}
\stackrel{r}{=} 
\lceil 
\forall_{obj} 
\mathsf{x}
\colon 
\mathsf{y}
\rceil 
,\linebreak [0]
\mathsf {p}
{}^{1}
\stackrel {t}{=}
\mathsf {c}
{}^{1}
\wedge 
Ded_4(
\mathsf {p}
{}^{2}
,
\mathsf {c}
{}^{2}
,
\mathsf {s}
,
\mathsf {p}
{}^{1}
\mathrel { : \, : }
\mathsf {p}
{}^{1}
\mathrel { : \, : }
\mathsf {b}
)
,\linebreak [0]
\mathrm {If}(
{\neg }
\mathsf {p}
\stackrel{r}{=} 
\lceil \underline{
\mathsf{x}}
\rceil 
,\linebreak [0]
Ded_4^*(
\mathsf {p}
{}^t
,
\mathsf {c}
{}^t
,
\mathsf {s}
,
\mathsf {b}
)
,\linebreak [0]
\mathsf {p}
{}^{1}
\stackrel {t}{=}
\mathsf {c}
{}^{1}
\wedge 
Ded_5(
\mathsf {p}
,
\mathsf {s}
,
\mathsf {b}
)
)
)
)
)
]$ \newline Test that the premise $
\mathsf {p}$ is identical to the conclusion $
\mathsf {c}$ except for instantiation of object variables as specified by the association list $
\mathsf {b}$. A term is an object variable if the root of the term is the `object variable operator'. For that reason, one can test whether or not a variable is an object variable by comparing its root to the root of an arbitrary object variable. For each meta variable, check that there are side conditions which ensure that the meta variables denote terms whose free object variables do not get caught in the context. Meta variables are recognized the same way as object variables. The object variable $\overline{
\mathsf{x}}$ and the meta variable $\underline{
\mathsf{x}}$ macro expand into $\overline{
\mathsf{x}}$ and $\underline{
\mathsf{x}}$, respectively, adding the object and meta variable operator, respectively, to the term $
\mathsf{x}$. The term $
\mathsf{x}$ is neither an object nor a meta variable. $
\mathsf{x}$ is a Logiweb programming language variable because no Logiweb definition assigns a value to it.

\item $
[
Ded_4^*(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {s}
,
\mathsf {b}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf {c}
!
\mathsf {s}
!
\mathsf {b}
!
\mathrm {If}(
\mathsf {p}
,\linebreak [0]
\mathsf {T}
,\linebreak [0]
Ded_4(
\mathsf {p}
{}^h
,
\mathsf {c}
{}^h
,
\mathsf {s}
,
\mathsf {b}
)
\wedge 
Ded_4^*(
\mathsf {p}
{}^t
,
\mathsf {c}
{}^t
,
\mathsf {s}
,
\mathsf {b}
)
)
]$ \newline Elementwise application of $
Ded_4(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {s}
,
\mathsf {b}
)$. $
\mathsf{x}
{}^h$ and $
\mathsf{x}
{}^t$ denote the head and tail, respectively, of the pair $
\mathsf{x}$. Terms are represented as lists comprising the principal operator followed by arguments just like Lisp S-expressions. The principal operator in turn is a list whose first two elements are cardinals that identify the operator followed by debugging information.

\item $
[
Ded_5(
\mathsf {p}
,
\mathsf {s}
,
\mathsf {b}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf {p}
!
\mathsf {s}
!
\mathrm {If}(
\mathsf {b}
,\linebreak [0]
\mathsf {T}
,\linebreak [0]
\lceil 
\lceil 
\mathsf{x}
\rceil 
\#^0
\lceil 
\mathsf{y}
\rceil 
\rceil 
{}^h
\mathrel { : \, : }
\lceil 
\lceil 
\ast 
\rceil 
\rceil 
{}^h
\mathrel { : \, : }
\mathsf {b}
{}^h
{}^h
\mathrel { : \, : }
\mathsf {T}
\mathrel { : \, : }
\lceil 
\lceil 
\mathsf{x}
\rceil 
\rceil 
{}^h
\mathrel { : \, : }
\mathsf {p}
\mathrel { : \, : }
\mathsf {T}
\mathrel { : \, : }
\mathsf {T}
\in_t 
\mathsf {s}
\wedge 
Ded_5(
\mathsf {p}
,
\mathsf {s}
,
\mathsf {b}
{}^t
)
)
]$ \newline For each variable that is bound in the context according to the association list $
\mathsf {b}$, check that the list $
\mathsf {s}$ of side conditions ensures that the meta variables $
\mathsf {p}$ denotes a term whose free variables do not get caught in the context. $
\mathsf{x}
\in_t 
\mathsf{y}$ is true if the term $
\mathsf{x}$ belongs to the list $
\mathsf{y}$ of terms.

\item $
[
Ded_6(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {e}
,
\mathsf {b}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf {p}
!
\mathsf {c}
!
\mathsf {b}
!
\mathsf {e}
!
\mathrm {If}(
\mathsf {p}
\stackrel{r}{=} 
\lceil \overline{
\mathsf{x}}
\rceil 
,\linebreak [0]
\mathsf {p}
\in_t 
\mathsf {e}
\left\{\protect \begin {array}{l}
\mathsf {b}
\\
\mathsf {p}
\mathrel { : \, : }
\mathsf {c}
\mathrel { : \, : }
\mathsf {b}
\protect \end {array}\right.
,\linebreak [0]
\mathrm {If}(
{\neg }
\mathsf {p}
\stackrel{r}{=} 
\mathsf {c}
,\linebreak [0]
\mathsf {T}
,\linebreak [0]
\mathrm {If}(
\mathsf {p}
\stackrel{r}{=} 
\lceil \underline{
\mathsf {a}}
\rceil 
,\linebreak [0]
\mathsf {b}
,\linebreak [0]
\mathrm {If}(
\mathsf {p}
\stackrel{r}{=} 
\lceil 
\forall_{obj} 
\mathsf{x}
\colon 
\mathsf{y}
\rceil 
,\linebreak [0]
Ded_6(
\mathsf {p}
{}^{2}
,
\mathsf {c}
{}^{2}
,
\mathsf {c}
{}^{1}
\mathrel { : \, : }
\mathsf {e}
,
\mathsf {b}
)
,\linebreak [0]
Ded_6^*(
\mathsf {p}
{}^t
,
\mathsf {c}
{}^t
,
\mathsf {e}
,
\mathsf {b}
)
)
)
)
)
]$

\item $
[
Ded_6^*(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {e}
,
\mathsf {b}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf {p}
!
\mathsf {c}
!
\mathsf {b}
!
\mathsf {e}
!
\mathrm {If}(
\mathsf {p}
,\linebreak [0]
\mathsf {b}
,\linebreak [0]
Ded_6^*(
\mathsf {p}
{}^t
,
\mathsf {c}
{}^t
,
\mathsf {e}
,
Ded_6(
\mathsf {p}
{}^h
,
\mathsf {c}
{}^h
,
\mathsf {e}
,
\mathsf {b}
)
)
)
]$ \newline Elementwise application of $
Ded_6(
\mathsf {p}
,
\mathsf {c}
,
\mathsf {e}
,
\mathsf {b}
)$.

\item $
[
Ded_7(
\mathsf {p}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf {p}
\stackrel{r}{=} 
\lceil 
\forall 
\mathsf{x}
\colon 
\mathsf{y}
\rceil 
\left\{\protect \begin {array}{l}
Ded_7(
\mathsf {p}
{}^{2}
)
\\
\mathsf {p}
\protect \end {array}\right.
]$ \newline Removal of all metaquantifiers.

\item $
[
Ded_8(
\mathsf {p}
,
\mathsf {b}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathrm {If}(
\mathsf {p}
\stackrel{r}{=} 
\lceil 
\forall 
\mathsf{x}
\colon 
\mathsf{y}
\rceil 
,\linebreak [0]
Ded_8(
\mathsf {p}
{}^{2}
,
\mathsf {p}
{}^{1}
\mathrel { : \, : }
\mathsf {b}
)
,\linebreak [0]
\mathrm {If}(
\mathsf {p}
\stackrel{r}{=} 
\lceil \underline{
\mathsf {a}}
\rceil 
,\linebreak [0]
\mathsf {p}
\in_t 
\mathsf {b}
,\linebreak [0]
Ded_8^*(
\mathsf {p}
{}^t
,
\mathsf {b}
)
)
)
]$ \newline True if all free meta variables of $
\mathsf {p}$ occur in the list $
\mathsf {b}$ of meta variables.

\item $
[
Ded_8^*(
\mathsf {p}
,
\mathsf {b}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf {b}
!
\mathrm {If}(
\mathsf {p}
,\linebreak [0]
\mathsf {T}
,\linebreak [0]
\mathrm {If}(
Ded_8(
\mathsf {p}
{}^h
,
\mathsf {b}
)
,\linebreak [0]
Ded_8^*(
\mathsf {p}
{}^t
,
\mathsf {b}
)
,\linebreak [0]
\mathsf {F}
)
)
]$ \newline Elementwise application of $
Ded_8(
\mathsf {p}
,
\mathsf {b}
)$.

\end{list}



\subsection{Avoidance}

\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}

\item $
[
\mathsf{x}
{}^{var}
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf{x}
\stackrel{r}{=} 
\lceil \overline{
\mathsf{x}}
\rceil 
]$

\item $
[
\mathsf{x}
\#
\mathsf{y}
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}_4(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
,
\lceil 
[
\mathsf{x}
\#
\mathsf{y}
\mathrel {\ddot {=}}
\lceil 
\mathsf{x}
\rceil 
\#^0
\lceil 
\mathsf{y}
\rceil 
]
\rceil 
)
]$

\item $
[
\mathsf{x}
\#^0
\mathsf{y}
\stackrel{
\mathrm {val}
}{\rightarrow}
\lambda 
\mathsf {c}
.
\mathsf{x}
{}^{var}
\wedge 
\mathsf{y}
{} ^ {\cal C}
\wedge 
\mathsf{x}
\#^1
\mathsf{y}
]$

\item $
[
\mathsf{x}
\#^1
\mathsf{y}
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathrm {If}(
\mathsf{y}
{}^{var}
,\linebreak [0]
{\neg }
\mathsf{x}
\stackrel {t}{=}
\mathsf{y}
,\linebreak [0]
\newline 
\mathrm {If}(
{\neg }
\mathsf{y}
\stackrel{r}{=} 
\lceil 
\forall_{obj} 
\mathsf{x}
\colon 
\mathsf{y}
\rceil 
,\linebreak [0]
\mathsf{x}
\#^*
\mathsf{y}
{}^t
,\linebreak [0]
\newline 
\mathrm {If}(
\mathsf{x}
\stackrel {t}{=}
\mathsf{y}
{}^{1}
,\linebreak [0]
\mathsf {T}
,\linebreak [0]
\mathsf{x}
\#^1
\mathsf{y}
{}^{2}
)
)
)
]$

\item $
[
\mathsf{x}
\#^*
\mathsf{y}
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf{x}
!
\mathrm {If}(
\mathsf{y}
,\linebreak [0]
\mathsf {T}
,\linebreak [0]
\mathrm {If}(
\mathsf{x}
\#^1
\mathsf{y}
{}^h
,\linebreak [0]
\mathsf{x}
\#^*
\mathsf{y}
{}^t
,\linebreak [0]
\mathsf {F}
)
)
]$

\end{list}



\subsection{Substition}

\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}

\item $
[
\langle 
\mathsf {a}
{\equiv} 
\mathsf {b}
| 
\mathsf{x}
{:=} 
\mathsf {t}
\rangle 
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.
\tilde {{\cal M}}_4(
\mathsf {t}
,
\mathsf {s}
,
\mathsf {c}
,
\lceil 
[
\langle 
\mathsf {a}
{\equiv} 
\mathsf {b}
| 
\mathsf{x}
{:=} 
\mathsf {t}
\rangle 
\mathrel {\ddot {=}}
\langle 
\lceil 
\mathsf {a}
\rceil 
{\equiv}^0 
\lceil 
\mathsf {b}
\rceil 
| 
\lceil 
\mathsf{x}
\rceil 
{:=} 
\lceil 
\mathsf {t}
\rceil 
\rangle 
]
\rceil 
)
]$

\item $
[
\langle 
\mathsf {a}
{\equiv}^0 
\mathsf {b}
| 
\mathsf{x}
{:=} 
\mathsf {t}
\rangle 
\stackrel{
\mathrm {val}
}{\rightarrow}
\lambda 
\mathsf {c}
.
\mathsf{x}
{}^{var}
\wedge 
\langle 
\mathsf {a}
{\equiv}^1 
\mathsf {b}
| 
\mathsf{x}
{:=} 
\mathsf {t}
\rangle 
]$

\item $
[
\langle 
\mathsf {a}
{\equiv}^1 
\mathsf {b}
| 
\mathsf{x}
{:=} 
\mathsf {t}
\rangle 
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf {a}
!
\mathsf{x}
!
\mathsf {t}
!
\newline 
\mathrm {If}(
\mathrm {If}(
\mathsf {b}
\stackrel{r}{=} 
\lceil 
\forall_{obj} 
\mathsf {u}
\colon 
\mathsf {v}
\rceil 
,\linebreak [0]
\mathsf {b}
{}^{1}
\stackrel {t}{=}
\mathsf{x}
,\linebreak [0]
\mathsf {F}
)
,\linebreak [0]
\mathsf {a}
\stackrel {t}{=}
\mathsf {b}
,\linebreak [0]
\newline 
\mathrm {If}(
\mathsf {b}
{}^{var}
\wedge 
\mathsf {b}
\stackrel {t}{=}
\mathsf{x}
,\linebreak [0]
\mathsf {a}
\stackrel {t}{=}
\mathsf {t}
,\linebreak [0]
\mathrm {If}(
\newline 
\mathsf {a}
\stackrel{r}{=} 
\mathsf {b}
,\linebreak [0]
\langle 
\mathsf {a}
{}^t
{\equiv}^* 
\mathsf {b}
{}^t
| 
\mathsf{x}
{:=} 
\mathsf {t}
\rangle 
,\linebreak [0]
\mathsf {F}
)
)
)
]$

\item $
[
\langle 
\mathsf {a}
{\equiv}^* 
\mathsf {b}
| 
\mathsf{x}
{:=} 
\mathsf {t}
\rangle 
\stackrel{
\mathrm {val}
}{\rightarrow}
\mathsf {b}
!
\mathsf{x}
!
\mathsf {t}
!
\mathrm {If}(
\mathsf {a}
,\linebreak [0]
\mathsf {T}
,\linebreak [0]
\mathrm {If}(
\langle 
\mathsf {a}
{}^h
{\equiv}^1 
\mathsf {b}
{}^h
| 
\mathsf{x}
{:=} 
\mathsf {t}
\rangle 
,\linebreak [0]
\langle 
\mathsf {a}
{}^t
{\equiv}^* 
\mathsf {b}
{}^t
| 
\mathsf{x}
{:=} 
\mathsf {t}
\rangle 
,\linebreak [0]
\mathsf {F}
)
)
]$

\end{list}



\section{Proofs}

\subsection{Proofs of FOL axioms using the inference of deduction}

We now prove axiom schemes A1 and A2 from \cite{mendelson}. Furthermore, we prove two, particular instances of A4 and A5 in a way that generalizes to arbitrary instances of those axiom schemes.

Furthermore, we prove a $
Repetition$ lemma which says $
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {a}}$ by a `hand made proof', i.e.\ by giving a proof metatactic explicitly which generates the sequent proof.

A page is verified by a top level verifier. The top level verifier of the present page is defined on the \href{\lgwBaseUrl index.html}{base} page. That verifier invokes, among other, a proof verifier. The proof verifier invokes each proof (where each proof is supposed to be a proof metatactic). When it does so, it applies the proof metatactic to a Logiweb cache $
\mathsf {c}$ and a pair $
\mathsf {n}
\mathrel { : \, : }
\mathsf {l}$. The cache $
\mathsf {c}$ is the Logiweb cache of the home page of the proof, i.e.\ a structure which contains all definitions present on the home page plus all transitively referenced Logiweb pages. $
\mathsf {n}$ is the identifier of the lemma (a cardinal which identifies the lemma uniquely within the home page) plus the contents of the lemma. The proof metatactic given below for proving $
Repetition$ ignores both arguments and just constructs a sequent term that proves $
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {a}}$. All other proofs in the present paper macro expand into proofs that are proved by a metatactic which scans the proof for object tactics and invokes those object tactics. The only object tactic used is named $\gg$ and does unification.

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}}

\item $
[
Repetition
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {a}}
]$

\item $
[
A1'
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
]$

\item $
[
A2'
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {c}}
]$

\item $
[
A4'
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall_{obj} \overline{
\mathsf{x}}
\colon 
\forall_{obj} \overline{
\mathsf{y}}
\colon \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}
\Rightarrow 
2
+ 
3
= 
3
+ 
2
]$

\item $
[
A5'
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall_{obj} \overline{
\mathsf{x}}
\colon 
2
+ 
3
= 
5
\Rightarrow 
2
+ 
3
+ \overline{
\mathsf{x}}
= 
5
+ \overline{
\mathsf{x}}
\Rightarrow 
2
+ 
3
= 
5
\Rightarrow 
\forall_{obj} \overline{
\mathsf{x}}
\colon 
2
+ 
3
+ \overline{
\mathsf{x}}
= 
5
+ \overline{
\mathsf{x}}
]$

\end{list}

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item $
[
Repetition
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
\lceil 
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
{} ^ { I }
\rceil 
]$

\item $
[
A1'
\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 {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
\vdash 
Repetition
\rhd \underline{
\mathsf {a}}
\gg \underline{
\mathsf {a}}
; 
Ded
\rhd 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\gg \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\item $
[
A2'
\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 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\vdash 
MP
\rhd \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\rhd \underline{
\mathsf {a}}
\gg \underline{
\mathsf {b}}
; 
MP
\rhd \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {c}}
\rhd \underline{
\mathsf {a}}
\gg \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {c}}
; 
MP
\rhd \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {c}}
\rhd \underline{
\mathsf {b}}
\gg \underline{
\mathsf {c}}
; 
Ded
\rhd 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {c}}
\gg \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {c}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\item $
[
A4'
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}
\vdash 
Repetition
\rhd \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}
\gg \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}
; 
Ded
\rhd \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}
\vdash \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}
\gg 
\forall_{obj} \overline{
\mathsf{x}}
\colon 
\forall_{obj} \overline{
\mathsf{y}}
\colon \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}
\Rightarrow 
2
+ 
3
= 
3
+ 
2
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\item $
[
A5'
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
2
+ 
3
= 
5
\Rightarrow 
2
+ 
3
+ \overline{
\mathsf{x}}
= 
5
+ \overline{
\mathsf{x}}
\vdash 
2
+ 
3
= 
5
\vdash 
MP
\rhd 
2
+ 
3
= 
5
\Rightarrow 
2
+ 
3
+ \overline{
\mathsf{x}}
= 
5
+ \overline{
\mathsf{x}}
\rhd 
2
+ 
3
= 
5
\gg 
2
+ 
3
+ \overline{
\mathsf{x}}
= 
5
+ \overline{
\mathsf{x}}
; 
Gen
\rhd 
2
+ 
3
+ \overline{
\mathsf{x}}
= 
5
+ \overline{
\mathsf{x}}
\gg 
\forall_{obj} \overline{
\mathsf{x}}
\colon 
2
+ 
3
+ \overline{
\mathsf{x}}
= 
5
+ \overline{
\mathsf{x}}
; 
Ded
\rhd 
2
+ 
3
= 
5
\Rightarrow 
2
+ 
3
+ \overline{
\mathsf{x}}
= 
5
+ \overline{
\mathsf{x}}
\vdash 
2
+ 
3
= 
5
\vdash 
\forall_{obj} \overline{
\mathsf{x}}
\colon 
2
+ 
3
+ \overline{
\mathsf{x}}
= 
5
+ \overline{
\mathsf{x}}
\gg 
\forall_{obj} \overline{
\mathsf{x}}
\colon 
2
+ 
3
= 
5
\Rightarrow 
2
+ 
3
+ \overline{
\mathsf{x}}
= 
5
+ \overline{
\mathsf{x}}
\Rightarrow 
2
+ 
3
= 
5
\Rightarrow 
\forall_{obj} \overline{
\mathsf{x}}
\colon 
2
+ 
3
+ \overline{
\mathsf{x}}
= 
5
+ \overline{
\mathsf{x}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\end{list}



\subsection{A proof of $
\mathsf{x}
+ 
\mathsf{y}
= 
\mathsf{y}
+ 
\mathsf{x}$}

\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}

\item $
[
Prop\ 3.2a
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.2b
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.2c
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
]$

\item $
[
Prop\ 3.2d
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
]$

\item $
[
Prop\ 3.2e
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
]$

\item $
[
Prop\ 3.2f
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.2g
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
]$

\item $
[
Prop\ 3.2h
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
]$

\end{list}



\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item $
[
Prop\ 3.2a
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
S5
\gg \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
; 
S1
\rhd \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
\rhd \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
\gg \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2b
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash 
Prop\ 3.2a
\gg \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
; 
S1
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\gg \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2c
\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}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\vdash 
Prop\ 3.2b
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\gg \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
; 
S1
\rhd \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
\rhd \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\gg \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2d
\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}}
= \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\vdash 
Prop\ 3.2b
\rhd \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\gg \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
; 
Prop\ 3.2c
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\rhd \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2e_1
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {b}}
+ 
0
]$



\item $
[
Prop\ 3.2e_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 {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash 
S5
\gg \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
; 
Prop\ 3.2c
\rhd \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {b}}
; 
S5
\gg \underline{
\mathsf {b}}
+ 
0
= \underline{
\mathsf {b}}
; 
Prop\ 3.2d
\rhd \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {b}}
\rhd \underline{
\mathsf {b}}
+ 
0
= \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {b}}
+ 
0
; 
Ded
\rhd 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {b}}
+ 
0
\gg \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {b}}
+ 
0
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2e_2
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
]$



\item $
[
Prop\ 3.2e_2
\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 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash 
MP
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
; 
S2
\rhd \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
; 
S6
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
{}'
; 
Prop\ 3.2c
\rhd \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
{}'
\rhd \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
; 
S6
\gg \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
; 
Prop\ 3.2d
\rhd \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
\rhd \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
; 
Ded
\rhd 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
\gg \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2e
\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}}
= \underline{
\mathsf {b}}
\vdash 
Prop\ 3.2e_1
\gg \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
+ 
0
= \overline{
\mathsf{y}}
+ 
0
; 
Prop\ 3.2e_2
\gg \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
+ \overline{
\mathsf{z}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{z}}
\Rightarrow \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
+ \overline{
\mathsf{z}}
{}'
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{z}}
{}'
; 
S9
\mathop {\char64} \overline{
\mathsf{z}}
\rhd \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
+ 
0
= \overline{
\mathsf{y}}
+ 
0
\rhd \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
+ \overline{
\mathsf{z}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{z}}
\Rightarrow \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
+ \overline{
\mathsf{z}}
{}'
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{z}}
{}'
\gg \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
+ \overline{
\mathsf{z}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{z}}
; 
Ded
\rhd \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
+ \overline{
\mathsf{z}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{z}}
\gg \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
; 
MP
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2f_1
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
0
= 
0
+ 
0
]$



\item $
[
Prop\ 3.2f_1
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
S5
\gg 
0
+ 
0
= 
0
; 
Prop\ 3.2b
\rhd 
0
+ 
0
= 
0
\gg 
0
= 
0
+ 
0
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2f_2
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
]$



\item $
[
Prop\ 3.2f_2
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
\vdash 
S2
\rhd \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
\gg \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
; 
S6
\gg 
0
+ \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
; 
Prop\ 3.2d
\rhd \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
\rhd 
0
+ \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
\gg \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
; 
Ded
\rhd 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
\gg \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
{}'
= 
0
+ \underline{
\mathsf {a}}
{}'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2f
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
Prop\ 3.2f_1
\gg 
0
= 
0
+ 
0
; 
Prop\ 3.2f_2
\gg \overline{
\mathsf{x}}
= 
0
+ \overline{
\mathsf{x}}
\Rightarrow \overline{
\mathsf{x}}
{}'
= 
0
+ \overline{
\mathsf{x}}
{}'
; 
S9
\mathop {\char64} \overline{
\mathsf{x}}
\rhd 
0
= 
0
+ 
0
\rhd \overline{
\mathsf{x}}
= 
0
+ \overline{
\mathsf{x}}
\Rightarrow \overline{
\mathsf{x}}
{}'
= 
0
+ \overline{
\mathsf{x}}
{}'
\gg \overline{
\mathsf{x}}
= 
0
+ \overline{
\mathsf{x}}
; 
Ded
\rhd \overline{
\mathsf{x}}
= 
0
+ \overline{
\mathsf{x}}
\gg \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2g_1
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
{}'
+ 
0
= \underline{
\mathsf {a}}
+ 
0
{}'
]$



\item $
[
Prop\ 3.2g_1
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
S5
\gg \underline{
\mathsf {a}}
{}'
+ 
0
= \underline{
\mathsf {a}}
{}'
; 
S5
\gg \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
; 
S2
\rhd \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
\gg \underline{
\mathsf {a}}
+ 
0
{}'
= \underline{
\mathsf {a}}
{}'
; 
Prop\ 3.2d
\rhd \underline{
\mathsf {a}}
{}'
+ 
0
= \underline{
\mathsf {a}}
{}'
\rhd \underline{
\mathsf {a}}
+ 
0
{}'
= \underline{
\mathsf {a}}
{}'
\gg \underline{
\mathsf {a}}
{}'
+ 
0
= \underline{
\mathsf {a}}
+ 
0
{}'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2g_2
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
\Rightarrow \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
{}'
]$



\item $
[
Prop\ 3.2g_2
\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 {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
\vdash 
S2
\rhd \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
\gg \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
{}'
; 
S6
\gg \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
{}'
; 
Prop\ 3.2c
\rhd \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
{}'
\rhd \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
{}'
\gg \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
{}'
; 
S6
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
; 
S2
\rhd \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
{}'
; 
Prop\ 3.2d
\rhd \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
{}'
\rhd \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
{}'
\gg \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
{}'
; 
Ded
\rhd 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
\vdash \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
{}'
\gg \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
\Rightarrow \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
{}'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2g
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
Prop\ 3.2g_1
\gg \overline{
\mathsf{x}}
{}'
+ 
0
= \overline{
\mathsf{x}}
+ 
0
{}'
; 
Prop\ 3.2g_2
\gg \overline{
\mathsf{x}}
{}'
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
{}'
\Rightarrow \overline{
\mathsf{x}}
{}'
+ \overline{
\mathsf{y}}
{}'
= \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
{}'
{}'
; 
S9
\mathop {\char64} \overline{
\mathsf{y}}
\rhd \overline{
\mathsf{x}}
{}'
+ 
0
= \overline{
\mathsf{x}}
+ 
0
{}'
\rhd \overline{
\mathsf{x}}
{}'
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
{}'
\Rightarrow \overline{
\mathsf{x}}
{}'
+ \overline{
\mathsf{y}}
{}'
= \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
{}'
{}'
\gg \overline{
\mathsf{x}}
{}'
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
{}'
; 
Ded
\rhd \overline{
\mathsf{x}}
{}'
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
{}'
\gg \underline{
\mathsf {a}}
{}'
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2h_1
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
+ 
0
= 
0
+ \underline{
\mathsf {a}}
]$



\item $
[
Prop\ 3.2h_1
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
S5
\gg \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
; 
Prop\ 3.2f
\gg \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
; 
Prop\ 3.2c
\rhd \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
\rhd \underline{
\mathsf {a}}
= 
0
+ \underline{
\mathsf {a}}
\gg \underline{
\mathsf {a}}
+ 
0
= 
0
+ \underline{
\mathsf {a}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2h_2
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {b}}
{}'
+ \underline{
\mathsf {a}}
]$



\item $
[
Prop\ 3.2h_2
\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 {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\vdash 
S2
\rhd \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
{}'
; 
S6
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
; 
Prop\ 3.2c
\rhd \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
\rhd \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
{}'
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
{}'
; 
Prop\ 3.2g
\gg \underline{
\mathsf {b}}
{}'
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
{}'
; 
Prop\ 3.2d
\rhd \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
{}'
\rhd \underline{
\mathsf {b}}
{}'
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
{}'
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {b}}
{}'
+ \underline{
\mathsf {a}}
; 
Ded
\rhd 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {b}}
{}'
+ \underline{
\mathsf {a}}
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {b}}
{}'
+ \underline{
\mathsf {a}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



\item $
[
Prop\ 3.2h
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
Prop\ 3.2h_1
\gg \overline{
\mathsf{x}}
+ 
0
= 
0
+ \overline{
\mathsf{x}}
; 
Prop\ 3.2h_2
\gg \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}
\Rightarrow \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
{}'
= \overline{
\mathsf{y}}
{}'
+ \overline{
\mathsf{x}}
; 
S9
\mathop {\char64} \overline{
\mathsf{y}}
\rhd \overline{
\mathsf{x}}
+ 
0
= 
0
+ \overline{
\mathsf{x}}
\rhd \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}
\Rightarrow \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
{}'
= \overline{
\mathsf{y}}
{}'
+ \overline{
\mathsf{x}}
\gg \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}
; 
Ded
\rhd \overline{
\mathsf{x}}
+ \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{x}}
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\end{list}



%------------------------------------------------------------------------------
\bibliographystyle{alpha}
\bibliography{./page}
%------------------------------------------------------------------------------
\everymath{}
\everydisplay{}

\end{document}
