\documentclass [fleqn]{article}

\everymath{\rm}
\everydisplay{\rm}
\usepackage{latexsym}
\setlength {\overfullrule }{0mm}
\input{lgwinclude}
\usepackage[danish]{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{url}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle=Logiweb sequent calculus}
\hypersetup{colorlinks=true}

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

\newcommand{\liberalUrlBreak}[1]{{%
\mathcode`\/="202F%
\mathcode`\0="2030%
\mathcode`\1="2031%
\mathcode`\2="2032%
\mathcode`\3="2033%
\mathcode`\4="2034%
\mathcode`\5="2035%
\mathcode`\6="2036%
\mathcode`\7="2037%
\mathcode`\8="2038%
\mathcode`\9="2039%
\mathcode`\:="203A%
\mathcode`\A="2041%
\mathcode`\B="2042%
\mathcode`\C="2043%
\mathcode`\D="2044%
\mathcode`\E="2045%
\mathcode`\F="2046%
%\thinmuskip=0mu%
\medmuskip=0mu plus 2mu minus 0mu%
%\thickmuskip=0mu%
%\def\thinspace{\kern 0em}%
$#1$}}

\begin {document}
\title {projekt i logik}
\author {Maja Hanne T\o nnesen, Rune Christoffer Kildetoft Andresen \\ \& Niels Peter Meyn Milthers}
\date {\today}
\maketitle
\tableofcontents


\raggedright



\begin{abstract}

\end{abstract}




\section{Introduction}\label{sec:Introduction}
In this paper we will prove the propositions regarding $
S$ starting with proposition $
Prop\ 3.2i$ in mendelson \cite{mendelson}. Continuing to$
Prop\ 3.4$ defining numerals neded to  prove $
Prop\ 3.5$ .
then we will define rules regarding $
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}$ needed to prove $
Prop\ 3.7$ .
after that we will define  $
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }\overline{
\mathsf{y}}
= \overline{
\mathsf{x}}
\cdot 
\mathsf{z}$ nedded to prove $
Prop\ 3.10$ , and
finally we will prove $
Prop\ 3.11$.




\section{Proof of $
Prop\ 3.2$ }


A modified version of Mendelsons system $
S$ (Peano arithmetic) \cite{mendelson} may be formulated thus:

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

\item \makebox[0.45\textwidth][l]{$
[
S
\stackrel{
stmt
}{\rightarrow}
\mathsf{x}
]$}$
[
MP
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
]
[
MP
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item \makebox[0.45\textwidth][l]{$
[
Gen
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\vdash 
\forall_{obj} \underline{
\mathsf{x}}
\colon \underline{
\mathsf {a}}
]
[
Gen
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}$
[
Ded
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\lambda 
\mathsf{x}
.
Ded_0(
\lceil \underline{
\mathsf {a}}
\rceil 
,
\lceil \underline{
\mathsf {b}}
\rceil 
)
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
]
[
Ded
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item \makebox[0.45\textwidth][l]{}$
[
S2
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
{}'
= \underline{
\mathsf {b}}
{}'
]
[
S2
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item \makebox[0.45\textwidth][l]{$
[
S3
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
0
= \underline{
\mathsf {a}}
{}'
]
[
S3
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}$
[
S4
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
{}'
= \underline{
\mathsf {b}}
{}'
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
]
[
S4
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item \makebox[0.45\textwidth][l]{$
[
S5
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {a}}
]
[
S5
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}$
[
S6
\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}}
{}'
]
[
S6
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item \makebox[0.45\textwidth][l]{$
[
S7
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\cdot 
0
= 
0
]
[
S7
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$}$
[
S8
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
]
[
S8
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
Neg
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }\underline{
\mathsf {b}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\vdash 
{\neg }\underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
]
[
Neg
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
S1
\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}}
\vdash \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
]
[
S1
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$

\item $
[
S9
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf{x}}
\colon 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
\langle 
\lceil \underline{
\mathsf {b}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {a}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil 
0
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\langle 
\lceil \underline{
\mathsf {c}}
\rceil 
{\equiv}^0 
\lceil \underline{
\mathsf {a}}
\rceil 
| 
\lceil \underline{
\mathsf{x}}
\rceil 
{:=} 
\lceil \underline{
\mathsf{x}}
{}'
\rceil 
\rangle 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
]
[
S9
\stackrel{
proof
}{\rightarrow}
Rule\ tactic
]$


\end{list}

Mendelson \cite{mendelson} defines a set of lemma's 

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

These Lemma's are proved in \cite{check}, and we will continue to prove the following lemma's, from Mendelson \cite{mendelson}.

\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\item $
[
Prop\ 3.2i
\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 {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
+ \underline{
\mathsf {b}}
]$

\item $
[
Prop\ 3.2j
\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}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
]$

\item $
[
Prop\ 3.2k
\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}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
]$

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

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

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

\item $
[
Prop\ 3.2o
\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 {c}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
]$

\end{list}


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

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

\end{list}


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

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

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

\item $
[
Prop\ 3.2j_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}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
]$

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

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

\end{list}



\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item $
[
Prop\ 3.2k_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}}
\cdot 
0
= \underline{
\mathsf {b}}
\cdot 
0
]$

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

\item $
[
Prop\ 3.2k_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}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
{}'
]$ 

