\documentclass [fleqn]{article}

\everymath{\rm}
\usepackage{latexsym}
\usepackage{amsmath}
\usepackage{amssymb}

\setlength {\overfullrule }{0mm}
\input{lgwinclude}

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



\begin {document}
\title {Udvidedlse af S-reglerne, Appendix}
\author {Maja Hanne T\o nnesen, Rune Christoffer Kildetoft Andresen \\ \& Niels Peter Meyn Milthers}
\date {\today}
\maketitle
\tableofcontents



\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 
{\neg }
\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 
{\neg }
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\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 
{\neg }
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\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 
{\neg }
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
{}'
\Rightarrow 
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\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 
{\neg }
\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 
{\neg }
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\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 
{\neg }
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\mathsf{z}
+ 
0
= \underline{
\mathsf {a}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\mathsf{z}
+ 
0
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\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 
{\neg }
\mathsf{z}
+ 
0
{}'
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\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 
{\neg }
\mathsf{z}
+ \underline{
\mathsf {b}}
= \underline{
\mathsf {c}}
\Rightarrow 
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\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 
{\neg }
\mathsf{z}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\Rightarrow 
{\neg }
{\neg }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\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 
{\neg }
\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 
{\neg }\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 
{\neg }\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 }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\mathsf{z}
+ \underline{
\mathsf {d}}
= \underline{
\mathsf {a}}
\Rightarrow 
{\neg }
\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 }
{\neg }
\forall_{obj} 
\mathsf{z}
\colon 
{\neg }
{\neg }
{\neg }
\mathsf{z}
= 
0
\Rightarrow 
{\neg }
\mathsf{z}
+ \underline{
\mathsf {f}}
= \underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {c}}
= \underline{
\mathsf {e}}
\Rightarrow 
{\neg }\underline{
\mathsf {d}}
= \underline{
\mathsf {f}}
]$

\end{list}





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

\end{document}
