\documentclass [fleqn]{article}

\everymath{\rm}
\everydisplay{\rm}
\usepackage{latexsym}
\setlength {\overfullrule }{0mm}
\input{lgwinclude}
\usepackage[danish]{babel}
\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 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$. continuing to 3.4, bevise 3.5,
%tilf\o je aksiomet %$ x < y <=> E z : z 0 \& z + x = y$, bevise 3.7, tilf\o je
aksiomer, der definerer x|y, bevise 3.10, og bevise 3.11.


We chose to prove chapter 3 from mendelson, starting with Lemma 3.2, since the first ten wfs' are proved in Mendelson, we will
start with Lemma 3.2.i.


\section{}


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}


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

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

we will start by  doing $
Prop\ 3.2i$
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

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


\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
= 
0
\cdot \underline{
\mathsf {a}}
\rhd 
0
\cdot \underline{
\mathsf {a}}
{}'
= 
0
\cdot \underline{
\mathsf {a}}
+ 
0
\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 
Prop\ 3.2l_1
\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 {t}}
\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 
0
= \underline{
\mathsf {a}}
\cdot 
0
; 
Prop\ 3.2e
\gg 
0
= \underline{
\mathsf {a}}
\cdot 
0
\Rightarrow 
0
+ 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
; 
0
= \underline{
\mathsf {a}}
\cdot 
0
\Rightarrow 
0
+ 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
\rhd 
0
= \underline{
\mathsf {a}}
\cdot 
0
\gg 
0
+ 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
; 
Prop\ 3.2c
\gg 
0
= 
0
+ 
0
\Rightarrow 
0
+ 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
\Rightarrow 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
; 
0
= 
0
+ 
0
\Rightarrow 
0
+ 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
\Rightarrow 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
\rhd 
0
= 
0
+ 
0
\rhd 
0
+ 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
\gg 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
; 
Prop\ 3.2c
\gg \underline{
\mathsf {a}}
{}'
\cdot 
0
= 
0
\Rightarrow 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
\Rightarrow \underline{
\mathsf {a}}
{}'
\cdot 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
; \underline{
\mathsf {a}}
{}'
\cdot 
0
= 
0
\Rightarrow 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
\Rightarrow \underline{
\mathsf {a}}
{}'
\cdot 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
\rhd \underline{
\mathsf {a}}
{}'
\cdot 
0
= 
0
\rhd \underline{
\mathsf {a}}
{}'
\cdot 
0
= 
0
\Rightarrow 
0
= \underline{
\mathsf {a}}
\cdot 
0
+ 
0
\Rightarrow \underline{
\mathsf {a}}
{}'
\cdot 
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
\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}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
{}'
; \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}}
{}'
= \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
{}'
\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}}
{}'
; 
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}}
\cdot \underline{
\mathsf {b}}
+ \underline{
\mathsf {a}}
+ \underline{
\mathsf {b}}
{}'
\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}}
{}'
\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.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.2c
\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.2b
\rhd 
Prop\ 3.2m
\gg \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {a}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
{}'
\cdot \underline{
\mathsf {a}}
; 
Prop\ 3.2c
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_e \else
\if \relax \csname lgwelle\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwelle {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwelle \fi 
\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 {s}}
\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}}
= \overline{
\mathsf{x}}
; 
Ded
\rhd \overline{
\mathsf{x}}
\cdot \overline{
\mathsf{y}}
= \overline{
\mathsf{y}}
= \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 
\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
\gg \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
; \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}}
; 
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
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
; \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
\Rightarrow \underline{
\mathsf {b}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
\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
\gg \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
; \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {b}}
\rhd \underline{
\mathsf {a}}
\cdot \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
\cdot \underline{
\mathsf {a}}
\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}}
\rceil 
, 
p_0
, 
\mathsf {c}
)
]$


\end{list}

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

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





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

\end{document}