\item $
[
Prop\ 3.2k_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}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash 
MP
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
; 
S8
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
; 
S8
\gg \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {b}}
; 
Prop\ 3.2e
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
; 
Prop\ 3.2i
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\gg \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {b}}
; 
Prop\ 3.2c
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
\rhd \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {b}}
; 
Prop\ 3.2c
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {b}}
; 
Prop\ 3.2d
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {b}}
\rhd \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
\cdot \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}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
{}'
\gg \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
{}'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\item $
[
Prop\ 3.2k
\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.2k_1
\gg \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
\cdot 
0
= \overline{
\mathsf{y}}
\cdot 
0
; 
Prop\ 3.2k_2
\gg \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{z}}
= \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
\Rightarrow \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{z}}
{}'
= \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
{}'
; 
S9
\mathop {\char64} \overline{
\mathsf{z}}
\rhd \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
\cdot 
0
= \overline{
\mathsf{y}}
\cdot 
0
\rhd \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{z}}
= \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
\Rightarrow \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{z}}
{}'
= \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
{}'
\gg \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{z}}
= \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
; 
Ded
\rhd \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{z}}
= \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
\gg \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
; 
MP
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\end{list}



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


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

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

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

\end{list}



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

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

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

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

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

\item $
[
Prop\ 3.2m
\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.2m_1
\gg \overline{
\mathsf{x}}
{}'
\cdot 
0
= \overline{
\mathsf{x}}
\cdot 
0
+ 
0
; 
Prop\ 3.2m_2
\gg \overline{
\mathsf{x}}
{}'
\cdot \overline{
\mathsf{y}}
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
+ \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
{}'
\cdot \overline{
\mathsf{y}}
{}'
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
{}'
+ \overline{
\mathsf{y}}
{}'
; 
S9
\mathop {\char64} \overline{
\mathsf{y}}
\rhd \overline{
\mathsf{x}}
{}'
\cdot 
0
= \overline{
\mathsf{x}}
\cdot 
0
+ 
0
\rhd \overline{
\mathsf{x}}
{}'
\cdot \overline{
\mathsf{y}}
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
+ \overline{
\mathsf{y}}
\Rightarrow \overline{
\mathsf{x}}
{}'
\cdot \overline{
\mathsf{y}}
{}'
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
{}'
+ \overline{
\mathsf{y}}
{}'
\gg \overline{
\mathsf{x}}
{}'
\cdot \overline{
\mathsf{y}}
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
+ \overline{
\mathsf{y}}
; 
Ded
\rhd \overline{
\mathsf{x}}
{}'
\cdot \overline{
\mathsf{y}}
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
+ \overline{
\mathsf{y}}
\gg \underline{
\mathsf {a}}
{}'
\cdot \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {b}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\end{list}



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

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

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

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

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

\item $
[
Prop\ 3.2n
\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.2n_1
\gg \overline{
\mathsf{x}}
\cdot 
0
= 
0
\cdot \overline{
\mathsf{x}}
; 
Prop\ 3.2n_2
\gg \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{x}}
\Rightarrow \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
{}'
= \overline{
\mathsf{y}}
{}'
\cdot \overline{
\mathsf{x}}
; 
S9
\mathop {\char64} \overline{
\mathsf{y}}
\rhd \overline{
\mathsf{x}}
\cdot 
0
= 
0
\cdot \overline{
\mathsf{x}}
\rhd \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{x}}
\Rightarrow \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
{}'
= \overline{
\mathsf{y}}
{}'
\cdot \overline{
\mathsf{x}}
\gg \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{x}}
; 
Ded
\rhd \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{x}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {a}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\end{list}



