\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 $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7a
\colon 
\Pi {\cal A}
\colon {\cal A} 
\not <  {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7b
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A} 
< {\cal B}
\Rightarrow {\cal B} 
< {\cal C}
\Rightarrow {\cal A} 
< {\cal C}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7c
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A} 
< {\cal B}
\Rightarrow {\cal B} 
\not <  {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7d
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A} 
< {\cal B}
\Rightarrow {\cal A}
+ {\cal C} 
< {\cal B}
+ {\cal C}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7e
\colon 
\Pi {\cal A}
\colon {\cal A} 
\leq {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7f
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A} 
\leq {\cal B}
\Rightarrow {\cal B} 
\leq {\cal C}
\Rightarrow {\cal A} 
\leq {\cal C}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7g
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A} 
\leq {\cal B}
\Rightarrow {\cal A}
+ {\cal C} 
\leq {\cal B}
+ {\cal C}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7g'
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A}
+ {\cal C} 
\leq {\cal B}
+ {\cal C}
\Rightarrow {\cal A} 
\leq {\cal B}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7h
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A} 
\leq {\cal B}
\Rightarrow {\cal B} 
< {\cal C}
\Rightarrow {\cal A} 
< {\cal C}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7i
\colon 
\Pi {\cal A}
\colon 
0 
\leq {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7j
\colon 
\Pi {\cal A}
\colon 
0 
< {\cal A}
{}'
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7k
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A} 
< {\cal B}
\Rightarrow {\cal A}
{}' 
\leq {\cal B}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7k'
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A}
{}' 
\leq {\cal B}
\Rightarrow {\cal A} 
< {\cal B}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7l
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A} 
\leq {\cal B}
\Rightarrow {\cal A} 
< {\cal B}
{}'
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7l'
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A} 
< {\cal B}
{}'
\Rightarrow {\cal A} 
\leq {\cal B}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7m
\colon 
\Pi {\cal A}
\colon {\cal A} 
< {\cal A}
{}'
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7o
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A} 
\neq {\cal B}
\Rightarrow 
({\cal A} 
< {\cal B}
\vee {\cal B} 
< {\cal A}
)
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7p
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A}
= {\cal B}
\vee {\cal A} 
< {\cal B}
\vee {\cal B} 
< {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7q
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A} 
\leq {\cal B}
\vee {\cal B} 
\leq {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7r
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A}
+ {\cal B} 
\geq {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7s
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal B} 
\neq 
0
\Rightarrow {\cal A}
+ {\cal B} 
> {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7t
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal B} 
\neq 
0
\Rightarrow {\cal A}
\cdot {\cal B} 
\geq {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7u
\colon 
\Pi {\cal A}
\colon {\cal A} 
\neq 
0
\Rightarrow {\cal A} 
> 
0
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7u'
\colon 
\Pi {\cal A}
\colon {\cal A} 
> 
0
\Rightarrow {\cal A} 
\neq 
0
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7v
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A} 
> 
0
\Rightarrow {\cal B} 
> 
0
\Rightarrow {\cal A}
\cdot {\cal B} 
> 
0
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7w
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A} 
\neq 
0
\Rightarrow {\cal B} 
> 
\overline{1}
\Rightarrow {\cal B}
\cdot {\cal A} 
> {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7x
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A} 
\neq 
0
\Rightarrow {\cal B} 
< {\cal C}
\Rightarrow {\cal B}
\cdot {\cal A} 
< {\cal C}
\cdot {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7x'
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A} 
\neq 
0
\Rightarrow {\cal B}
\cdot {\cal A} 
< {\cal C}
\cdot {\cal A}
\Rightarrow {\cal B} 
< {\cal C}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7y
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A} 
\neq 
0
\Rightarrow {\cal B} 
\leq {\cal C}
\Rightarrow {\cal B}
\cdot {\cal A} 
\leq {\cal C}
\cdot {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7y'
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A} 
\neq 
0
\Rightarrow {\cal B}
\cdot {\cal A} 
\leq {\cal C}
\cdot {\cal A}
\Rightarrow {\cal B} 
\leq {\cal C}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7z
\colon 
\Pi {\cal A}
\colon {\cal A} 
\not <  
0
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.7z'
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A} 
\leq {\cal B}
\wedge {\cal B} 
\leq {\cal A}
\Rightarrow {\cal A}
= {\cal 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 $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.10a
\colon 
\Pi {\cal A}
\colon {\cal A}
\mathrel{|} {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.10b
\colon 
\Pi {\cal A}
\colon 
\overline{1}
\mathrel{|} {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.10c
\colon 
\Pi {\cal A}
\colon {\cal A}
\mathrel{|} 
0
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.10d
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A}
\mathrel{|} {\cal B}
\wedge {\cal B}
\mathrel{|} {\cal C}
\Rightarrow {\cal A}
\mathrel{|} {\cal C}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.10e
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A} 
\neq 
0
\wedge {\cal B}
\mathrel{|} {\cal B}
\Rightarrow {\cal A} 
\leq {\cal A}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.10f
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A}
\mathrel{|} {\cal B}
\wedge {\cal B}
\mathrel{|} {\cal A}
\Rightarrow {\cal A}
= {\cal B}
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.10g
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A}
\mathrel{|} {\cal B}
\Rightarrow {\cal A}
\mathrel{|} 
({\cal B}
\cdot {\cal C}
)
]$

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.10h
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
,\linebreak [0] {\cal C}
\colon {\cal A}
\mathrel{|} {\cal B}
\wedge {\cal A}
\mathrel{|} {\cal C}
\Rightarrow {\cal A}
\mathrel{|} 
({\cal B}
+ {\cal C}
)
]$

\end{list}


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

\item $
[ 
S
\mathbf{\ lemma\ } 
Prop\ 3.11
\colon 
\Pi {\cal A}
,\linebreak [0] {\cal B}
\colon {\cal A} 
\neq 
0
\Rightarrow 
\exists {\cal C}
,\linebreak [0] {\cal D}
\colon 
({\cal B}
= {\cal A}
\cdot {\cal C}
+ {\cal D}
\wedge {\cal D} 
< {\cal A}
\wedge 
\forall {\cal E}
,\linebreak [0] {\cal F}
\colon 
(
({\cal B}
= {\cal A}
\cdot {\cal E}
+ {\cal F}
\wedge {\cal F} 
< {\cal A}
)
\Rightarrow {\cal C}
= {\cal E}
\wedge {\cal D}
= {\cal F}
)
)
]$

\end{list}





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

\end{document}