\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item $
[
Prop\ 3.2o
\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 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash 
Prop\ 3.2k
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
; 
Prop\ 3.2n
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
; 
Prop\ 3.2n
\gg \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
; 
Prop\ 3.2c
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\rhd \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
; 
S1
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
\gg \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
; 
Ded
\rhd 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
; 
MP
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
\rhd \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\gg \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\end{list}
And thus we hve proved $
Prop\ 3.2$.


\section{Proof of $
Prop\ 3.4$ }
in this section we will prove $
Prop\ 3.4$ from \cite{mendelson}

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item $
[
Prop\ 3.4a
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
]$ 

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

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

\item $
[
Prop\ 3.4d
\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}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
]$

\end{list}

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

\item $
[
Prop\ 3.4a_1
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ 
0
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot 
0
]$

\item $
[
Prop\ 3.4a_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 
S5
\gg \underline{
\mathsf {b}}
+ 
0
= \underline{
\mathsf {b}}
; 
Prop\ 3.2o
\rhd \underline{
\mathsf {b}}
+ 
0
= \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ 
0
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
; 
S5
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ 
0
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
; 
Prop\ 3.2d
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ 
0
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ 
0
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ 
0
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ 
0
; 
S7
\gg \underline{
\mathsf {a}}
\cdot 
0
= 
0
; 
Prop\ 3.2i
\rhd \underline{
\mathsf {a}}
\cdot 
0
= 
0
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot 
0
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ 
0
; 
Prop\ 3.2d
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ 
0
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ 
0
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot 
0
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ 
0
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ 
0
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot 
0
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$



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

\item $
[
Prop\ 3.4a_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}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
\vdash 
S6
\gg \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
; 
Prop\ 3.2o
\rhd \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
; 
S8
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
; 
Prop\ 3.2e
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
; 
Prop\ 3.2j
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
; 
Prop\ 3.2c
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
; 
S8
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
; 
Prop\ 3.2i
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
; 
Prop\ 3.2d
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
; 
Prop\ 3.2c
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
; 
Prop\ 3.2c
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
; 
Ded
\rhd 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
{}'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

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

\end{list}

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

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


\end{list}

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item $
[
Prop\ 3.4c_1
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
\cdot 
0
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
\cdot 
0
]$

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

\item $
[
Prop\ 3.4c_2
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
{}'
]$

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

\item $
[
Prop\ 3.4c
\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 
Prop\ 3.4c_1
\gg \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot 
0
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot 
0
; 
Prop\ 3.4c_2
\gg \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
\Rightarrow \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
{}'
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
{}'
; 
S9
\mathop {\char64} \overline{
\mathsf{z}}
\rhd \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot 
0
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot 
0
\rhd \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
\Rightarrow \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
{}'
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
{}'
\gg \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
; 
Ded
\rhd \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
= \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
\cdot \overline{
\mathsf{z}}
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$
\end{list}

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item $
[
Prop\ 3.4d_1
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
+ 
0
= \underline{
\mathsf {b}}
+ 
0
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
]$

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

\item $
[
Prop\ 3.4d_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 {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}}
{}'
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
]$

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

\item $
[
Prop\ 3.4d
\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 
Prop\ 3.4d_1
\gg \overline{
\mathsf{x}}
+ 
0
= \overline{
\mathsf{y}}
+ 
0
\Rightarrow \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
; 
Prop\ 3.4d_2
\gg \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}}
{}'
\Rightarrow \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
; 
S9
\mathop {\char64} \overline{
\mathsf{z}}
\rhd \overline{
\mathsf{x}}
+ 
0
= \overline{
\mathsf{y}}
+ 
0
\Rightarrow \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\rhd \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}}
{}'
\Rightarrow \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\gg \overline{
\mathsf{x}}
+ \overline{
\mathsf{z}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{z}}
\Rightarrow \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
; 
Ded
\rhd \overline{
\mathsf{x}}
+ \overline{
\mathsf{z}}
= \overline{
\mathsf{y}}
+ \overline{
\mathsf{z}}
\Rightarrow \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}
\gg \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$
\end{list}

\section{Numerals}

We will for the remainder of the project need to construct some numerals, the numerals are the names for $
0
,\linebreak [0] 
0
{}'
,\linebreak [0] 
0
{}'
{}'
\ldots$ we will define them as folows $
0
,\linebreak [0] 
0
{}'
,\linebreak [0] 
0
{}'
{}'
\ldots$

With these definitions we will now continue to prove $
Prop\ 3.5$ that states different things about numerals.

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

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

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

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

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

\item $
[
Prop\ 3.5e
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {a}}
= 
0
\Rightarrow \underline{
\mathsf {b}}
= 
0
]$

\item $
[
Prop\ 3.5f
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
= 
0
{}'
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow \underline{
\mathsf {b}}
= 
0
{}'
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
= 
0
{}'
\Rightarrow \underline{
\mathsf {b}}
= 
0
]$

\item $
[
Prop\ 3.5g
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
= 
0
{}'
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
= 
0
{}'
\Rightarrow \underline{
\mathsf {b}}
= 
0
{}'
]$

\item $
[
Prop\ 3.5h
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow 
{\neg }
\forall_{obj} \underline{
\mathsf {b}}
\colon 
{\neg }\underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
{}'
]$

\item $
[
Prop\ 3.5i
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
{\neg }\underline{
\mathsf {c}}
= 
0
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
]$

\item $
[
Prop\ 3.5j
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
= 
0
{}'
\Rightarrow 
{\neg }
\forall_{obj} \underline{
\mathsf {b}}
\colon 
{\neg }\underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
{}'
{}'
]$

\end{list}

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

\item $
[
Prop\ 3.5a
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
S6
\gg \underline{
\mathsf {a}}
+ 
0
{}'
= \underline{
\mathsf {a}}
+ 
0
{}'
; 
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.2c
\rhd \underline{
\mathsf {a}}
+ 
0
{}'
= \underline{
\mathsf {a}}
+ 
0
{}'
\rhd \underline{
\mathsf {a}}
+ 
0
{}'
= \underline{
\mathsf {a}}
{}'
\gg \underline{
\mathsf {a}}
+ 
0
{}'
= \underline{
\mathsf {a}}
{}'
; 
Prop\ 3.2a
\gg \underline{
\mathsf {a}}
+ 
0
{}'
= \underline{
\mathsf {a}}
+ 
0
{}'
; 
S1
\rhd \underline{
\mathsf {a}}
+ 
0
{}'
= \underline{
\mathsf {a}}
+ 
0
{}'
\rhd \underline{
\mathsf {a}}
+ 
0
{}'
= \underline{
\mathsf {a}}
{}'
\gg \underline{
\mathsf {a}}
+ 
0
{}'
= \underline{
\mathsf {a}}
{}'
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

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

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

\item $
[
Prop\ 3.5d_1
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
+ 
0
\Rightarrow \underline{
\mathsf {a}}
= 
0
\wedge 
0
= 
0
]$

\item $
[
Prop\ 3.5d_2
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
= 
0
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow \underline{
\mathsf {b}}
= 
0
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
= 
0
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow \underline{
\mathsf {b}}
{}'
= 
0
]$


\end{list}

\section{Lemma $
Prop\ 3.7$}
\subsection{Definitions of $
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \overline{
\mathsf{x}}
= \overline{
\mathsf{y}}$}

in the folowing we need some definitions, we will macro define them as:


$
[
\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 {=}}
\exists 
\mathsf{z}
\colon 
(
\mathsf{z} 
\neq 
0
\wedge 
\mathsf{z}
+ 
\mathsf{x}
= 
\mathsf{y}
)
]
\rceil 
)
]$

$
[
\mathsf{x} 
\leq 
\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} 
\leq 
\mathsf{y}
\mathrel {\ddot {=}}
\mathsf{x} 
< 
\mathsf{y}
\vee 
\mathsf{x}
= 
\mathsf{y}
]
\rceil 
)
]$

$
[
\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 {=}}
\mathsf{y} 
< 
\mathsf{x}
]
\rceil 
)
]$

$
[
\mathsf{x} 
\geq 
\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} 
\geq 
\mathsf{y}
\mathrel {\ddot {=}}
\mathsf{y} 
\leq 
\mathsf{x}
]
\rceil 
)
]$

$
[
\mathsf{x} 
\nless 
\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} 
\nless 
\mathsf{y}
\mathrel {\ddot {=}}
{\neg }
(
\mathsf{x} 
< 
\mathsf{y}
)
]
\rceil 
)
]$

$
[
\mathsf{x} 
\ngtr 
\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} 
\ngtr 
\mathsf{y}
\mathrel {\ddot {=}}
\mathsf{y} 
\nless 
\mathsf{x}
]
\rceil 
)
]$

$
[
\mathsf{x}
\mathrel{|} 
\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}
\mathrel{|} 
\mathsf{y}
\mathrel {\ddot {=}}
\exists 
\mathsf{z}
\colon 
\mathsf{y}
= 
\mathsf{x}
\cdot 
\mathsf{z}
]
\rceil 
)
]$

with these definitions, we will continue to prove the following statements:

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

\item $
[
Prop\ 3.7a
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.7b
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
]$

\item $
[
Prop\ 3.7c
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.7d
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
]$

\item $
[
Prop\ 3.7e
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.7f
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
]$

\item $
[
Prop\ 3.7g
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
]$

\item $
[
Prop\ 3.7g'
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
]$

\item $
[
Prop\ 3.7h
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
]$

\item $
[
Prop\ 3.7i
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ 
0
= \underline{
\mathsf {a}}
\Rightarrow 
0
= \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.7j
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ 
0
= \underline{
\mathsf {a}}
{}'
]$

\item $
[
Prop\ 3.7k
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
{}'
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
{}'
= \underline{
\mathsf {b}}
]$

\item $
[
Prop\ 3.7k'
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
{}'
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
{}'
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
]$

\item $
[
Prop\ 3.7l
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
{}'
]$

\item $
[
Prop\ 3.7l'
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
{}'
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
]$

\item $
[
Prop\ 3.7m
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
{}'
]$

\item $
[
Prop\ 3.7o
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }\underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.7p
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }
{\neg }\underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.7q
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.7r
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
]$

\item $
[
Prop\ 3.7s
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }\underline{
\mathsf {b}}
= 
0
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
]$

\item $
[
Prop\ 3.7t
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }\underline{
\mathsf {b}}
= 
0
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
]$

\item $
[
Prop\ 3.7u
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ 
0
= \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.7u'
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ 
0
= \underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
= 
0
]$

\item $
[
Prop\ 3.7v
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ 
0
= \underline{
\mathsf {a}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ 
0
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ 
0
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
]$

\item $
[
Prop\ 3.7w
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ 
0
{}'
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.7x
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.7x'
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
]$

\item $
[
Prop\ 3.7y
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
]$

\item $
[
Prop\ 3.7y'
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon 
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
]$

\item $
[
Prop\ 3.7z
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= 
0
]$

\item $
[
Prop\ 3.7z'
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
]$ 
\end{list}
\subsection{proof of $
Prop\ 3.7$}

\section{Lemma $
Prop\ 3.10$}
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item $
[
Prop\ 3.10a
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }\underline{
\mathsf {a}}
= 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\cdot 
\mathsf{z}
]$

\item $
[
Prop\ 3.10b
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }\underline{
\mathsf {a}}
= 
\forall \underline{
\mathsf {a}}
\colon 
0
{}'
\cdot 
\mathsf{z}
]$

\item $
[
Prop\ 3.10c
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
0
= 
\forall \underline{
\mathsf {a}}
\colon \underline{
\mathsf {a}}
\cdot 
\mathsf{z}
]$

\item $
[
Prop\ 3.10d
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }\underline{
\mathsf {c}}
= 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }\underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
= 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }\underline{
\mathsf {b}}
\wedge \underline{
\mathsf {b}}
= 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
\cdot 
\mathsf{z}
\cdot 
\mathsf{z}
\cdot 
\mathsf{z}
]$

\item $
[
Prop\ 3.10e
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }\underline{
\mathsf {b}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {a}}
= 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow \underline{
\mathsf {b}}
\cdot 
\mathsf{z}
]$

\item $
[
Prop\ 3.10f
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
= 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }\underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {b}}
= 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\cdot 
\mathsf{z}
\cdot 
\mathsf{z}
]$

\item $
[
Prop\ 3.10g
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }\underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
= 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }\underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
= 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
\cdot 
\mathsf{z}
\cdot 
\mathsf{z}
]$

\item $
[
Prop\ 3.10h
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }\underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
= 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }\underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {a}}
= 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }\underline{
\mathsf {b}}
\wedge \underline{
\mathsf {a}}
= 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
\forall \underline{
\mathsf {c}}
\colon \underline{
\mathsf {a}}
\cdot 
\mathsf{z}
\cdot 
\mathsf{z}
\cdot 
\mathsf{z}
]$

\end{list}


\section{Lemma $
Prop\ 3.11$}
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item $
[
Prop\ 3.11
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon 
{\neg }\underline{
\mathsf {a}}
= 
0
\Rightarrow 
{\neg }
\forall_{obj} \underline{
\mathsf {c}}
\colon 
\forall_{obj} \underline{
\mathsf {d}}
\colon 
{\neg }
{\neg }
{\neg }\underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
+ \underline{
\mathsf {d}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {d}}
= \underline{
\mathsf {a}}
\Rightarrow 
\forall_{obj} \underline{
\mathsf {e}}
\colon 
\forall_{obj} \underline{
\mathsf {f}}
\colon 
{\neg }\underline{
\mathsf {b}}
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {e}}
+ \underline{
\mathsf {f}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
\mathsf{z}
+ \underline{
\mathsf {f}}
= \underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {c}}
= \underline{
\mathsf {e}}
\Rightarrow \underline{
\mathsf {d}}
= \underline{
\mathsf {f}}
]$

\end{list}

\appendix

\section{Helping lemmas}

for some of our proofs we need to prove some lemmas concerning $\wedge$ and $\vee$ these will be proved here.
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

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

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

\item $
[
H0a
\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}}
\vdash \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {c}}
\vdash \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {c}}
]$

\item $
[
H0b
\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}}
\vdash \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {c}}
]$


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

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



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

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

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

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

\item $
[
Dis2
\stackrel{
stmt
}{\rightarrow}
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {b}}
\vdash 
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
]$
\end{list}
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item $
[
T0
\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 {b}}
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\vdash 
Repetition
\rhd \underline{
\mathsf {b}}
\gg \underline{
\mathsf {b}}
; 
Ded
\rhd 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {a}}
\vdash \underline{
\mathsf {b}}
\gg \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
; 
Ded
\rhd 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{
\mathsf {b}}
\colon \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\gg \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {b}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

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

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

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

\item $
[
H1
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
Neg
\gg 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
; 
Repetition
\gg 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
; 
H0b
\rhd 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
\rhd 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\gg 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
; 
A1'
\gg 
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
; 
H0a
\rhd 
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
\rhd 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
\gg 
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$

\item $
[
H2
\stackrel{
proof
}{\rightarrow}
\lambda 
\mathsf {c}
.
\lambda 
\mathsf{x}
.
{\cal P}( 
\lceil 
S
\vdash 
\forall \underline{
\mathsf {a}}
\colon 
Neg
\gg 
{\neg }
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
; 
H1
\gg 
{\neg }
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
; 
MP
\rhd 
{\neg }
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
\rhd 
{\neg }
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\gg 
{\neg }
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
; 
A1'
\gg \underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
; 
H1
\rhd 
{\neg }
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
\rhd \underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
\gg \underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$
\end{list}
%------------------------------------------------------------------------------
\bibliographystyle{alpha}
\bibliography{./page}
%------------------------------------------------------------------------------
\everymath{}
\everydisplay{}

\end{document}
