Logiweb expansion of opgave in pyk

Up Help

"File page.tex
\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 {Udvidelse af S-reglerne}
\author {Maja Hanne T\o nnesen, Rune Christoffer Kildetoft Andresen \\ \& Niels Peter Meyn Milthers}
\date {\today}
\maketitle
\tableofcontents

" [ ragged right ] "



\section{Introduktion}
Dette skriftlige projekt er lavet i forbindelse med
Logik-kurset 2006\footnote{Kursus 061004/202 Logik}.

Vores m\aa{}l i denne opgave var at bevise en delm\ae{}ngde af udsagnene\footnote{Eng.:
proposition} vedr\o{}rende l\ae{}res\ae{}tningerne\footnote{Eng.: theorem} fra
S-systemet, som er beskrevet i Mendelson \cite{mendelson} i kapitel 3.1. For lethedens skyld er alle nummereringer de samme som i Mendelson.

Mere pr\ae{}cist g\aa{}r opgaven ud p\aa{} at bevise 3.2(j-o), bevise 3.4, bevise
3.5, tilf\o{}je aksiomet $x < y \Leftrightarrow \exists z : z \neq 0
\land z + x = y$, bevise 3.7, tilf\o{}je aksiomer, der definere " [ math not for all objects var z indeed not object var var y end var equal object var var x end var times var z end math ] ",
bevise 3.10 og bevise 3.11.

I afsnittene 3 til 7 er beviserne for de p\aa{}viste lemmaer
gennemg\aa{}et. Alle trivielle hj\ae{}lpelemmaer er bevist i appendix \ref{help}.

\section{Konklusion}
Vi har ikke l\o{}st opgaven til fulde, men har dog form\aa{}et at p\aa{}vise
3.2j - 3.2o, 3.4, 3.5a -g. P\aa{} grund af problemer med definitionen af
reglen svarende til ``existensial rule'' side 77 i mendelson, har vi
som beskrevet i afsnit \ref{35} ikke v\ae{}ret i stand til at kunne bevise
lemmaerne fra 3.5h og frem.

Vi har dog som beskrevet i afsnit \ref{35h} og \ref{exist} gennemg\aa{}et hvordan
beviserne for 3.5h og ``existensial rule'' ville have set ud, hvis
problemet ikke var opst\aa{}et.

Vi har endvidere kort gennemg\aa{}et de definitioner, som ville v\ae{}re
n\o{}dvendige for at kunne p\aa{}vise Lemma 3.7

\section{S-reglerne}

S-systemet er en f\o{}rste ordens teori, som er udviklet ud fra Peanos
postulater og ved hj\ae{}lp m\ae{}ngdel\ae{}re. Det skulle v\ae{}re passende at
bruge til at bevise basis-resultaterne for tal-teori. Aksiomerne for S
er f\o{}lgende.\\

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

\item \makebox[0.45\textwidth][l]{" [ math define statement of system s as var x end define end math ] "}" [ math define statement of rule mp as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar end define , define proof of rule mp as rule tactic end define end math ] "

\item \makebox[0.45\textwidth][l]{" [ math define statement of rule gen as system s infer all metavar var x end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer for all objects metavar var x end metavar indeed metavar var a end metavar end define , define proof of rule gen as rule tactic end define end math ] "}" [ math define statement of deduction as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed lambda var x dot deduction zero quote metavar var a end metavar end quote conclude quote metavar var b end metavar end quote end deduction endorse metavar var a end metavar infer metavar var b end metavar end define , define proof of deduction as rule tactic end define end math ] "

\item \makebox[0.45\textwidth][l]{}" [ math define statement of axiom s two as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var a end metavar suc equal metavar var b end metavar suc end define , define proof of axiom s two as rule tactic end define end math ] "

\item \makebox[0.45\textwidth][l]{" [ math define statement of axiom s three as system s infer all metavar var a end metavar indeed not zero equal metavar var a end metavar suc end define , define proof of axiom s three as rule tactic end define end math ] "}" [ math define statement of axiom s four as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar suc equal metavar var b end metavar suc infer metavar var a end metavar equal metavar var b end metavar end define , define proof of axiom s four as rule tactic end define end math ] "

\item \makebox[0.45\textwidth][l]{" [ math define statement of axiom s five as system s infer all metavar var a end metavar indeed metavar var a end metavar plus zero equal metavar var a end metavar end define , define proof of axiom s five as rule tactic end define end math ] "}" [ math define statement of axiom s six as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc end define , define proof of axiom s six as rule tactic end define end math ] "

\item \makebox[0.45\textwidth][l]{" [ math define statement of axiom s seven as system s infer all metavar var a end metavar indeed metavar var a end metavar times zero equal zero end define , define proof of axiom s seven as rule tactic end define end math ] "}" [ math define statement of axiom s eight as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar end define , define proof of axiom s eight as rule tactic end define end math ] "

\item " [ math define statement of axiom s one as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var a end metavar equal metavar var c end metavar infer metavar var b end metavar equal metavar var c end metavar end define , define proof of axiom s one as rule tactic end define end math ] "
\end{list}



Endvidere er reglen \textit{S9}, som er grundl\ae{}ggende for matematisk
induktion, ogs\aa{} en del af \textit{S}-teorien. Denne regel kan p\aa{}
almindeligt sprog udtrykkes som:

\begin{quote}\textit{Hvis en egenskab holder for 0 og egenskaben holder for efterf\o{}lgeren $x'$
til et naturligt tal $x$, som egenskaben g\ae{}lder for, s\aa{} vil egenskaben
g\ae{}lde for alle naturlige tal. }
\end{quote}

I pyk er S9 defineret som:\\

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

\item " [ math define statement of axiom s nine as system s infer all metavar var x end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed sub zero quote metavar var b end metavar end quote is quote metavar var a end metavar end quote where quote metavar var x end metavar end quote is quote zero end quote end sub endorse sub zero quote metavar var c end metavar end quote is quote metavar var a end metavar end quote where quote metavar var x end metavar end quote is quote metavar var x end metavar suc end quote end sub endorse metavar var b end metavar infer metavar var a end metavar imply metavar var c end metavar infer metavar var a end metavar end define , define proof of axiom s nine as rule tactic end define end math ] "

\end{list}
Reglen for bevis ved mods\ae{}tninger er den sidste grundl\ae{}ggende regel,
der skal bruges i beviserne. Reglen kan p\aa{} almindeligt sprog udtrykkes
som f\o{}lgende:

\begin{quote} \textit{Hvis man ud fra en antagelse $A$
kan p\aa{}vise at en egenskab $B$ g\ae{}lder, og at man (n\aa{}r antagelsen stadig g\ae{}lder) kan vise at den modsatte egenskab $\lnot B$ ogs\aa{} g\ae{}lder, s\aa{}
m\aa{} det modsatte af antagelsen g\ae{}lde, dvs. $\lnot A$.}
\end{quote}

I pyk er reglen defineret som:\\

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

\item " [ math define statement of double negation as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar imply not metavar var a end metavar infer not metavar var b end metavar imply metavar var a end metavar infer metavar var b end metavar end define , define proof of double negation as rule tactic end define end math ] "
\end{list}

\section{Udsagn 3.2}
Dette udsagn indeholder de grundl\ae{}ggende regneregler for tal, som
opf\o{}rer sig som de naturlige tal. Hj\ae{}lpes\ae{}tningerne eller lemmaerne er
generelt set en direkte konsekvens af aksiomerne.

Alle lemmaerne i dette afsnit kan udledes ud fra de tidligere n\ae{}vnte og som
det er bevist i b\aa{}de check \cite{check} og Mendelson er der for ethvert
udtryk " [ math metavar var a end metavar comma metavar var b end metavar comma metavar var c end metavar end math ] "
f\o{}lgende velformulerede s\ae{}tninger\footnote{Eng.: Wellformed formulas} i systemet S:\\

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

\item " [ math define statement of prop three two a as system s infer all metavar var a end metavar indeed metavar var a end metavar equal metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three two b as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var b end metavar equal metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three two c as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var b end metavar equal metavar var c end metavar infer metavar var a end metavar equal metavar var c end metavar end define end math ] "

\item " [ math define statement of prop three two d as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var c end metavar infer metavar var b end metavar equal metavar var c end metavar infer metavar var a end metavar equal metavar var b end metavar end define end math ] "

\item " [ math define statement of prop three two e as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar end define end math ] "

\item " [ math define statement of prop three two f as system s infer all metavar var a end metavar indeed metavar var a end metavar equal zero plus metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three two g as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar suc plus metavar var b end metavar equal metavar var a end metavar plus metavar var b end metavar suc end define end math ] "

\item " [ math define statement of prop three two h as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar equal metavar var b end metavar plus metavar var a end metavar end define end math ] "
\end{list}

Da 3.2i ikke er bevist i check, (men er i Mendelson),
har vi valgt for \o{}velsens skyld at indskrive beviset:\\
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item " [ math define statement of prop three two i as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var c end metavar plus metavar var a end metavar equal metavar var c end metavar plus metavar var b end metavar end define end math ] "

\item " [ math define proof of prop three two i as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer prop three two e modus ponens metavar var a end metavar equal metavar var b end metavar conclude metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar cut prop three two h conclude metavar var a end metavar plus metavar var c end metavar equal metavar var c end metavar plus metavar var a end metavar cut prop three two h conclude metavar var b end metavar plus metavar var c end metavar equal metavar var c end metavar plus metavar var b end metavar cut axiom s one modus ponens metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar modus ponens metavar var a end metavar plus metavar var c end metavar equal metavar var c end metavar plus metavar var a end metavar conclude metavar var b end metavar plus metavar var c end metavar equal metavar var c end metavar plus metavar var a end metavar cut prop three two b modus ponens metavar var b end metavar plus metavar var c end metavar equal metavar var c end metavar plus metavar var a end metavar conclude metavar var c end metavar plus metavar var a end metavar equal metavar var b end metavar plus metavar var c end metavar cut prop three two c modus ponens metavar var c end metavar plus metavar var a end metavar equal metavar var b end metavar plus metavar var c end metavar modus ponens metavar var b end metavar plus metavar var c end metavar equal metavar var c end metavar plus metavar var b end metavar conclude metavar var c end metavar plus metavar var a end metavar equal metavar var c end metavar plus metavar var b end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var c end metavar plus metavar var a end metavar equal metavar var c end metavar plus metavar var b end metavar conclude metavar var a end metavar equal metavar var b end metavar infer metavar var c end metavar plus metavar var a end metavar equal metavar var c end metavar plus metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "

\end{list}

De f\o{}lgende lemmaer er opskrevet, men ikke bevist i Mendelson. Disse er
blandt dem som vi \o{}nsker at bevise.


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

\item " [ math define statement of prop three two j as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar end define end math ] "

\item " [ math define statement of prop three two k as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar end define end math ] "

\item " [ math define statement of prop three two l as system s infer all metavar var a end metavar indeed zero times metavar var a end metavar equal zero end define end math ] "

\item " [ math define statement of prop three two m as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar suc times metavar var b end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar end define end math ] "

\item " [ math define statement of prop three two n as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar equal metavar var b end metavar times metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three two o as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var c end metavar times metavar var a end metavar equal metavar var c end metavar times metavar var b end metavar end define end math ] "

\end{list}

Her efter f\o{}lger beviserne.

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

\item " [ math define statement of prop three two j one as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar plus zero equal metavar var a end metavar plus metavar var b end metavar plus zero end define end math ] "

\item " [ math define proof of prop three two j one as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed axiom s five conclude metavar var a end metavar plus metavar var b end metavar plus zero equal metavar var a end metavar plus metavar var b end metavar cut axiom s five conclude metavar var b end metavar plus zero equal metavar var b end metavar cut prop three two i modus ponens metavar var b end metavar plus zero equal metavar var b end metavar conclude metavar var a end metavar plus metavar var b end metavar plus zero equal metavar var a end metavar plus metavar var b end metavar cut prop three two d modus ponens metavar var a end metavar plus metavar var b end metavar plus zero equal metavar var a end metavar plus metavar var b end metavar modus ponens metavar var a end metavar plus metavar var b end metavar plus zero equal metavar var a end metavar plus metavar var b end metavar conclude metavar var a end metavar plus metavar var b end metavar plus zero equal metavar var a end metavar plus metavar var b end metavar plus zero end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three two j two as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar imply metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc end define end math ] "

\item " [ math define proof of prop three two j two as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar infer axiom s six conclude metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc cut axiom s two modus ponens metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar conclude metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc cut prop three two c modus ponens metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc modus ponens metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc conclude metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc cut axiom s six conclude metavar var b end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc cut prop three two i modus ponens metavar var b end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc conclude metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc cut axiom s six conclude metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc cut prop three two c modus ponens metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc modus ponens metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc conclude metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc cut prop three two d modus ponens metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc modus ponens metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc conclude metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar infer metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc conclude metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar imply metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar suc end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three two j as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar end define end math ] "



\item " [ math define proof of prop three two j as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed prop three two j one conclude object var var x end var plus object var var y end var plus zero equal object var var x end var plus object var var y end var plus zero cut prop three two j two conclude object var var x end var plus object var var y end var plus object var var z end var equal object var var x end var plus object var var y end var plus object var var z end var imply object var var x end var plus object var var y end var plus object var var z end var suc equal object var var x end var plus object var var y end var plus object var var z end var suc cut axiom s nine at object var var z end var modus ponens object var var x end var plus object var var y end var plus zero equal object var var x end var plus object var var y end var plus zero modus ponens object var var x end var plus object var var y end var plus object var var z end var equal object var var x end var plus object var var y end var plus object var var z end var imply object var var x end var plus object var var y end var plus object var var z end var suc equal object var var x end var plus object var var y end var plus object var var z end var suc conclude object var var x end var plus object var var y end var plus object var var z end var equal object var var x end var plus object var var y end var plus object var var z end var cut deduction modus ponens object var var x end var plus object var var y end var plus object var var z end var equal object var var x end var plus object var var y end var plus object var var z end var conclude metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar plus metavar var b end metavar plus metavar var c end metavar end quote state proof state cache var c end expand end define end math ] "

\end{list}


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

\item " [ math define statement of prop three two k one as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar times zero equal metavar var b end metavar times zero end define end math ] "

\item " [ math define proof of prop three two k one as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar equal metavar var b end metavar infer axiom s seven conclude metavar var a end metavar times zero equal zero cut axiom s seven conclude metavar var b end metavar times zero equal zero cut prop three two a conclude zero equal zero cut prop three two b modus ponens metavar var b end metavar times zero equal zero conclude zero equal metavar var b end metavar times zero cut prop three two c modus ponens metavar var a end metavar times zero equal zero modus ponens zero equal metavar var b end metavar times zero conclude metavar var a end metavar times zero equal metavar var b end metavar times zero cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var a end metavar times zero equal metavar var b end metavar times zero conclude metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar times zero equal metavar var b end metavar times zero end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three two k two as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar imply metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar times metavar var c end metavar suc equal metavar var b end metavar times metavar var c end metavar suc end define end math ] "

\item " [ math define proof of prop three two k two as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar infer metavar var a end metavar equal metavar var b end metavar infer rule mp modus ponens metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar modus ponens metavar var a end metavar equal metavar var b end metavar conclude metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar cut axiom s eight conclude metavar var a end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar cut axiom s eight conclude metavar var b end metavar times metavar var c end metavar suc equal metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar cut prop three two e modus ponens metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar conclude metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar equal metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar cut prop three two i modus ponens metavar var a end metavar equal metavar var b end metavar conclude metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar equal metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar cut prop three two c modus ponens metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar equal metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar modus ponens metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar equal metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar conclude metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar equal metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar cut prop three two c modus ponens metavar var a end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar modus ponens metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar equal metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar conclude metavar var a end metavar times metavar var c end metavar suc equal metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar cut prop three two d modus ponens metavar var a end metavar times metavar var c end metavar suc equal metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar modus ponens metavar var b end metavar times metavar var c end metavar suc equal metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar conclude metavar var a end metavar times metavar var c end metavar suc equal metavar var b end metavar times metavar var c end metavar suc cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar infer metavar var a end metavar equal metavar var b end metavar infer metavar var a end metavar times metavar var c end metavar suc equal metavar var b end metavar times metavar var c end metavar suc conclude metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar imply metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar times metavar var c end metavar suc equal metavar var b end metavar times metavar var c end metavar suc end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three two k as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar end define end math ] "

\item " [ math define proof of prop three two k as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer prop three two k one conclude object var var x end var equal object var var y end var imply object var var x end var times zero equal object var var y end var times zero cut prop three two k two conclude object var var x end var equal object var var y end var imply object var var x end var times object var var z end var equal object var var y end var times object var var z end var imply object var var x end var equal object var var y end var imply object var var x end var times object var var z end var suc equal object var var y end var times object var var z end var suc cut axiom s nine at object var var z end var modus ponens object var var x end var equal object var var y end var imply object var var x end var times zero equal object var var y end var times zero modus ponens object var var x end var equal object var var y end var imply object var var x end var times object var var z end var equal object var var y end var times object var var z end var imply object var var x end var equal object var var y end var imply object var var x end var times object var var z end var suc equal object var var y end var times object var var z end var suc conclude object var var x end var equal object var var y end var imply object var var x end var times object var var z end var equal object var var y end var times object var var z end var cut deduction modus ponens object var var x end var equal object var var y end var imply object var var x end var times object var var z end var equal object var var y end var times object var var z end var conclude metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar cut rule mp modus ponens metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar modus ponens metavar var a end metavar equal metavar var b end metavar conclude metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar end quote state proof state cache var c end expand end define end math ] "

\end{list}


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


\item " [ math define statement of prop three two l two as system s infer all metavar var a end metavar indeed zero times metavar var a end metavar equal zero imply zero times metavar var a end metavar suc equal zero end define end math ] "

\item " [ math define proof of prop three two l two as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var a end metavar indeed zero times metavar var a end metavar equal zero infer axiom s eight conclude zero times metavar var a end metavar suc equal zero times metavar var a end metavar plus zero cut axiom s five conclude zero times metavar var a end metavar plus zero equal zero times metavar var a end metavar cut prop three two c modus ponens zero times metavar var a end metavar suc equal zero times metavar var a end metavar plus zero modus ponens zero times metavar var a end metavar plus zero equal zero times metavar var a end metavar conclude zero times metavar var a end metavar suc equal zero times metavar var a end metavar cut prop three two c modus ponens zero times metavar var a end metavar suc equal zero times metavar var a end metavar modus ponens zero times metavar var a end metavar equal zero conclude zero times metavar var a end metavar suc equal zero cut deduction modus ponens all metavar var a end metavar indeed zero times metavar var a end metavar equal zero infer zero times metavar var a end metavar suc equal zero conclude zero times metavar var a end metavar equal zero imply zero times metavar var a end metavar suc equal zero end quote state proof state cache var c end expand end define end math ] "
\item " [ math define statement of prop three two l as system s infer all metavar var a end metavar indeed zero times metavar var a end metavar equal zero end define end math ] "


\item " [ math define proof of prop three two l as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed axiom s seven conclude zero times zero equal zero cut prop three two l two conclude zero times object var var x end var equal zero imply zero times object var var x end var suc equal zero cut axiom s nine at object var var x end var modus ponens zero times zero equal zero modus ponens zero times object var var x end var equal zero imply zero times object var var x end var suc equal zero conclude zero times object var var x end var equal zero cut deduction modus ponens zero times object var var x end var equal zero conclude zero times metavar var a end metavar equal zero end quote state proof state cache var c end expand end define end math ] "

\end{list}


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

\item " [ math define statement of prop three two m one as system s infer all metavar var a end metavar indeed metavar var a end metavar suc times zero equal metavar var a end metavar times zero plus zero end define end math ] "

\item " [ math define proof of prop three two m one as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed axiom s seven conclude metavar var a end metavar suc times zero equal zero cut prop three two f conclude zero equal zero plus zero cut axiom s seven conclude metavar var a end metavar times zero equal zero cut prop three two b modus ponens metavar var a end metavar times zero equal zero conclude zero equal metavar var a end metavar times zero cut prop three two e modus ponens zero equal metavar var a end metavar times zero conclude zero plus zero equal metavar var a end metavar times zero plus zero cut prop three two c modus ponens zero equal zero plus zero modus ponens zero plus zero equal metavar var a end metavar times zero plus zero conclude zero equal metavar var a end metavar times zero plus zero cut prop three two c modus ponens metavar var a end metavar suc times zero equal zero modus ponens zero equal metavar var a end metavar times zero plus zero conclude metavar var a end metavar suc times zero equal metavar var a end metavar times zero plus zero end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three two m two as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar suc times metavar var b end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar imply metavar var a end metavar suc times metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar suc plus metavar var b end metavar suc end define end math ] "

\item " [ math define proof of prop three two m two as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar suc times metavar var b end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar infer axiom s eight conclude metavar var a end metavar suc times metavar var b end metavar suc equal metavar var a end metavar suc times metavar var b end metavar plus metavar var a end metavar suc cut prop three two e modus ponens metavar var a end metavar suc times metavar var b end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar conclude metavar var a end metavar suc times metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc cut axiom s six conclude metavar var b end metavar plus metavar var a end metavar suc equal metavar var b end metavar plus metavar var a end metavar suc cut prop three two g conclude metavar var b end metavar suc plus metavar var a end metavar equal metavar var b end metavar plus metavar var a end metavar suc cut prop three two d modus ponens metavar var b end metavar plus metavar var a end metavar suc equal metavar var b end metavar plus metavar var a end metavar suc modus ponens metavar var b end metavar suc plus metavar var a end metavar equal metavar var b end metavar plus metavar var a end metavar suc conclude metavar var b end metavar plus metavar var a end metavar suc equal metavar var b end metavar suc plus metavar var a end metavar cut prop three two h conclude metavar var b end metavar suc plus metavar var a end metavar equal metavar var a end metavar plus metavar var b end metavar suc cut prop three two c modus ponens metavar var b end metavar plus metavar var a end metavar suc equal metavar var b end metavar suc plus metavar var a end metavar modus ponens metavar var b end metavar suc plus metavar var a end metavar equal metavar var a end metavar plus metavar var b end metavar suc conclude metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc cut prop three two i modus ponens metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc conclude metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar plus metavar var b end metavar suc cut prop three two j conclude metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar plus metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar plus metavar var b end metavar suc cut prop three two d modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar plus metavar var b end metavar suc modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar plus metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar plus metavar var b end metavar suc conclude metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar plus metavar var b end metavar suc cut axiom s eight conclude metavar var a end metavar times metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar cut prop three two e modus ponens metavar var a end metavar times metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar conclude metavar var a end metavar times metavar var b end metavar suc plus metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar plus metavar var b end metavar suc cut prop three two d modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar plus metavar var b end metavar suc modus ponens metavar var a end metavar times metavar var b end metavar suc plus metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar plus metavar var b end metavar suc conclude metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar suc plus metavar var b end metavar suc cut prop three two j conclude metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc cut prop three two c modus ponens metavar var a end metavar suc times metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc conclude metavar var a end metavar suc times metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc cut prop three two c modus ponens metavar var a end metavar suc times metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar suc plus metavar var b end metavar suc conclude metavar var a end metavar suc times metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar suc plus metavar var b end metavar suc cut prop three two c modus ponens metavar var a end metavar suc times metavar var b end metavar suc equal metavar var a end metavar suc times metavar var b end metavar plus metavar var a end metavar suc modus ponens metavar var a end metavar suc times metavar var b end metavar plus metavar var a end metavar suc equal metavar var a end metavar times metavar var b end metavar suc plus metavar var b end metavar suc conclude metavar var a end metavar suc times metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar suc plus metavar var b end metavar suc cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar suc times metavar var b end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar infer metavar var a end metavar suc times metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar suc plus metavar var b end metavar suc conclude metavar var a end metavar suc times metavar var b end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar imply metavar var a end metavar suc times metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar suc plus metavar var b end metavar suc end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three two m as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar suc times metavar var b end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar end define end math ] "



\item " [ math define proof of prop three two m as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed prop three two m one conclude object var var x end var suc times zero equal object var var x end var times zero plus zero cut prop three two m two conclude object var var x end var suc times object var var y end var equal object var var x end var times object var var y end var plus object var var y end var imply object var var x end var suc times object var var y end var suc equal object var var x end var times object var var y end var suc plus object var var y end var suc cut axiom s nine at object var var y end var modus ponens object var var x end var suc times zero equal object var var x end var times zero plus zero modus ponens object var var x end var suc times object var var y end var equal object var var x end var times object var var y end var plus object var var y end var imply object var var x end var suc times object var var y end var suc equal object var var x end var times object var var y end var suc plus object var var y end var suc conclude object var var x end var suc times object var var y end var equal object var var x end var times object var var y end var plus object var var y end var cut deduction modus ponens object var var x end var suc times object var var y end var equal object var var x end var times object var var y end var plus object var var y end var conclude metavar var a end metavar suc times metavar var b end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "

\end{list}


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

\item " [ math define statement of prop three two n one as system s infer all metavar var a end metavar indeed metavar var a end metavar times zero equal zero times metavar var a end metavar end define end math ] "

\item " [ math define proof of prop three two n one as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed axiom s seven conclude metavar var a end metavar times zero equal zero cut prop three two l conclude zero times metavar var a end metavar equal zero cut prop three two d modus ponens metavar var a end metavar times zero equal zero modus ponens zero times metavar var a end metavar equal zero conclude metavar var a end metavar times zero equal zero times metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three two n two as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar equal metavar var b end metavar times metavar var a end metavar imply metavar var a end metavar times metavar var b end metavar suc equal metavar var b end metavar suc times metavar var a end metavar end define end math ] "

\item " [ math define proof of prop three two n two as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar equal metavar var b end metavar times metavar var a end metavar infer axiom s eight conclude metavar var a end metavar times metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar cut prop three two e modus ponens metavar var a end metavar times metavar var b end metavar equal metavar var b end metavar times metavar var a end metavar conclude metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar equal metavar var b end metavar times metavar var a end metavar plus metavar var a end metavar cut prop three two m conclude metavar var b end metavar suc times metavar var a end metavar equal metavar var b end metavar times metavar var a end metavar plus metavar var a end metavar cut prop three two b modus ponens metavar var b end metavar suc times metavar var a end metavar equal metavar var b end metavar times metavar var a end metavar plus metavar var a end metavar conclude metavar var b end metavar times metavar var a end metavar plus metavar var a end metavar equal metavar var b end metavar suc times metavar var a end metavar cut prop three two c modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar equal metavar var b end metavar times metavar var a end metavar plus metavar var a end metavar modus ponens metavar var b end metavar times metavar var a end metavar plus metavar var a end metavar equal metavar var b end metavar suc times metavar var a end metavar conclude metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar equal metavar var b end metavar suc times metavar var a end metavar cut prop three two c modus ponens metavar var a end metavar times metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar equal metavar var b end metavar suc times metavar var a end metavar conclude metavar var a end metavar times metavar var b end metavar suc equal metavar var b end metavar suc times metavar var a end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar equal metavar var b end metavar times metavar var a end metavar infer metavar var a end metavar times metavar var b end metavar suc equal metavar var b end metavar suc times metavar var a end metavar conclude metavar var a end metavar times metavar var b end metavar equal metavar var b end metavar times metavar var a end metavar imply metavar var a end metavar times metavar var b end metavar suc equal metavar var b end metavar suc times metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "
\item " [ math define statement of prop three two n as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar equal metavar var b end metavar times metavar var a end metavar end define end math ] "


\item " [ math define proof of prop three two n as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed prop three two n one conclude object var var x end var times zero equal zero times object var var x end var cut prop three two n two conclude object var var x end var times object var var y end var equal object var var y end var times object var var x end var imply object var var x end var times object var var y end var suc equal object var var y end var suc times object var var x end var cut axiom s nine at object var var y end var modus ponens object var var x end var times zero equal zero times object var var x end var modus ponens object var var x end var times object var var y end var equal object var var y end var times object var var x end var imply object var var x end var times object var var y end var suc equal object var var y end var suc times object var var x end var conclude object var var x end var times object var var y end var equal object var var y end var times object var var x end var cut deduction modus ponens object var var x end var times object var var y end var equal object var var y end var times object var var x end var conclude metavar var a end metavar times metavar var b end metavar equal metavar var b end metavar times metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "

\end{list}


\subsection{3.2o}
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math define statement of prop three two o as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var c end metavar times metavar var a end metavar equal metavar var c end metavar times metavar var b end metavar end define end math ] "

\item " [ math define proof of prop three two o as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer prop three two k modus ponens metavar var a end metavar equal metavar var b end metavar conclude metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar cut prop three two n conclude metavar var a end metavar times metavar var c end metavar equal metavar var c end metavar times metavar var a end metavar cut prop three two n conclude metavar var b end metavar times metavar var c end metavar equal metavar var c end metavar times metavar var b end metavar cut prop three two c modus ponens metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar modus ponens metavar var b end metavar times metavar var c end metavar equal metavar var c end metavar times metavar var b end metavar conclude metavar var a end metavar times metavar var c end metavar equal metavar var c end metavar times metavar var b end metavar cut axiom s one modus ponens metavar var a end metavar times metavar var c end metavar equal metavar var c end metavar times metavar var a end metavar modus ponens metavar var a end metavar times metavar var c end metavar equal metavar var c end metavar times metavar var b end metavar conclude metavar var c end metavar times metavar var a end metavar equal metavar var c end metavar times metavar var b end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var c end metavar times metavar var a end metavar equal metavar var c end metavar times metavar var b end metavar conclude metavar var a end metavar equal metavar var b end metavar imply metavar var c end metavar times metavar var a end metavar equal metavar var c end metavar times metavar var b end metavar cut rule mp modus ponens metavar var a end metavar equal metavar var b end metavar imply metavar var c end metavar times metavar var a end metavar equal metavar var c end metavar times metavar var b end metavar modus ponens metavar var a end metavar equal metavar var b end metavar conclude metavar var c end metavar times metavar var a end metavar equal metavar var c end metavar times metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "

\end{list}

\section{Udsagn 3.4}
De f\o{}lgende udsagn er en udvidelse af egenskaberne ved addition og
multiplikation.

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

\item " [ math define statement of prop three four a as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar end define end math ] "

\item " [ math define statement of prop three four b as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var b end metavar plus metavar var c end metavar times metavar var a end metavar equal metavar var b end metavar times metavar var a end metavar plus metavar var c end metavar times metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three four c as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar times metavar var b end metavar times metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar end define end math ] "

\item " [ math define statement of prop three four d as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar imply metavar var a end metavar equal metavar var b end metavar end define end math ] "

\end{list}

\subsection{3.4a}

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

\item " [ math define statement of prop three four a one as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar plus zero equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times zero end define end math ] "

\item " [ math define proof of prop three four a one as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed axiom s five conclude metavar var b end metavar plus zero equal metavar var b end metavar cut prop three two o modus ponens metavar var b end metavar plus zero equal metavar var b end metavar conclude metavar var a end metavar times metavar var b end metavar plus zero equal metavar var a end metavar times metavar var b end metavar cut axiom s five conclude metavar var a end metavar times metavar var b end metavar plus zero equal metavar var a end metavar times metavar var b end metavar cut prop three two d modus ponens metavar var a end metavar times metavar var b end metavar plus zero equal metavar var a end metavar times metavar var b end metavar modus ponens metavar var a end metavar times metavar var b end metavar plus zero equal metavar var a end metavar times metavar var b end metavar conclude metavar var a end metavar times metavar var b end metavar plus zero equal metavar var a end metavar times metavar var b end metavar plus zero cut axiom s seven conclude metavar var a end metavar times zero equal zero cut prop three two i modus ponens metavar var a end metavar times zero equal zero conclude metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times zero equal metavar var a end metavar times metavar var b end metavar plus zero cut prop three two d modus ponens metavar var a end metavar times metavar var b end metavar plus zero equal metavar var a end metavar times metavar var b end metavar plus zero modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times zero equal metavar var a end metavar times metavar var b end metavar plus zero conclude metavar var a end metavar times metavar var b end metavar plus zero equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times zero end quote state proof state cache var c end expand end define end math ] "



\item " [ math define statement of prop three four a two as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar imply metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar suc end define end math ] "

\item " [ math define proof of prop three four a two as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar infer axiom s six conclude metavar var b end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc cut prop three two o modus ponens metavar var b end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc conclude metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar suc cut axiom s eight conclude metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar plus metavar var a end metavar cut prop three two e modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar conclude metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar plus metavar var a end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar cut prop three two j conclude metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar cut prop three two c modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar plus metavar var a end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar conclude metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar plus metavar var a end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar cut axiom s eight conclude metavar var a end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar cut prop three two i modus ponens metavar var a end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar conclude metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar cut prop three two d modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar plus metavar var a end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar plus metavar var a end metavar conclude metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar plus metavar var a end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar suc cut prop three two c modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar plus metavar var a end metavar modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar plus metavar var a end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar suc conclude metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar suc cut prop three two c modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar suc modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar suc conclude metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar suc cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar infer metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar suc conclude metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar imply metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar suc end quote state proof state cache var c end expand end define end math ] "
\item " [ math define statement of prop three four a as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar end define end math ] "

\item " [ math define proof of prop three four a as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed prop three four a one conclude object var var x end var times object var var y end var plus zero equal object var var x end var times object var var y end var plus object var var x end var times zero cut prop three four a two conclude object var var x end var times object var var y end var plus object var var z end var equal object var var x end var times object var var y end var plus object var var x end var times object var var z end var imply object var var x end var times object var var y end var plus object var var z end var suc equal object var var x end var times object var var y end var plus object var var x end var times object var var z end var suc cut axiom s nine at object var var z end var modus ponens object var var x end var times object var var y end var plus zero equal object var var x end var times object var var y end var plus object var var x end var times zero modus ponens object var var x end var times object var var y end var plus object var var z end var equal object var var x end var times object var var y end var plus object var var x end var times object var var z end var imply object var var x end var times object var var y end var plus object var var z end var suc equal object var var x end var times object var var y end var plus object var var x end var times object var var z end var suc conclude object var var x end var times object var var y end var plus object var var z end var equal object var var x end var times object var var y end var plus object var var x end var times object var var z end var cut deduction modus ponens object var var x end var times object var var y end var plus object var var z end var equal object var var x end var times object var var y end var plus object var var x end var times object var var z end var conclude metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar end quote state proof state cache var c end expand end define end math ] "

\end{list}

\subsection{3.4b}

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

\item " [ math define statement of prop three four b as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var b end metavar plus metavar var c end metavar times metavar var a end metavar equal metavar var b end metavar times metavar var a end metavar plus metavar var c end metavar times metavar var a end metavar end define end math ] "

\item " [ math define proof of prop three four b as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed prop three four a conclude metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar cut prop three two n conclude metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar times metavar var a end metavar cut prop three two n conclude metavar var a end metavar times metavar var b end metavar equal metavar var b end metavar times metavar var a end metavar cut prop three two n conclude metavar var a end metavar times metavar var c end metavar equal metavar var c end metavar times metavar var a end metavar cut axiom s one modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar times metavar var a end metavar modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar conclude metavar var b end metavar plus metavar var c end metavar times metavar var a end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar cut prop three two e modus ponens metavar var a end metavar times metavar var b end metavar equal metavar var b end metavar times metavar var a end metavar conclude metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var a end metavar plus metavar var a end metavar times metavar var c end metavar cut prop three two i modus ponens metavar var a end metavar times metavar var c end metavar equal metavar var c end metavar times metavar var a end metavar conclude metavar var b end metavar times metavar var a end metavar plus metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var a end metavar plus metavar var c end metavar times metavar var a end metavar cut prop three two c modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var a end metavar plus metavar var a end metavar times metavar var c end metavar modus ponens metavar var b end metavar times metavar var a end metavar plus metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var a end metavar plus metavar var c end metavar times metavar var a end metavar conclude metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var a end metavar plus metavar var c end metavar times metavar var a end metavar cut prop three two c modus ponens metavar var b end metavar plus metavar var c end metavar times metavar var a end metavar equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var a end metavar plus metavar var c end metavar times metavar var a end metavar conclude metavar var b end metavar plus metavar var c end metavar times metavar var a end metavar equal metavar var b end metavar times metavar var a end metavar plus metavar var c end metavar times metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "


\end{list}

\subsection{3.4c}

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

\item " [ math define statement of prop three four c one as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar times zero equal metavar var a end metavar times metavar var b end metavar times zero end define end math ] "

\item " [ math define proof of prop three four c one as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed axiom s seven conclude metavar var a end metavar times metavar var b end metavar times zero equal zero cut axiom s seven conclude metavar var b end metavar times zero equal zero cut prop three two o modus ponens metavar var b end metavar times zero equal zero conclude metavar var a end metavar times metavar var b end metavar times zero equal metavar var a end metavar times zero cut axiom s seven conclude metavar var a end metavar times zero equal zero cut prop three two c modus ponens metavar var a end metavar times metavar var b end metavar times zero equal metavar var a end metavar times zero modus ponens metavar var a end metavar times zero equal zero conclude metavar var a end metavar times metavar var b end metavar times zero equal zero cut prop three two d modus ponens metavar var a end metavar times metavar var b end metavar times zero equal zero modus ponens metavar var a end metavar times metavar var b end metavar times zero equal zero conclude metavar var a end metavar times metavar var b end metavar times zero equal metavar var a end metavar times metavar var b end metavar times zero end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three four c two as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar times metavar var b end metavar times metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar imply metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc end define end math ] "

\item " [ math define proof of prop three four c two as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar times metavar var b end metavar times metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar infer axiom s eight conclude metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar times metavar var b end metavar cut prop three two e modus ponens metavar var a end metavar times metavar var b end metavar times metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar conclude metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar times metavar var b end metavar equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar times metavar var b end metavar cut prop three two c modus ponens metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar times metavar var b end metavar modus ponens metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar times metavar var b end metavar equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar times metavar var b end metavar conclude metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar times metavar var b end metavar cut prop three four a conclude metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar times metavar var b end metavar cut prop three two d modus ponens metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar times metavar var b end metavar modus ponens metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var a end metavar times metavar var b end metavar conclude metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar cut axiom s eight conclude metavar var b end metavar times metavar var c end metavar suc equal metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar cut prop three two o modus ponens metavar var b end metavar times metavar var c end metavar suc equal metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar conclude metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar cut prop three two d modus ponens metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar modus ponens metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar plus metavar var b end metavar conclude metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar times metavar var b end metavar times metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar infer metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc conclude metavar var a end metavar times metavar var b end metavar times metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar imply metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar suc end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three four c as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar times metavar var b end metavar times metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar end define end math ] "

\item " [ math define proof of prop three four c as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed prop three four c one conclude object var var x end var times object var var y end var times zero equal object var var x end var times object var var y end var times zero cut prop three four c two conclude object var var x end var times object var var y end var times object var var z end var equal object var var x end var times object var var y end var times object var var z end var imply object var var x end var times object var var y end var times object var var z end var suc equal object var var x end var times object var var y end var times object var var z end var suc cut axiom s nine at object var var z end var modus ponens object var var x end var times object var var y end var times zero equal object var var x end var times object var var y end var times zero modus ponens object var var x end var times object var var y end var times object var var z end var equal object var var x end var times object var var y end var times object var var z end var imply object var var x end var times object var var y end var times object var var z end var suc equal object var var x end var times object var var y end var times object var var z end var suc conclude object var var x end var times object var var y end var times object var var z end var equal object var var x end var times object var var y end var times object var var z end var cut deduction modus ponens object var var x end var times object var var y end var times object var var z end var equal object var var x end var times object var var y end var times object var var z end var conclude metavar var a end metavar times metavar var b end metavar times metavar var c end metavar equal metavar var a end metavar times metavar var b end metavar times metavar var c end metavar end quote state proof state cache var c end expand end define end math ] "

\end{list}

\subsection{3.4d}

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

\item " [ math define statement of prop three four d one as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus zero equal metavar var b end metavar plus zero imply metavar var a end metavar equal metavar var b end metavar end define end math ] "

\item " [ math define proof of prop three four d one as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus zero equal metavar var b end metavar plus zero infer axiom s five conclude metavar var a end metavar plus zero equal metavar var a end metavar cut axiom s five conclude metavar var b end metavar plus zero equal metavar var b end metavar cut axiom s one modus ponens metavar var a end metavar plus zero equal metavar var a end metavar modus ponens metavar var a end metavar plus zero equal metavar var b end metavar plus zero conclude metavar var a end metavar equal metavar var b end metavar plus zero cut prop three two c modus ponens metavar var a end metavar equal metavar var b end metavar plus zero modus ponens metavar var b end metavar plus zero equal metavar var b end metavar conclude metavar var a end metavar equal metavar var b end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus zero equal metavar var b end metavar plus zero infer metavar var a end metavar equal metavar var b end metavar conclude metavar var a end metavar plus zero equal metavar var b end metavar plus zero imply metavar var a end metavar equal metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three four d two as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar imply metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc imply metavar var a end metavar equal metavar var b end metavar end define end math ] "


\item " [ math define proof of prop three four d two as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar imply metavar var a end metavar equal metavar var b end metavar infer metavar var a end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc infer axiom s six conclude metavar var a end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var c end metavar suc cut axiom s six conclude metavar var b end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc cut axiom s one modus ponens metavar var a end metavar plus metavar var c end metavar suc equal metavar var a end metavar plus metavar var c end metavar suc modus ponens metavar var a end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc conclude metavar var a end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc cut prop three two c modus ponens metavar var a end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc modus ponens metavar var b end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc conclude metavar var a end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc cut axiom s four modus ponens metavar var a end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc conclude metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar cut rule mp modus ponens metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar imply metavar var a end metavar equal metavar var b end metavar modus ponens metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar conclude metavar var a end metavar equal metavar var b end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar imply metavar var a end metavar equal metavar var b end metavar infer metavar var a end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc infer metavar var a end metavar equal metavar var b end metavar conclude metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar imply metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar plus metavar var c end metavar suc equal metavar var b end metavar plus metavar var c end metavar suc imply metavar var a end metavar equal metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three four d as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar imply metavar var a end metavar equal metavar var b end metavar end define end math ] "

\item " [ math define proof of prop three four d as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed prop three four d one conclude object var var x end var plus zero equal object var var y end var plus zero imply object var var x end var equal object var var y end var cut prop three four d two conclude object var var x end var plus object var var z end var equal object var var y end var plus object var var z end var imply object var var x end var equal object var var y end var imply object var var x end var plus object var var z end var suc equal object var var y end var plus object var var z end var suc imply object var var x end var equal object var var y end var cut axiom s nine at object var var z end var modus ponens object var var x end var plus zero equal object var var y end var plus zero imply object var var x end var equal object var var y end var modus ponens object var var x end var plus object var var z end var equal object var var y end var plus object var var z end var imply object var var x end var equal object var var y end var imply object var var x end var plus object var var z end var suc equal object var var y end var plus object var var z end var suc imply object var var x end var equal object var var y end var conclude object var var x end var plus object var var z end var equal object var var y end var plus object var var z end var imply object var var x end var equal object var var y end var cut deduction modus ponens object var var x end var plus object var var z end var equal object var var y end var plus object var var z end var imply object var var x end var equal object var var y end var conclude metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar imply metavar var a end metavar equal metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "

\end{list}

\section{Udsagn 3.5}\label{35}
I denne del har vi kun kunne l\o{}se indtil h, da denne og de efterf\o{}lgende
kr\ae{}ver reglen ``existensial rule''. Dog er der i afsnit \ref{exist} genemg\aa{}et hvilket problem der forhindrer os i at bevise '' existencial rule'', og hvordan vi
ville have bevist reglen, hvis problemet ikke var opst\aa{}et. Endvidere er der i \ref{exist} genemg\aa{}et hvordan vi ville have l\o{}st 3.5h.

I de f\o{}lgende udsagn indg\aa{}r numeraler opf\o{}rer sig som de naturlige
tal og er defineret i forhold til 0 p\aa{} f\o{}lgende m\aa{}de:

\[
\begin{array}{lcr}
0 &=& \overline{0} \\
0' &=& \overline{1} \\
0'' & = & \overline{2} \\
\vdots & & \vdots \\
0^{n*'} & = & \overline{n} \\
\end{array}
\]

Dvs. hvis $\overline{0}$ er et numeral, og hvis $\overline{n}$ er et numeral, s\aa{} er $\overline{n}'$ ogs\aa{}.\\

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

\item " [ math define statement of prop three five a as system s infer all metavar var a end metavar indeed metavar var a end metavar plus zero suc equal metavar var a end metavar suc end define end math ] "

\item " [ math define statement of prop three five b as system s infer all metavar var a end metavar indeed metavar var a end metavar times zero suc equal metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three five c as system s infer all metavar var a end metavar indeed metavar var a end metavar times zero suc suc equal metavar var a end metavar plus metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three five d as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero end define end math ] "

\item " [ math define statement of prop three five e as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar equal zero imply metavar var a end metavar times metavar var b end metavar equal zero imply metavar var a end metavar equal zero end define end math ] "

\item " [ math define statement of prop three five f as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar equal zero suc imply not not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero end define end math ] "

\item " [ math define statement of prop three five g as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero suc end define end math ] "

\item " [ math define statement of prop three five h as system s infer all metavar var a end metavar indeed not metavar var a end metavar equal zero imply not for all objects metavar var b end metavar indeed not metavar var a end metavar equal metavar var b end metavar suc end define end math ] "

\item " [ math define statement of prop three five i as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not metavar var c end metavar equal zero imply metavar var a end metavar times metavar var c end metavar equal metavar var b end metavar times metavar var c end metavar imply metavar var a end metavar equal metavar var b end metavar end define end math ] "

\item " [ math define statement of prop three five j as system s infer all metavar var a end metavar indeed not metavar var a end metavar equal zero imply not metavar var a end metavar equal zero suc imply not for all objects metavar var b end metavar indeed not metavar var a end metavar equal metavar var b end metavar suc suc end define end math ] "

\end{list}

Efterf\o[]lgende vil vi gennemg\aa de n\o[]dvendige hj\ae{}lpes\ae{}tninger og definitioner for at kunne bevise 3.5a-3.5g.

\subsection{Definitioner i forbindelse med $\land$ og $\lor$}

Fra 3.5d bruges $\land$ og $\lor$, som begge er makrodefinerede udtryk.

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math define macro of var x and1 var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x and1 var y as not parenthesis var x imply not var y end parenthesis end define end quote end define end define end math ] "
\item " [ math define macro of var x or1 var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x or1 var y as parenthesis not var x end parenthesis imply var y end define end quote end define end define end math ] "
\end{list}

Endvidere er det klart at reglerne for introduktion og eliminering af $\land$ og
$\lor$ dermed ogs\aa{} skal bruges. Alle disse er bevist i de f\o{}lgende afsnit.

\subsubsection{Introduktion af $\land$}

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

\item " [ math define statement of conjin as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer metavar var b end metavar infer not metavar var a end metavar imply not metavar var b end metavar end define end math ] "

\item " [ math define proof of conjin as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer metavar var b end metavar infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply not metavar var b end metavar infer repetition modus ponens metavar var a end metavar conclude metavar var a end metavar cut rule mp modus ponens metavar var a end metavar imply not metavar var b end metavar modus ponens metavar var a end metavar conclude not metavar var b end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply not metavar var b end metavar infer not metavar var b end metavar conclude metavar var a end metavar imply not metavar var b end metavar imply not metavar var b end metavar cut h two conclude metavar var b end metavar imply not not metavar var b end metavar cut rule mp modus ponens metavar var b end metavar imply not not metavar var b end metavar modus ponens metavar var b end metavar conclude not not metavar var b end metavar cut modus tollens modus ponens metavar var a end metavar imply not metavar var b end metavar imply not metavar var b end metavar modus ponens not not metavar var b end metavar conclude not metavar var a end metavar imply not metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "

\end{list}

\subsubsection{Elimination af $\land$ 1}
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item " [ math define statement of conjel1 as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar imply not metavar var b end metavar infer metavar var a end metavar end define end math ] "
\item " [ math define proof of conjel1 as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar imply not metavar var b end metavar infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar infer lemma a one conclude not metavar var a end metavar imply not not metavar var b end metavar imply not metavar var a end metavar cut rule mp modus ponens not metavar var a end metavar imply not not metavar var b end metavar imply not metavar var a end metavar modus ponens not metavar var a end metavar conclude not not metavar var b end metavar imply not metavar var a end metavar cut h eight conclude not not metavar var b end metavar imply not metavar var a end metavar imply metavar var a end metavar imply not metavar var b end metavar cut rule mp modus ponens not not metavar var b end metavar imply not metavar var a end metavar imply metavar var a end metavar imply not metavar var b end metavar modus ponens not not metavar var b end metavar imply not metavar var a end metavar conclude metavar var a end metavar imply not metavar var b end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar infer metavar var a end metavar imply not metavar var b end metavar conclude not metavar var a end metavar imply metavar var a end metavar imply not metavar var b end metavar cut modus tollens modus ponens not metavar var a end metavar imply metavar var a end metavar imply not metavar var b end metavar modus ponens not metavar var a end metavar imply not metavar var b end metavar conclude not not metavar var a end metavar cut h one conclude not not metavar var a end metavar imply metavar var a end metavar cut rule mp modus ponens not not metavar var a end metavar imply metavar var a end metavar modus ponens not not metavar var a end metavar conclude metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "


\end{list}

\subsubsection{Elimination af $\land$ 2}
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item " [ math define statement of conjel2 as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar imply not metavar var b end metavar infer metavar var b end metavar end define end math ] "

\item " [ math define proof of conjel2 as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar imply not metavar var b end metavar infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar infer lemma a one conclude not metavar var b end metavar imply metavar var a end metavar imply not metavar var b end metavar cut rule mp modus ponens not metavar var b end metavar imply metavar var a end metavar imply not metavar var b end metavar modus ponens not metavar var b end metavar conclude metavar var a end metavar imply not metavar var b end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar infer metavar var a end metavar imply not metavar var b end metavar conclude not metavar var b end metavar imply metavar var a end metavar imply not metavar var b end metavar cut modus tollens modus ponens not metavar var b end metavar imply metavar var a end metavar imply not metavar var b end metavar modus ponens not metavar var a end metavar imply not metavar var b end metavar conclude not not metavar var b end metavar cut h one conclude not not metavar var b end metavar imply metavar var b end metavar cut rule mp modus ponens not not metavar var b end metavar imply metavar var b end metavar modus ponens not not metavar var b end metavar conclude metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "

\end{list}

\subsubsection{Introduktion af $\lor$ 1}
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item " [ math define statement of disjin1 as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer not metavar var a end metavar imply metavar var b end metavar end define end math ] "
\item " [ math define proof of disjin1 as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer t one conclude not not metavar var a end metavar imply not metavar var a end metavar imply metavar var b end metavar cut h two conclude metavar var a end metavar imply not not metavar var a end metavar cut rule mp modus ponens metavar var a end metavar imply not not metavar var a end metavar modus ponens metavar var a end metavar conclude not not metavar var a end metavar cut rule mp modus ponens not not metavar var a end metavar imply not metavar var a end metavar imply metavar var b end metavar modus ponens not not metavar var a end metavar conclude not metavar var a end metavar imply metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "


\end{list}

\subsubsection{Introduktion af $\lor$ 2}

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

\item " [ math define statement of disjin2 as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var b end metavar infer not metavar var a end metavar imply metavar var b end metavar end define end math ] "

\item " [ math define proof of disjin2 as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var b end metavar infer lemma a one conclude metavar var b end metavar imply not metavar var a end metavar imply metavar var b end metavar cut rule mp modus ponens metavar var b end metavar imply not metavar var a end metavar imply metavar var b end metavar modus ponens metavar var b end metavar conclude not metavar var a end metavar imply metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "
\end{list}

\subsubsection{Elimination af $\lor$ }

Da vi ikke har haft brug for at fjerne $\lor$, har vi ikke bevist denne regel.


\subsection{Andre hj\ae{}lpes\ae{}tninger}
Vi har til beviset af 3.5a-3.5g haft brug for nogle af reglerne fra
\cite{check}, dog med \texttt{imply} istedet for
\texttt{infer}. S\aa{}danne regler er navngivet med det $<$oprindelige
navn$>$' og beviserne for disse kan ses i Appendix \ref{help}. \\

\subsubsection{ $\mathcal{A} \neq \mathcal{B}$}
En ny hj\ae{}lperegel er \textbf{regel " [ math h three end math ] " }, som skal bruges i forbindelse med
$\mathcal{A} \neq \mathcal{B}$ for at kunne konkludere sammenh\ae{}nge i
mellem $(x = y)$ $\land$ $(x \neq 3)$ $\Rightarrow$ $(y \neq 3)$.\\

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

\item " [ math define statement of h three as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar infer metavar var a end metavar infer not metavar var c end metavar infer not metavar var b end metavar end define end math ] "

\item " [ math define proof of h three as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar infer metavar var a end metavar infer not metavar var c end metavar infer rule mp modus ponens metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar modus ponens metavar var a end metavar conclude metavar var b end metavar imply metavar var c end metavar cut modus tollens modus ponens metavar var b end metavar imply metavar var c end metavar modus ponens not metavar var c end metavar conclude not metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "
\end{list}

\subsubsection{$\exists$ x}\label{exist}
Selv om vi ikke har n\aa{}et at implementere fra opgave 3.5h, hvor der
g\o{}res brug af $\exists$, har vi alligevel makrodefineret kvantoren som
f\o{}lger.

" [ math define macro of exists var x indeed var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define exists var x indeed var y as not parenthesis for all var x indeed not var y end parenthesis end define end quote end define end define end math ] "

Vores problem har v\ae{}ret, at vi ikke har kunne udtrykke
\emph{``$\mathcal{B}(x,t)$, hvor $t$ kan inds\ae{}ttes i stedet for $x$'erne uden at
blive bundet til en alkvantor''}, i pyk.

Beviset for hj\ae{}lpes\ae{}tningen, der indf\o{}rer eksistenskvantoren, ville dog have v\ae{}ret opbygget
nogenlunde som f\o{}lger.\\

F\o{}lgende tautologi,
\[( \mathcal{A} \Rightarrow \lnot \mathcal{B})
\Rightarrow (\mathcal{B} \Rightarrow \lnot \mathcal{A})\]

antages vist nogenlunde som Modus Tollens, dog med variation.


Ved axiom " [ math lemma a four end math ] " kan vi f\aa{} instansen: \[(\forall x) \lnot
\mathcal{A}(x,t) \Rightarrow \lnot A(t,t) \]

Idet man kan f\aa{} f\o{}lgende instans af tautologien:
\[
\big( (\forall x) \lnot \mathcal{A}(x,t) \Rightarrow \lnot A(t,t) \big)
\Rightarrow
\big(A(t,t) \Rightarrow \lnot (\forall x) \lnot \mathcal{A}(x,t)\big)
\]

kan man vha. MP p\aa{} instansen og axiomet f\aa{}:
\[\big(A(t,t) \Rightarrow \lnot (\forall x) \lnot \mathcal{A}(x,t)\big)
\]

og pga. af makrodefinitionen er denne nu vist.

Herefter vises Lemmaerne 3.5a-3.5g
\subsection{3.5a}


\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math define statement of prop three five a as system s infer all metavar var a end metavar indeed metavar var a end metavar plus zero suc equal metavar var a end metavar suc end define end math ] "


\item " [ math define proof of prop three five a as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed axiom s six conclude metavar var a end metavar plus zero suc equal metavar var a end metavar plus zero suc cut axiom s five conclude metavar var a end metavar plus zero equal metavar var a end metavar cut axiom s two modus ponens metavar var a end metavar plus zero equal metavar var a end metavar conclude metavar var a end metavar plus zero suc equal metavar var a end metavar suc cut prop three two c modus ponens metavar var a end metavar plus zero suc equal metavar var a end metavar plus zero suc modus ponens metavar var a end metavar plus zero suc equal metavar var a end metavar suc conclude metavar var a end metavar plus zero suc equal metavar var a end metavar suc cut prop three two a conclude metavar var a end metavar plus zero suc equal metavar var a end metavar plus zero suc cut axiom s one modus ponens metavar var a end metavar plus zero suc equal metavar var a end metavar plus zero suc modus ponens metavar var a end metavar plus zero suc equal metavar var a end metavar suc conclude metavar var a end metavar plus zero suc equal metavar var a end metavar suc end quote state proof state cache var c end expand end define end math ] "
\end{list}
\subsection{3.5b}

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math define statement of prop three five b as system s infer all metavar var a end metavar indeed metavar var a end metavar times zero suc equal metavar var a end metavar end define end math ] "



\item " [ math define proof of prop three five b as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed axiom s eight conclude metavar var a end metavar times zero suc equal metavar var a end metavar times zero plus metavar var a end metavar cut axiom s seven conclude metavar var a end metavar times zero equal zero cut prop three two e modus ponens metavar var a end metavar times zero equal zero conclude metavar var a end metavar times zero plus metavar var a end metavar equal zero plus metavar var a end metavar cut prop three two c modus ponens metavar var a end metavar times zero suc equal metavar var a end metavar times zero plus metavar var a end metavar modus ponens metavar var a end metavar times zero plus metavar var a end metavar equal zero plus metavar var a end metavar conclude metavar var a end metavar times zero suc equal zero plus metavar var a end metavar cut prop three two f conclude metavar var a end metavar equal zero plus metavar var a end metavar cut prop three two b modus ponens metavar var a end metavar equal zero plus metavar var a end metavar conclude zero plus metavar var a end metavar equal metavar var a end metavar cut prop three two c modus ponens metavar var a end metavar times zero suc equal zero plus metavar var a end metavar modus ponens zero plus metavar var a end metavar equal metavar var a end metavar conclude metavar var a end metavar times zero suc equal metavar var a end metavar cut prop three two a conclude metavar var a end metavar times zero suc equal metavar var a end metavar times zero suc cut axiom s one modus ponens metavar var a end metavar times zero suc equal metavar var a end metavar times zero suc modus ponens metavar var a end metavar times zero suc equal metavar var a end metavar conclude metavar var a end metavar times zero suc equal metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "
\end{list}
\subsection{3.5c}

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

\item " [ math define statement of prop three five c as system s infer all metavar var a end metavar indeed metavar var a end metavar times zero suc suc equal metavar var a end metavar plus metavar var a end metavar end define end math ] "


\item " [ math define proof of prop three five c as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed axiom s eight conclude metavar var a end metavar times zero suc suc equal metavar var a end metavar times zero suc plus metavar var a end metavar cut prop three five b conclude metavar var a end metavar times zero suc equal metavar var a end metavar cut prop three two e modus ponens metavar var a end metavar times zero suc equal metavar var a end metavar conclude metavar var a end metavar times zero suc plus metavar var a end metavar equal metavar var a end metavar plus metavar var a end metavar cut prop three two c modus ponens metavar var a end metavar times zero suc suc equal metavar var a end metavar times zero suc plus metavar var a end metavar modus ponens metavar var a end metavar times zero suc plus metavar var a end metavar equal metavar var a end metavar plus metavar var a end metavar conclude metavar var a end metavar times zero suc suc equal metavar var a end metavar plus metavar var a end metavar cut prop three two a conclude metavar var a end metavar times zero suc suc equal metavar var a end metavar times zero suc suc cut axiom s one modus ponens metavar var a end metavar times zero suc suc equal metavar var a end metavar times zero suc suc modus ponens metavar var a end metavar times zero suc suc equal metavar var a end metavar plus metavar var a end metavar conclude metavar var a end metavar times zero suc suc equal metavar var a end metavar plus metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "
\end{list}
\subsection{3.5d}

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


\item " [ math define statement of prop three five d one as system s infer all metavar var a end metavar indeed metavar var a end metavar plus zero equal zero imply not metavar var a end metavar equal zero imply not zero equal zero end define end math ] "


\item " [ math define proof of prop three five d one as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var a end metavar indeed metavar var a end metavar plus zero equal zero infer axiom s five conclude metavar var a end metavar plus zero equal metavar var a end metavar cut axiom s one modus ponens metavar var a end metavar plus zero equal metavar var a end metavar modus ponens metavar var a end metavar plus zero equal zero conclude metavar var a end metavar equal zero cut prop three two a conclude zero equal zero cut conjin modus ponens metavar var a end metavar equal zero modus ponens zero equal zero conclude not metavar var a end metavar equal zero imply not zero equal zero cut deduction modus ponens all metavar var a end metavar indeed metavar var a end metavar plus zero equal zero infer not metavar var a end metavar equal zero imply not zero equal zero conclude metavar var a end metavar plus zero equal zero imply not metavar var a end metavar equal zero imply not zero equal zero end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three five d two as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero imply metavar var a end metavar plus metavar var b end metavar suc equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero end define end math ] "

\item " [ math define proof of prop three five d two as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar suc equal zero infer axiom s three conclude not zero equal metavar var a end metavar plus metavar var b end metavar suc cut h nine conclude metavar var a end metavar plus metavar var b end metavar suc equal zero imply zero equal metavar var a end metavar plus metavar var b end metavar suc cut h seven conclude metavar var a end metavar plus metavar var b end metavar suc equal zero imply zero equal metavar var a end metavar plus metavar var b end metavar suc imply not zero equal metavar var a end metavar plus metavar var b end metavar suc imply not metavar var a end metavar plus metavar var b end metavar suc equal zero cut rule mp modus ponens metavar var a end metavar plus metavar var b end metavar suc equal zero imply zero equal metavar var a end metavar plus metavar var b end metavar suc imply not zero equal metavar var a end metavar plus metavar var b end metavar suc imply not metavar var a end metavar plus metavar var b end metavar suc equal zero modus ponens metavar var a end metavar plus metavar var b end metavar suc equal zero imply zero equal metavar var a end metavar plus metavar var b end metavar suc conclude not zero equal metavar var a end metavar plus metavar var b end metavar suc imply not metavar var a end metavar plus metavar var b end metavar suc equal zero cut rule mp modus ponens not zero equal metavar var a end metavar plus metavar var b end metavar suc imply not metavar var a end metavar plus metavar var b end metavar suc equal zero modus ponens not zero equal metavar var a end metavar plus metavar var b end metavar suc conclude not metavar var a end metavar plus metavar var b end metavar suc equal zero cut axiom s six conclude metavar var a end metavar plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc cut h four mark conclude metavar var a end metavar plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc imply metavar var a end metavar plus metavar var b end metavar suc equal zero imply metavar var a end metavar plus metavar var b end metavar suc equal zero cut h three modus ponens metavar var a end metavar plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc imply metavar var a end metavar plus metavar var b end metavar suc equal zero imply metavar var a end metavar plus metavar var b end metavar suc equal zero modus ponens metavar var a end metavar plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc modus ponens not metavar var a end metavar plus metavar var b end metavar suc equal zero conclude not metavar var a end metavar plus metavar var b end metavar suc equal zero cut t one conclude not metavar var a end metavar plus metavar var b end metavar suc equal zero imply metavar var a end metavar plus metavar var b end metavar suc equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero cut rule mp modus ponens not metavar var a end metavar plus metavar var b end metavar suc equal zero imply metavar var a end metavar plus metavar var b end metavar suc equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero modus ponens not metavar var a end metavar plus metavar var b end metavar suc equal zero conclude metavar var a end metavar plus metavar var b end metavar suc equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero cut rule mp modus ponens metavar var a end metavar plus metavar var b end metavar suc equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero modus ponens metavar var a end metavar plus metavar var b end metavar suc equal zero conclude not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar suc equal zero infer not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero conclude metavar var a end metavar plus metavar var b end metavar suc equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero infer metavar var a end metavar plus metavar var b end metavar suc equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero conclude metavar var a end metavar plus metavar var b end metavar equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero imply metavar var a end metavar plus metavar var b end metavar suc equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero end quote state proof state cache var c end expand end define end math ] "


\item " [ math define statement of prop three five d as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero end define end math ] "


\item " [ math define proof of prop three five d as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed prop three five d one conclude object var var x end var plus zero equal zero imply not object var var x end var equal zero imply not zero equal zero cut prop three five d two conclude object var var x end var plus object var var y end var equal zero imply not object var var x end var equal zero imply not object var var y end var equal zero imply object var var x end var plus object var var y end var suc equal zero imply not object var var x end var equal zero imply not object var var y end var suc equal zero cut axiom s nine at object var var y end var modus ponens object var var x end var plus zero equal zero imply not object var var x end var equal zero imply not zero equal zero modus ponens object var var x end var plus object var var y end var equal zero imply not object var var x end var equal zero imply not object var var y end var equal zero imply object var var x end var plus object var var y end var suc equal zero imply not object var var x end var equal zero imply not object var var y end var suc equal zero conclude object var var x end var plus object var var y end var equal zero imply not object var var x end var equal zero imply not object var var y end var equal zero cut deduction modus ponens object var var x end var plus object var var y end var equal zero imply not object var var x end var equal zero imply not object var var y end var equal zero conclude metavar var a end metavar plus metavar var b end metavar equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero end quote state proof state cache var c end expand end define end math ] "

\end{list}
\subsection{3.5e}

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


\item " [ math define statement of prop three five e one as system s infer all metavar var a end metavar indeed not zero equal zero imply metavar var a end metavar times zero equal zero imply metavar var a end metavar equal zero end define end math ] "

\item " [ math define proof of prop three five e one as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var a end metavar indeed not zero equal zero infer prop three two a conclude zero equal zero cut t one conclude not zero equal zero imply zero equal zero imply metavar var a end metavar times zero equal zero imply metavar var a end metavar equal zero cut rule mp modus ponens not zero equal zero imply zero equal zero imply metavar var a end metavar times zero equal zero imply metavar var a end metavar equal zero modus ponens not zero equal zero conclude zero equal zero imply metavar var a end metavar times zero equal zero imply metavar var a end metavar equal zero cut rule mp modus ponens zero equal zero imply metavar var a end metavar times zero equal zero imply metavar var a end metavar equal zero modus ponens zero equal zero conclude metavar var a end metavar times zero equal zero imply metavar var a end metavar equal zero cut deduction modus ponens all metavar var a end metavar indeed not zero equal zero infer metavar var a end metavar times zero equal zero imply metavar var a end metavar equal zero conclude not zero equal zero imply metavar var a end metavar times zero equal zero imply metavar var a end metavar equal zero end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three five e two as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar equal zero imply metavar var a end metavar times metavar var b end metavar equal zero imply metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero imply metavar var a end metavar times metavar var b end metavar suc equal zero imply metavar var a end metavar equal zero end define end math ] "


\item " [ math define proof of prop three five e two as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar equal zero imply metavar var a end metavar times metavar var b end metavar equal zero imply metavar var a end metavar equal zero infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar suc equal zero infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar suc equal zero infer axiom s eight conclude metavar var a end metavar times metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar cut axiom s one modus ponens metavar var a end metavar times metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar modus ponens metavar var a end metavar times metavar var b end metavar suc equal zero conclude metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar equal zero cut prop three five d conclude metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar equal zero imply not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero cut rule mp modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar equal zero imply not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar equal zero conclude not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero cut conjel2 modus ponens not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero conclude metavar var a end metavar equal zero cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar suc equal zero infer metavar var a end metavar equal zero conclude metavar var a end metavar times metavar var b end metavar suc equal zero imply metavar var a end metavar equal zero cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar suc equal zero infer metavar var a end metavar times metavar var b end metavar suc equal zero imply metavar var a end metavar equal zero conclude not metavar var b end metavar suc equal zero imply metavar var a end metavar times metavar var b end metavar suc equal zero imply metavar var a end metavar equal zero cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar equal zero imply metavar var a end metavar times metavar var b end metavar equal zero imply metavar var a end metavar equal zero infer not metavar var b end metavar suc equal zero imply metavar var a end metavar times metavar var b end metavar suc equal zero imply metavar var a end metavar equal zero conclude not metavar var b end metavar equal zero imply metavar var a end metavar times metavar var b end metavar equal zero imply metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero imply metavar var a end metavar times metavar var b end metavar suc equal zero imply metavar var a end metavar equal zero end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three five e as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar equal zero imply metavar var a end metavar times metavar var b end metavar equal zero imply metavar var a end metavar equal zero end define end math ] "


\item " [ math define proof of prop three five e as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed prop three five e one conclude not zero equal zero imply object var var x end var times zero equal zero imply object var var x end var equal zero cut prop three five e two conclude not object var var y end var equal zero imply object var var x end var times object var var y end var equal zero imply object var var x end var equal zero imply not object var var y end var suc equal zero imply object var var x end var times object var var y end var suc equal zero imply object var var x end var equal zero cut axiom s nine at object var var y end var modus ponens not zero equal zero imply object var var x end var times zero equal zero imply object var var x end var equal zero modus ponens not object var var y end var equal zero imply object var var x end var times object var var y end var equal zero imply object var var x end var equal zero imply not object var var y end var suc equal zero imply object var var x end var times object var var y end var suc equal zero imply object var var x end var equal zero conclude not object var var y end var equal zero imply object var var x end var times object var var y end var equal zero imply object var var x end var equal zero cut deduction modus ponens not object var var y end var equal zero imply object var var x end var times object var var y end var equal zero imply object var var x end var equal zero conclude not metavar var b end metavar equal zero imply metavar var a end metavar times metavar var b end metavar equal zero imply metavar var a end metavar equal zero end quote state proof state cache var c end expand end define end math ] "
\end{list}

\subsection{3.5f}

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


\item " [ math define statement of prop three five f one as system s infer all metavar var a end metavar indeed metavar var a end metavar plus zero equal zero suc imply not not metavar var a end metavar equal zero imply not zero equal zero suc imply not metavar var a end metavar equal zero suc imply not zero equal zero end define end math ] "

\item " [ math define proof of prop three five f one as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var a end metavar indeed metavar var a end metavar plus zero equal zero suc infer axiom s five conclude metavar var a end metavar plus zero equal metavar var a end metavar cut axiom s one modus ponens metavar var a end metavar plus zero equal metavar var a end metavar modus ponens metavar var a end metavar plus zero equal zero suc conclude metavar var a end metavar equal zero suc cut prop three two a conclude zero equal zero cut conjin modus ponens metavar var a end metavar equal zero suc modus ponens zero equal zero conclude not metavar var a end metavar equal zero suc imply not zero equal zero cut disjin2 modus ponens not metavar var a end metavar equal zero suc imply not zero equal zero conclude not not metavar var a end metavar equal zero imply not zero equal zero suc imply not metavar var a end metavar equal zero suc imply not zero equal zero cut deduction modus ponens all metavar var a end metavar indeed metavar var a end metavar plus zero equal zero suc infer not not metavar var a end metavar equal zero imply not zero equal zero suc imply not metavar var a end metavar equal zero suc imply not zero equal zero conclude metavar var a end metavar plus zero equal zero suc imply not not metavar var a end metavar equal zero imply not zero equal zero suc imply not metavar var a end metavar equal zero suc imply not zero equal zero end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three five f two as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar equal zero suc imply not not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero imply metavar var a end metavar plus metavar var b end metavar suc equal zero suc imply not not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero end define end math ] "

\item " [ math define proof of prop three five f two as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar equal zero suc imply not not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar suc equal zero suc infer axiom s six conclude metavar var a end metavar plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc cut axiom s one modus ponens metavar var a end metavar plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc modus ponens metavar var a end metavar plus metavar var b end metavar suc equal zero suc conclude metavar var a end metavar plus metavar var b end metavar suc equal zero suc cut axiom s four modus ponens metavar var a end metavar plus metavar var b end metavar suc equal zero suc conclude metavar var a end metavar plus metavar var b end metavar equal zero cut prop three five d conclude metavar var a end metavar plus metavar var b end metavar equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero cut rule mp modus ponens metavar var a end metavar plus metavar var b end metavar equal zero imply not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero modus ponens metavar var a end metavar plus metavar var b end metavar equal zero conclude not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero cut conjel1 modus ponens not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero conclude metavar var a end metavar equal zero cut conjel2 modus ponens not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero conclude metavar var b end metavar equal zero cut axiom s two modus ponens metavar var b end metavar equal zero conclude metavar var b end metavar suc equal zero suc cut conjin modus ponens metavar var a end metavar equal zero modus ponens metavar var b end metavar suc equal zero suc conclude not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero suc cut disjin1 modus ponens not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero suc conclude not not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar suc equal zero suc infer not not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero conclude metavar var a end metavar plus metavar var b end metavar suc equal zero suc imply not not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar equal zero suc imply not not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero infer metavar var a end metavar plus metavar var b end metavar suc equal zero suc imply not not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero conclude metavar var a end metavar plus metavar var b end metavar equal zero suc imply not not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero imply metavar var a end metavar plus metavar var b end metavar suc equal zero suc imply not not metavar var a end metavar equal zero imply not metavar var b end metavar suc equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero end quote state proof state cache var c end expand end define end math ] "
\item " [ math define statement of prop three five f as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar plus metavar var b end metavar equal zero suc imply not not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero end define end math ] "


\item " [ math define proof of prop three five f as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed prop three five f one conclude object var var x end var plus zero equal zero suc imply not not object var var x end var equal zero imply not zero equal zero suc imply not object var var x end var equal zero suc imply not zero equal zero cut prop three five f two conclude object var var x end var plus object var var y end var equal zero suc imply not not object var var x end var equal zero imply not object var var y end var equal zero suc imply not object var var x end var equal zero suc imply not object var var y end var equal zero imply object var var x end var plus object var var y end var suc equal zero suc imply not not object var var x end var equal zero imply not object var var y end var suc equal zero suc imply not object var var x end var equal zero suc imply not object var var y end var suc equal zero cut axiom s nine at object var var y end var modus ponens object var var x end var plus zero equal zero suc imply not not object var var x end var equal zero imply not zero equal zero suc imply not object var var x end var equal zero suc imply not zero equal zero modus ponens object var var x end var plus object var var y end var equal zero suc imply not not object var var x end var equal zero imply not object var var y end var equal zero suc imply not object var var x end var equal zero suc imply not object var var y end var equal zero imply object var var x end var plus object var var y end var suc equal zero suc imply not not object var var x end var equal zero imply not object var var y end var suc equal zero suc imply not object var var x end var equal zero suc imply not object var var y end var suc equal zero conclude object var var x end var plus object var var y end var equal zero suc imply not not object var var x end var equal zero imply not object var var y end var equal zero suc imply not object var var x end var equal zero suc imply not object var var y end var equal zero cut deduction modus ponens object var var x end var plus object var var y end var equal zero suc imply not not object var var x end var equal zero imply not object var var y end var equal zero suc imply not object var var x end var equal zero suc imply not object var var y end var equal zero conclude metavar var a end metavar plus metavar var b end metavar equal zero suc imply not not metavar var a end metavar equal zero imply not metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero end quote state proof state cache var c end expand end define end math ] "
\end{list}

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


\item " [ math define statement of prop three five g one as system s infer all metavar var a end metavar indeed metavar var a end metavar times zero equal zero suc imply not metavar var a end metavar equal zero suc imply not zero equal zero suc end define end math ] "

\item " [ math define proof of prop three five g one as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var a end metavar indeed metavar var a end metavar times zero equal zero suc infer axiom s seven conclude metavar var a end metavar times zero equal zero cut axiom s one modus ponens metavar var a end metavar times zero equal zero modus ponens metavar var a end metavar times zero equal zero suc conclude zero equal zero suc cut axiom s three conclude not zero equal zero suc cut t one conclude not zero equal zero suc imply zero equal zero suc imply not metavar var a end metavar equal zero suc imply not zero equal zero suc cut rule mp modus ponens not zero equal zero suc imply zero equal zero suc imply not metavar var a end metavar equal zero suc imply not zero equal zero suc modus ponens not zero equal zero suc conclude zero equal zero suc imply not metavar var a end metavar equal zero suc imply not zero equal zero suc cut rule mp modus ponens zero equal zero suc imply not metavar var a end metavar equal zero suc imply not zero equal zero suc modus ponens zero equal zero suc conclude not metavar var a end metavar equal zero suc imply not zero equal zero suc cut deduction modus ponens all metavar var a end metavar indeed metavar var a end metavar times zero equal zero suc infer not metavar var a end metavar equal zero suc imply not zero equal zero suc conclude metavar var a end metavar times zero equal zero suc imply not metavar var a end metavar equal zero suc imply not zero equal zero suc end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three five g three as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc end define end math ] "

\item " [ math define proof of prop three five g three as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero suc infer conjel2 modus ponens not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero suc conclude metavar var a end metavar equal zero suc cut conjel1 modus ponens not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero suc conclude metavar var a end metavar times metavar var b end metavar equal zero cut axiom s three conclude not zero equal zero suc cut h ten modus ponens not zero equal zero suc conclude not zero suc equal zero cut h four mark conclude metavar var a end metavar equal zero suc imply metavar var a end metavar equal zero imply zero suc equal zero cut h three modus ponens metavar var a end metavar equal zero suc imply metavar var a end metavar equal zero imply zero suc equal zero modus ponens metavar var a end metavar equal zero suc modus ponens not zero suc equal zero conclude not metavar var a end metavar equal zero cut prop three two n conclude metavar var a end metavar times metavar var b end metavar equal metavar var b end metavar times metavar var a end metavar cut axiom s one modus ponens metavar var a end metavar times metavar var b end metavar equal metavar var b end metavar times metavar var a end metavar modus ponens metavar var a end metavar times metavar var b end metavar equal zero conclude metavar var b end metavar times metavar var a end metavar equal zero cut prop three five e conclude not metavar var a end metavar equal zero imply metavar var b end metavar times metavar var a end metavar equal zero imply metavar var b end metavar equal zero cut rule mp modus ponens not metavar var a end metavar equal zero imply metavar var b end metavar times metavar var a end metavar equal zero imply metavar var b end metavar equal zero modus ponens not metavar var a end metavar equal zero conclude metavar var b end metavar times metavar var a end metavar equal zero imply metavar var b end metavar equal zero cut rule mp modus ponens metavar var b end metavar times metavar var a end metavar equal zero imply metavar var b end metavar equal zero modus ponens metavar var b end metavar times metavar var a end metavar equal zero conclude metavar var b end metavar equal zero cut axiom s two modus ponens metavar var b end metavar equal zero conclude metavar var b end metavar suc equal zero suc cut conjin modus ponens metavar var a end metavar equal zero suc modus ponens metavar var b end metavar suc equal zero suc conclude not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero suc infer not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc conclude not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of prop three five g four as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero suc infer not metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc end define end math ] "

\item " [ math define proof of prop three five g four as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero suc infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero infer conjel1 modus ponens not metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero conclude metavar var a end metavar times metavar var b end metavar equal zero suc cut rule mp modus ponens metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero suc modus ponens metavar var a end metavar times metavar var b end metavar equal zero suc conclude not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero suc cut conjel1 modus ponens not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero suc conclude metavar var a end metavar equal zero suc cut conjel2 modus ponens not metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero conclude metavar var a end metavar equal zero cut axiom s one modus ponens metavar var a end metavar equal zero modus ponens metavar var a end metavar equal zero suc conclude zero equal zero suc cut axiom s three conclude not zero equal zero suc cut t one conclude not zero equal zero suc imply zero equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc cut rule mp modus ponens not zero equal zero suc imply zero equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc modus ponens not zero equal zero suc conclude zero equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc cut rule mp modus ponens zero equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc modus ponens zero equal zero suc conclude not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero infer not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc conclude not metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc end quote state proof state cache var c end expand end define end math ] "


\item " [ math define statement of prop three five g two as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero suc imply metavar var a end metavar times metavar var b end metavar suc equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc end define end math ] "



\item " [ math define proof of prop three five g two as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero suc infer metavar var a end metavar times metavar var b end metavar suc equal zero suc infer axiom s eight conclude metavar var a end metavar times metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar cut axiom s one modus ponens metavar var a end metavar times metavar var b end metavar suc equal metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar modus ponens metavar var a end metavar times metavar var b end metavar suc equal zero suc conclude metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar equal zero suc cut prop three five f conclude metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar equal zero suc imply not not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero suc imply not metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero cut rule mp modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar equal zero suc imply not not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero suc imply not metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero modus ponens metavar var a end metavar times metavar var b end metavar plus metavar var a end metavar equal zero suc conclude not not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero suc imply not metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero cut prop three five g three conclude not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc cut prop three five g four modus ponens metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero suc conclude not metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc cut h eleven modus ponens not not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero suc imply not metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero modus ponens not metavar var a end metavar times metavar var b end metavar equal zero imply not metavar var a end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc modus ponens not metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc conclude not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero suc infer metavar var a end metavar times metavar var b end metavar suc equal zero suc infer not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc conclude metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero suc imply metavar var a end metavar times metavar var b end metavar suc equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar suc equal zero suc end quote state proof state cache var c end expand end define end math ] "
\item " [ math define statement of prop three five g as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero suc end define end math ] "


\item " [ math define proof of prop three five g as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed prop three five g one conclude object var var x end var times zero equal zero suc imply not object var var x end var equal zero suc imply not zero equal zero suc cut prop three five g two conclude object var var x end var times object var var y end var equal zero suc imply not object var var x end var equal zero suc imply not object var var y end var equal zero suc imply object var var x end var times object var var y end var suc equal zero suc imply not object var var x end var equal zero suc imply not object var var y end var suc equal zero suc cut axiom s nine at object var var y end var modus ponens object var var x end var times zero equal zero suc imply not object var var x end var equal zero suc imply not zero equal zero suc modus ponens object var var x end var times object var var y end var equal zero suc imply not object var var x end var equal zero suc imply not object var var y end var equal zero suc imply object var var x end var times object var var y end var suc equal zero suc imply not object var var x end var equal zero suc imply not object var var y end var suc equal zero suc conclude object var var x end var times object var var y end var equal zero suc imply not object var var x end var equal zero suc imply not object var var y end var equal zero suc cut deduction modus ponens object var var x end var times object var var y end var equal zero suc imply not object var var x end var equal zero suc imply not object var var y end var equal zero suc conclude metavar var a end metavar times metavar var b end metavar equal zero suc imply not metavar var a end metavar equal zero suc imply not metavar var b end metavar equal zero suc end quote state proof state cache var c end expand end define end math ] "

\end{list}
\subsection{3.5h}\label{35h}

" [ math define statement of prop three five h as system s infer all metavar var a end metavar indeed not metavar var a end metavar equal zero imply not for all objects metavar var b end metavar indeed not metavar var a end metavar equal metavar var b end metavar suc end define end math ] "

Beviset for 3.5.h ville i pyk have set ud nogenlunde som f\o{}lgende:
\[
t \neq 0 \Rightarrow (\exists y) (t = y')
\]


\subsubsection*{Part I}
\[
\begin{array}{lll}
L01 & prem & 0 \neq 0 \\
L02 & abbr. L01 & \lnot ( 0=0)\\
L03 & 3.2.a & 0 = 0 \\
L04 & Lemma 1.11.c & \lnot (0=0) \Rightarrow ((0=0) \Rightarrow (\exists w)(0=w')) \\
L05 & MP, L02, L03 & (\exists w)(0=w')\\
L06 & Ded, L05 & (0 \neq 0) \Rightarrow (\exists w)(0 = w') \\
\end{array}
\]
\subsubsection*{Part II}
\[
\begin{array}{llr}
L01: & premise & (x \neq 0) \Rightarrow (\exists w) (x = w')\\
L02: & S3'& x' \neq 0 \\
L03: & Taut.:\ \mathcal{A} \lor \lnot \mathcal{A} & (x=0)\lor \lnot(x = 0) \\
L04: &prem.& (x= 0) \\
L05: &S2'& 0'= x'\\
L06: &E4& (x=0)\Rightarrow(\exists w)(x'= w')\\
L07: &prem& \lnot(x = 0)\\
L08: & MP,L01,L07 & (\exists w) (x = w')\\
L09: & rule c& x = b'\\
L10: &S2' &(\exists w) (x' = w')\\
L11: &E4& \lnot (x = 0) \Rightarrow (\exists w)(x' = w')\\
L12 & Lemma\ H11,L06. L11 & (x' \neq 0) \Rightarrow (\exists w)(x' = w') \\
\end{array}
\]
Tilbage er blot at bruge s\ae{}tning " [ math axiom s nine end math ] " for at fuldende induktionsbeviset.

\section{Udsagn 3.7}

Vi har kun lavet de indledende definitioner, da hele 3.7 kr\ae{}ver ''existential rule''.

\subsection{Definitioner af " [ math not for all objects var z indeed not not not var z equal zero imply not var z plus object var var x end var equal object var var y end var end math ] "}

Vi har makrodefineret f\o{}lgende definitioner:

" [ math define macro of var x ist var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x ist var y as exists var z indeed parenthesis var z neq zero and1 var z plus var x equal var y end parenthesis end define end quote end define end define end math ] "

" [ math define macro of var x istq var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x istq var y as var x ist var y or1 var x equal var y end define end quote end define end define end math ] "

" [ math define macro of var x igt var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x igt var y as var y ist var x end define end quote end define end define end math ] "

" [ math define macro of var x igtq var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x igtq var y as var y istq var x end define end quote end define end define end math ] "

" [ math define macro of var x inst var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x inst var y as not parenthesis var x ist var y end parenthesis end define end quote end define end define end math ] "

" [ math define macro of var x ingt var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x ingt var y as var y inst var x end define end quote end define end define end math ] "

" [ math define macro of var x divides var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x divides var y as exists var z indeed var y equal var x times var z end define end quote end define end define end math ] "

Ved hj\ae{}lp af disse definitioner og ''existential rule'' ville 3.7 kunne bevises.

\appendix

\section{Hj\ae{}lpe lemmaer}\label{help}

Til flere af vores beviser har vi brug for nogle hj\ae{}lpe-lemmaer, disse er bevist i det f\o{}lgende afsnit
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}


\item " [ math define statement of t one as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar imply metavar var a end metavar imply metavar var b end metavar end define end math ] "

\item " [ math define statement of h zero a as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar imply metavar var b end metavar infer metavar var b end metavar imply metavar var c end metavar infer metavar var a end metavar imply metavar var c end metavar end define end math ] "

\item " [ math define statement of h zero b as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar infer metavar var b end metavar infer metavar var a end metavar imply metavar var c end metavar end define end math ] "


\item " [ math define statement of h one as system s infer all metavar var a end metavar indeed not not metavar var a end metavar imply metavar var a end metavar end define end math ] "

\item " [ math define statement of h two as system s infer all metavar var a end metavar indeed metavar var a end metavar imply not not metavar var a end metavar end define end math ] "


\item " [ math define statement of h four as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar imply metavar var b end metavar equal metavar var c end metavar imply metavar var a end metavar equal metavar var c end metavar end define end math ] "
\item " [ math define statement of h four mark as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar equal metavar var c end metavar imply metavar var b end metavar equal metavar var c end metavar end define end math ] "

\item " [ math define statement of h five as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar imply not metavar var a end metavar imply not metavar var b end metavar imply metavar var a end metavar imply metavar var b end metavar end define end math ] "

\item " [ math define statement of h six as system s infer all metavar var a end metavar indeed metavar var a end metavar imply metavar var a end metavar end define end math ] "

\item " [ math define statement of h seven as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar imply not metavar var b end metavar imply not metavar var a end metavar end define end math ] "


\item " [ math define statement of h eight as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar imply not metavar var a end metavar imply metavar var a end metavar imply metavar var b end metavar end define end math ] "

\item " [ math define statement of h nine as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar equal metavar var b end metavar imply metavar var b end metavar equal metavar var a end metavar end define end math ] "
\item " [ math define statement of h ten as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar equal metavar var a end metavar infer not metavar var a end metavar equal metavar var b end metavar end define end math ] "

\item " [ math define statement of h eleven as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not metavar var a end metavar imply metavar var b end metavar infer metavar var a end metavar imply metavar var c end metavar infer metavar var b end metavar imply metavar var c end metavar infer metavar var c end metavar end define end math ] "

\item " [ math define statement of h twelwe as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer not metavar var a end metavar imply metavar var b end metavar infer metavar var b end metavar end define end math ] "

\item " [ math define statement of modus tollens as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer not metavar var b end metavar infer not metavar var a end metavar end define end math ] "




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

\item " [ math define statement of t one as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar imply metavar var a end metavar imply metavar var b end metavar end define end math ] "



\item " [ math define proof of t one as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer repetition modus ponens not metavar var a end metavar conclude not metavar var a end metavar cut lemma a one conclude metavar var a end metavar imply not metavar var b end metavar imply metavar var a end metavar cut rule mp modus ponens metavar var a end metavar imply not metavar var b end metavar imply metavar var a end metavar modus ponens metavar var a end metavar conclude not metavar var b end metavar imply metavar var a end metavar cut lemma a one conclude not metavar var a end metavar imply not metavar var b end metavar imply not metavar var a end metavar cut rule mp modus ponens not metavar var a end metavar imply not metavar var b end metavar imply not metavar var a end metavar modus ponens not metavar var a end metavar conclude not metavar var b end metavar imply not metavar var a end metavar cut double negation modus ponens not metavar var b end metavar imply not metavar var a end metavar modus ponens not metavar var b end metavar imply metavar var a end metavar conclude metavar var b end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer metavar var b end metavar conclude metavar var a end metavar imply metavar var b end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar infer metavar var a end metavar imply metavar var b end metavar conclude not metavar var a end metavar imply metavar var a end metavar imply metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "
\item " [ math define statement of h zero a as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar imply metavar var b end metavar infer metavar var b end metavar imply metavar var c end metavar infer metavar var a end metavar imply metavar var c end metavar end define end math ] "

\item " [ math define proof of h zero a as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar imply metavar var b end metavar infer metavar var b end metavar imply metavar var c end metavar infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar imply metavar var b end metavar infer metavar var b end metavar imply metavar var c end metavar infer metavar var a end metavar infer rule mp modus ponens metavar var a end metavar imply metavar var b end metavar modus ponens metavar var a end metavar conclude metavar var b end metavar cut rule mp modus ponens metavar var b end metavar imply metavar var c end metavar modus ponens metavar var b end metavar conclude metavar var c end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar imply metavar var b end metavar infer metavar var b end metavar imply metavar var c end metavar infer metavar var a end metavar infer metavar var c end metavar conclude metavar var a end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var c end metavar imply metavar var a end metavar imply metavar var c end metavar cut rule mp modus ponens metavar var a end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var c end metavar imply metavar var a end metavar imply metavar var c end metavar modus ponens metavar var a end metavar imply metavar var b end metavar conclude metavar var b end metavar imply metavar var c end metavar imply metavar var a end metavar imply metavar var c end metavar cut rule mp modus ponens metavar var b end metavar imply metavar var c end metavar imply metavar var a end metavar imply metavar var c end metavar modus ponens metavar var b end metavar imply metavar var c end metavar conclude metavar var a end metavar imply metavar var c end metavar end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of h zero b as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar infer metavar var b end metavar infer metavar var a end metavar imply metavar var c end metavar end define end math ] "


\item " [ math define proof of h zero b as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar infer metavar var b end metavar infer lemma a two conclude metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar imply metavar var a end metavar imply metavar var b end metavar imply metavar var a end metavar imply metavar var c end metavar cut rule mp modus ponens metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar imply metavar var a end metavar imply metavar var b end metavar imply metavar var a end metavar imply metavar var c end metavar modus ponens metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar conclude metavar var a end metavar imply metavar var b end metavar imply metavar var a end metavar imply metavar var c end metavar cut lemma a one conclude metavar var b end metavar imply metavar var a end metavar imply metavar var b end metavar cut rule mp modus ponens metavar var b end metavar imply metavar var a end metavar imply metavar var b end metavar modus ponens metavar var b end metavar conclude metavar var a end metavar imply metavar var b end metavar cut rule mp modus ponens metavar var a end metavar imply metavar var b end metavar imply metavar var a end metavar imply metavar var c end metavar modus ponens metavar var a end metavar imply metavar var b end metavar conclude metavar var a end metavar imply metavar var c end metavar end quote state proof state cache var c end expand end define end math ] "


\item " [ math define statement of h one as system s infer all metavar var a end metavar indeed not not metavar var a end metavar imply metavar var a end metavar end define end math ] "


\item " [ math define proof of h one as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed h five conclude not metavar var a end metavar imply not not metavar var a end metavar imply not metavar var a end metavar imply not metavar var a end metavar imply metavar var a end metavar cut h six conclude not metavar var a end metavar imply not metavar var a end metavar cut h zero b modus ponens not metavar var a end metavar imply not not metavar var a end metavar imply not metavar var a end metavar imply not metavar var a end metavar imply metavar var a end metavar modus ponens not metavar var a end metavar imply not metavar var a end metavar conclude not metavar var a end metavar imply not not metavar var a end metavar imply metavar var a end metavar cut lemma a one conclude not not metavar var a end metavar imply not metavar var a end metavar imply not not metavar var a end metavar cut h zero a modus ponens not not metavar var a end metavar imply not metavar var a end metavar imply not not metavar var a end metavar modus ponens not metavar var a end metavar imply not not metavar var a end metavar imply metavar var a end metavar conclude not not metavar var a end metavar imply metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of h two as system s infer all metavar var a end metavar indeed metavar var a end metavar imply not not metavar var a end metavar end define end math ] "


\item " [ math define proof of h two as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed h five conclude not not not metavar var a end metavar imply not metavar var a end metavar imply not not not metavar var a end metavar imply metavar var a end metavar imply not not metavar var a end metavar cut h one conclude not not not metavar var a end metavar imply not metavar var a end metavar cut rule mp modus ponens not not not metavar var a end metavar imply not metavar var a end metavar imply not not not metavar var a end metavar imply metavar var a end metavar imply not not metavar var a end metavar modus ponens not not not metavar var a end metavar imply not metavar var a end metavar conclude not not not metavar var a end metavar imply metavar var a end metavar imply not not metavar var a end metavar cut lemma a one conclude metavar var a end metavar imply not not not metavar var a end metavar imply metavar var a end metavar cut h zero a modus ponens metavar var a end metavar imply not not not metavar var a end metavar imply metavar var a end metavar modus ponens not not not metavar var a end metavar imply metavar var a end metavar imply not not metavar var a end metavar conclude metavar var a end metavar imply not not metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of h four as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar imply metavar var b end metavar equal metavar var c end metavar imply metavar var a end metavar equal metavar var c end metavar end define end math ] "

\item " [ math define proof of h four as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var b end metavar equal metavar var c end metavar infer prop three two c modus ponens metavar var a end metavar equal metavar var b end metavar modus ponens metavar var b end metavar equal metavar var c end metavar conclude metavar var a end metavar equal metavar var c end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var b end metavar equal metavar var c end metavar infer metavar var a end metavar equal metavar var c end metavar conclude metavar var b end metavar equal metavar var c end metavar imply metavar var a end metavar equal metavar var c end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var b end metavar equal metavar var c end metavar imply metavar var a end metavar equal metavar var c end metavar conclude metavar var a end metavar equal metavar var b end metavar imply metavar var b end metavar equal metavar var c end metavar imply metavar var a end metavar equal metavar var c end metavar end quote state proof state cache var c end expand end define end math ] "
\item " [ math define statement of h four mark as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar equal metavar var c end metavar imply metavar var b end metavar equal metavar var c end metavar end define end math ] "

\item " [ math define proof of h four mark as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var c end metavar infer axiom s one modus ponens metavar var a end metavar equal metavar var b end metavar modus ponens metavar var a end metavar equal metavar var c end metavar conclude metavar var b end metavar equal metavar var c end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var c end metavar infer metavar var b end metavar equal metavar var c end metavar conclude metavar var a end metavar equal metavar var c end metavar imply metavar var b end metavar equal metavar var c end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var a end metavar equal metavar var c end metavar imply metavar var b end metavar equal metavar var c end metavar conclude metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar equal metavar var c end metavar imply metavar var b end metavar equal metavar var c end metavar end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of h five as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar imply not metavar var a end metavar imply not metavar var b end metavar imply metavar var a end metavar imply metavar var b end metavar end define end math ] "


\item " [ math define proof of h five as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar imply not metavar var a end metavar infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar imply metavar var a end metavar infer double negation modus ponens not metavar var b end metavar imply not metavar var a end metavar modus ponens not metavar var b end metavar imply metavar var a end metavar conclude metavar var b end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar imply metavar var a end metavar infer metavar var b end metavar conclude not metavar var b end metavar imply metavar var a end metavar imply metavar var b end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar imply not metavar var a end metavar infer not metavar var b end metavar imply metavar var a end metavar imply metavar var b end metavar conclude not metavar var b end metavar imply not metavar var a end metavar imply not metavar var b end metavar imply metavar var a end metavar imply metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "
\item " [ math define statement of h six as system s infer all metavar var a end metavar indeed metavar var a end metavar imply metavar var a end metavar end define end math ] "


\item " [ math define proof of h six as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer repetition modus ponens metavar var a end metavar conclude metavar var a end metavar cut deduction modus ponens all metavar var a end metavar indeed metavar var a end metavar infer metavar var a end metavar conclude metavar var a end metavar imply metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "
\item " [ math define statement of h ten as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar equal metavar var a end metavar infer not metavar var a end metavar equal metavar var b end metavar end define end math ] "

\item " [ math define proof of h ten as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar equal metavar var a end metavar infer h nine conclude metavar var a end metavar equal metavar var b end metavar imply metavar var b end metavar equal metavar var a end metavar cut h seven conclude metavar var a end metavar equal metavar var b end metavar imply metavar var b end metavar equal metavar var a end metavar imply not metavar var b end metavar equal metavar var a end metavar imply not metavar var a end metavar equal metavar var b end metavar cut rule mp modus ponens metavar var a end metavar equal metavar var b end metavar imply metavar var b end metavar equal metavar var a end metavar imply not metavar var b end metavar equal metavar var a end metavar imply not metavar var a end metavar equal metavar var b end metavar modus ponens metavar var a end metavar equal metavar var b end metavar imply metavar var b end metavar equal metavar var a end metavar conclude not metavar var b end metavar equal metavar var a end metavar imply not metavar var a end metavar equal metavar var b end metavar cut rule mp modus ponens not metavar var b end metavar equal metavar var a end metavar imply not metavar var a end metavar equal metavar var b end metavar modus ponens not metavar var b end metavar equal metavar var a end metavar conclude not metavar var a end metavar equal metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of modus tollens as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer not metavar var b end metavar infer not metavar var a end metavar end define end math ] "

\item " [ math define proof of modus tollens as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer not metavar var b end metavar infer h one conclude not not metavar var a end metavar imply metavar var a end metavar cut h zero a modus ponens not not metavar var a end metavar imply metavar var a end metavar modus ponens metavar var a end metavar imply metavar var b end metavar conclude not not metavar var a end metavar imply metavar var b end metavar cut all metavar var a end metavar indeed all metavar var b end metavar indeed not not metavar var a end metavar imply metavar var b end metavar infer not metavar var b end metavar infer lemma a one conclude not metavar var b end metavar imply not not metavar var a end metavar imply not metavar var b end metavar cut rule mp modus ponens not metavar var b end metavar imply not not metavar var a end metavar imply not metavar var b end metavar modus ponens not metavar var b end metavar conclude not not metavar var a end metavar imply not metavar var b end metavar cut double negation modus ponens not not metavar var a end metavar imply not metavar var b end metavar modus ponens not not metavar var a end metavar imply metavar var b end metavar conclude not metavar var a end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed not not metavar var a end metavar imply metavar var b end metavar infer not metavar var b end metavar infer not metavar var a end metavar conclude not not metavar var a end metavar imply metavar var b end metavar imply not metavar var b end metavar imply not metavar var a end metavar cut rule mp modus ponens not not metavar var a end metavar imply metavar var b end metavar imply not metavar var b end metavar imply not metavar var a end metavar modus ponens not not metavar var a end metavar imply metavar var b end metavar conclude not metavar var b end metavar imply not metavar var a end metavar cut rule mp modus ponens not metavar var b end metavar imply not metavar var a end metavar modus ponens not metavar var b end metavar conclude not metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "
\item " [ math define statement of h seven as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar imply not metavar var b end metavar imply not metavar var a end metavar end define end math ] "



\item " [ math define proof of h seven as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer h one conclude not not metavar var a end metavar imply metavar var a end metavar cut h zero a modus ponens not not metavar var a end metavar imply metavar var a end metavar modus ponens metavar var a end metavar imply metavar var b end metavar conclude not not metavar var a end metavar imply metavar var b end metavar cut h two conclude metavar var b end metavar imply not not metavar var b end metavar cut h zero a modus ponens not not metavar var a end metavar imply metavar var b end metavar modus ponens metavar var b end metavar imply not not metavar var b end metavar conclude not not metavar var a end metavar imply not not metavar var b end metavar cut h eight conclude not not metavar var a end metavar imply not not metavar var b end metavar imply not metavar var b end metavar imply not metavar var a end metavar cut rule mp modus ponens not not metavar var a end metavar imply not not metavar var b end metavar imply not metavar var b end metavar imply not metavar var a end metavar modus ponens not not metavar var a end metavar imply not not metavar var b end metavar conclude not metavar var b end metavar imply not metavar var a end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer not metavar var b end metavar imply not metavar var a end metavar conclude metavar var a end metavar imply metavar var b end metavar imply not metavar var b end metavar imply not metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "
\item " [ math define statement of h eight as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar imply not metavar var a end metavar imply metavar var a end metavar imply metavar var b end metavar end define end math ] "


\item " [ math define proof of h eight as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar imply not metavar var a end metavar infer h five conclude not metavar var b end metavar imply not metavar var a end metavar imply not metavar var b end metavar imply metavar var a end metavar imply metavar var b end metavar cut lemma a one conclude metavar var a end metavar imply not metavar var b end metavar imply metavar var a end metavar cut rule mp modus ponens not metavar var b end metavar imply not metavar var a end metavar imply not metavar var b end metavar imply metavar var a end metavar imply metavar var b end metavar modus ponens not metavar var b end metavar imply not metavar var a end metavar conclude not metavar var b end metavar imply metavar var a end metavar imply metavar var b end metavar cut h zero a modus ponens metavar var a end metavar imply not metavar var b end metavar imply metavar var a end metavar modus ponens not metavar var b end metavar imply metavar var a end metavar imply metavar var b end metavar conclude metavar var a end metavar imply metavar var b end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar imply not metavar var a end metavar infer metavar var a end metavar imply metavar var b end metavar conclude not metavar var b end metavar imply not metavar var a end metavar imply metavar var a end metavar imply metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "
\item " [ math define statement of h nine as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar equal metavar var b end metavar imply metavar var b end metavar equal metavar var a end metavar end define end math ] "

\item " [ math define proof of h nine as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar equal metavar var b end metavar infer prop three two b modus ponens metavar var a end metavar equal metavar var b end metavar conclude metavar var b end metavar equal metavar var a end metavar cut deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar equal metavar var b end metavar infer metavar var b end metavar equal metavar var a end metavar conclude metavar var a end metavar equal metavar var b end metavar imply metavar var b end metavar equal metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "
\item " [ math define statement of h twelwe as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer not metavar var a end metavar imply metavar var b end metavar infer metavar var b end metavar end define end math ] "

\item " [ math define proof of h twelwe as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer not metavar var a end metavar imply metavar var b end metavar infer h seven conclude metavar var a end metavar imply metavar var b end metavar imply not metavar var b end metavar imply not metavar var a end metavar cut rule mp modus ponens metavar var a end metavar imply metavar var b end metavar imply not metavar var b end metavar imply not metavar var a end metavar modus ponens metavar var a end metavar imply metavar var b end metavar conclude not metavar var b end metavar imply not metavar var a end metavar cut h seven conclude not metavar var a end metavar imply metavar var b end metavar imply not metavar var b end metavar imply not not metavar var a end metavar cut rule mp modus ponens not metavar var a end metavar imply metavar var b end metavar imply not metavar var b end metavar imply not not metavar var a end metavar modus ponens not metavar var a end metavar imply metavar var b end metavar conclude not metavar var b end metavar imply not not metavar var a end metavar cut double negation modus ponens not metavar var b end metavar imply not not metavar var a end metavar modus ponens not metavar var b end metavar imply not metavar var a end metavar conclude metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "

\item " [ math define statement of h eleven as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not metavar var a end metavar imply metavar var b end metavar infer metavar var a end metavar imply metavar var c end metavar infer metavar var b end metavar imply metavar var c end metavar infer metavar var c end metavar end define end math ] "


\item " [ math define proof of h eleven as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not metavar var a end metavar imply metavar var b end metavar infer metavar var a end metavar imply metavar var c end metavar infer metavar var b end metavar imply metavar var c end metavar infer h zero a modus ponens not metavar var a end metavar imply metavar var b end metavar modus ponens metavar var b end metavar imply metavar var c end metavar conclude not metavar var a end metavar imply metavar var c end metavar cut h twelwe modus ponens metavar var a end metavar imply metavar var c end metavar modus ponens not metavar var a end metavar imply metavar var c end metavar conclude metavar var c end metavar end quote state proof state cache var c end expand end define end math ] "

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

\end{document}
End of file
File page.bib

@article {grue92,
author = {K. Grue},
title = {Map Theory},
journal = TCS,
year = {1992},
volume = {102},
number = {1},
pages = {1--133},
month = {jul}}

@book {MathComp,
author = {Klaus Grue},
year = {2001},
title = {Mathematics and Computation},
publisher = {DIKU},
address = {Universitetsparken 1, DK-2100 Copenhagen},
volume = {1--3},
edition = {7},
keywords = {Logic}}


@techreport{grue02b,
author = {K. Grue},
year = {2002},
title = {Map Theory with Classical Maps},
institution
= {DIKU},
note = {\url{http://www.diku.dk/publikationer/tekniske.rapporter/2002/}},
number = {02/21}}

@inproceedings{grue04,
author = {K. Grue},
title = {Logiweb},
editor = {Fairouz Kamareddine},
booktitle = {Mathematical Knowledge Management Symposium 2003},
publisher = {Elsevier},
series = {Electronic Notes in Theoretical Computer Science},
volume = {93},
year = {2004},
pages = {70--101}}

@InProceedings{grue05,
author = {K. Grue},
year = {2005},
title = {The implementation of Logiweb},
booktitle = {Empirically Successful Classical Automated Reasoning
(ESCAR)},
editor = {Bernd Fischer and Stephan Schulz and Geoff Sutcliffe},
keywords = {Automated Reasoning, Electronic Publishing}}

@techreport{base,
author = {K. Grue},
year = {2006},
title = {A Logiweb base page},
institution={Logiweb},
note = {{\small \url{\lgwBaseUrl}}}}

@techreport{check,
author = {K. Grue},
year = {2006},
title = {A Logiweb base page},
institution={Logiweb},
note = {{\small \url{\lgwCheckUrl}}}}

@techreport{ijcar,
author = {K. Grue},
year = {2006},
title = {A Logiweb base page},
institution={Logiweb},
note = {{\small \url{\lgwIjcarUrl}}}}

@book {mendelson,
author = {E. Mendelson},
title = {Introduction to Mathematical Logic},
publisher = {Chapmann \& Hall},
year = {1997},
edition = {4.}}

End of file
latex page
bibtex page
latex page
latex page
dvipdfm page
File appendix.tex
\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 " [ math define statement of prop three seven a as system s infer all metavar var a end metavar indeed not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three seven b as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar equal metavar var c end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var c end metavar end define end math ] "

\item " [ math define statement of prop three seven c as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar equal metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three seven d as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar end define end math ] "

\item " [ math define statement of prop three seven e as system s infer all metavar var a end metavar indeed not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var a end metavar imply metavar var a end metavar equal metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three seven f as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar equal metavar var b end metavar imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar equal metavar var c end metavar imply metavar var b end metavar equal metavar var c end metavar imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var c end metavar imply metavar var a end metavar equal metavar var c end metavar end define end math ] "

\item " [ math define statement of prop three seven g as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar equal metavar var b end metavar imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar imply metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar end define end math ] "

\item " [ math define statement of prop three seven g mark as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar imply metavar var a end metavar plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar equal metavar var b end metavar end define end math ] "

\item " [ math define statement of prop three seven h as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar equal metavar var b end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar equal metavar var c end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var c end metavar end define end math ] "

\item " [ math define statement of prop three seven i as system s infer all metavar var a end metavar indeed not not for all objects var z indeed not not not var z equal zero imply not var z plus zero equal metavar var a end metavar imply zero equal metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three seven j as system s infer all metavar var a end metavar indeed not for all objects var z indeed not not not var z equal zero imply not var z plus zero equal metavar var a end metavar suc end define end math ] "

\item " [ math define statement of prop three seven k as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar suc equal metavar var b end metavar imply metavar var a end metavar suc equal metavar var b end metavar end define end math ] "

\item " [ math define statement of prop three seven k mark as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar suc equal metavar var b end metavar imply metavar var a end metavar suc equal metavar var b end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar end define end math ] "

\item " [ math define statement of prop three seven l as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar equal metavar var b end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar suc end define end math ] "

\item " [ math define statement of prop three seven l mark as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar suc imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar equal metavar var b end metavar end define end math ] "

\item " [ math define statement of prop three seven m as system s infer all metavar var a end metavar indeed not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var a end metavar suc end define end math ] "

\item " [ math define statement of prop three seven o as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar equal metavar var b end metavar imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar equal metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three seven p as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not not metavar var a end metavar equal metavar var b end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar equal metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three seven q as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar equal metavar var b end metavar imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar equal metavar var a end metavar imply metavar var b end metavar equal metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three seven r as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var a end metavar plus metavar var b end metavar imply metavar var a end metavar equal metavar var a end metavar plus metavar var b end metavar end define end math ] "

\item " [ math define statement of prop three seven s as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar equal zero imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var a end metavar plus metavar var b end metavar end define end math ] "

\item " [ math define statement of prop three seven t as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var b end metavar equal zero imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var a end metavar times metavar var b end metavar imply metavar var a end metavar equal metavar var a end metavar times metavar var b end metavar end define end math ] "

\item " [ math define statement of prop three seven u as system s infer all metavar var a end metavar indeed not metavar var a end metavar equal zero imply not for all objects var z indeed not not not var z equal zero imply not var z plus zero equal metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three seven u mark as system s infer all metavar var a end metavar indeed not for all objects var z indeed not not not var z equal zero imply not var z plus zero equal metavar var a end metavar imply not metavar var a end metavar equal zero end define end math ] "

\item " [ math define statement of prop three seven v as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not for all objects var z indeed not not not var z equal zero imply not var z plus zero equal metavar var a end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus zero equal metavar var b end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus zero equal metavar var a end metavar times metavar var b end metavar end define end math ] "

\item " [ math define statement of prop three seven w as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar equal zero imply not for all objects var z indeed not not not var z equal zero imply not var z plus zero suc equal metavar var b end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar times metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three seven x as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not metavar var a end metavar equal zero imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar equal metavar var c end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar times metavar var a end metavar equal metavar var c end metavar times metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three seven x mark as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not metavar var a end metavar equal zero imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar times metavar var a end metavar equal metavar var c end metavar times metavar var a end metavar imply not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar equal metavar var c end metavar end define end math ] "

\item " [ math define statement of prop three seven y as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not metavar var a end metavar equal zero imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar equal metavar var c end metavar imply metavar var b end metavar equal metavar var c end metavar imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar times metavar var a end metavar equal metavar var c end metavar times metavar var a end metavar imply metavar var b end metavar times metavar var a end metavar equal metavar var c end metavar times metavar var a end metavar end define end math ] "

\item " [ math define statement of prop three seven y mark as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not metavar var a end metavar equal zero imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar times metavar var a end metavar equal metavar var c end metavar times metavar var a end metavar imply metavar var b end metavar times metavar var a end metavar equal metavar var c end metavar times metavar var a end metavar imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar equal metavar var c end metavar imply metavar var b end metavar equal metavar var c end metavar end define end math ] "

\item " [ math define statement of prop three seven z as system s infer all metavar var a end metavar indeed not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal zero end define end math ] "

\item " [ math define statement of prop three seven z mark as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar equal metavar var b end metavar imply not not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var b end metavar equal metavar var a end metavar imply metavar var b end metavar equal metavar var a end metavar imply metavar var a end metavar equal metavar var b end metavar end define end math ] "
\end{list}
\subsection{proof of " [ math prop three seven end math ] "}

\section{Lemma " [ math prop three ten end math ] "}
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item " [ math define statement of prop three ten a as system s infer not for all objects var z indeed not metavar var a end metavar equal all metavar var a end metavar indeed metavar var a end metavar times var z end define end math ] "

\item " [ math define statement of prop three ten b as system s infer not for all objects var z indeed not metavar var a end metavar equal all metavar var a end metavar indeed zero suc times var z end define end math ] "

\item " [ math define statement of prop three ten c as system s infer not for all objects var z indeed not zero equal all metavar var a end metavar indeed metavar var a end metavar times var z end define end math ] "

\item " [ math define statement of prop three ten d as system s infer not for all objects var z indeed not metavar var c end metavar equal not for all objects var z indeed not metavar var c end metavar imply metavar var a end metavar equal not for all objects var z indeed not metavar var b end metavar and metavar var b end metavar equal all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar times var z times var z times var z end define end math ] "

\item " [ math define statement of prop three ten e as system s infer not for all objects var z indeed not metavar var b end metavar imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var a end metavar equal metavar var a end metavar imply metavar var a end metavar equal metavar var a end metavar equal all metavar var a end metavar indeed all metavar var b end metavar indeed not not metavar var a end metavar equal zero imply not metavar var b end metavar times var z end define end math ] "

\item " [ math define statement of prop three ten f as system s infer not for all objects var z indeed not metavar var a end metavar imply metavar var a end metavar equal metavar var b end metavar equal not for all objects var z indeed not not metavar var b end metavar imply not metavar var b end metavar equal all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar times var z times var z end define end math ] "

\item " [ math define statement of prop three ten g as system s infer not for all objects var z indeed not metavar var b end metavar times metavar var c end metavar equal not for all objects var z indeed not metavar var b end metavar imply metavar var a end metavar equal all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar times var z times var z end define end math ] "

\item " [ math define statement of prop three ten h as system s infer not for all objects var z indeed not metavar var b end metavar plus metavar var c end metavar equal not for all objects var z indeed not metavar var c end metavar imply metavar var a end metavar equal not for all objects var z indeed not metavar var b end metavar and metavar var a end metavar equal all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var a end metavar times var z times var z times var z end define end math ] "

\end{list}


\section{Lemma " [ math prop three eleven end math ] "}
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item " [ math define statement of prop three eleven as system s infer all metavar var a end metavar indeed all metavar var b end metavar indeed not metavar var a end metavar equal zero imply not for all objects metavar var c end metavar indeed for all objects metavar var d end metavar indeed not not not metavar var b end metavar equal metavar var a end metavar times metavar var c end metavar plus metavar var d end metavar imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var d end metavar equal metavar var a end metavar imply not for all objects metavar var e end metavar indeed for all objects metavar var f end metavar indeed not metavar var b end metavar equal metavar var a end metavar times metavar var e end metavar plus metavar var f end metavar imply not not for all objects var z indeed not not not var z equal zero imply not var z plus metavar var f end metavar equal metavar var a end metavar imply not metavar var c end metavar equal metavar var e end metavar imply not metavar var d end metavar equal metavar var f end metavar end define end math ] "

\end{list}





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

\end{document}
End of file
latex appendix
bibtex appendix
latex appendix
latex appendix
dvipdfm appendix
File chores.tex
\documentclass [fleqn]{article}

\everymath{\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 130 490 730}}
\hypersetup{pdftitle=Logiweb sequent calculus - Chores}
\hypersetup{colorlinks=true}

\begin {document}



\title {Logiweb sequent calculus, Chores}
\author {Klaus Grue}
\date {\today}
\maketitle
\tableofcontents

\section{Test cases}



\section{Pyk definitions}

\begin{flushleft}
" [ math define pyk of numeral zero as text "numeral zero" end text end define linebreak define pyk of numeral one as text "numeral one" end text end define linebreak define pyk of numeral two as text "numeral two" end text end define linebreak define pyk of numeral three as text "numeral three" end text end define linebreak define pyk of numeral four as text "numeral four" end text end define linebreak define pyk of numeral five as text "numeral five" end text end define linebreak define pyk of numeral six as text "numeral six" end text end define linebreak define pyk of numeral seven as text "numeral seven" end text end define linebreak define pyk of numeral eight as text "numeral eight" end text end define linebreak define pyk of numeral nine as text "numeral nine" end text end define linebreak define pyk of numeral n as text "numeral n" end text end define linebreak define pyk of rule div as text "rule div" end text end define linebreak define pyk of rule r as text "rule r" end text end define linebreak define pyk of rule r one as text "rule r one" end text end define linebreak define pyk of rule r two as text "rule r two" end text end define linebreak define pyk of rule r three as text "rule r three" end text end define linebreak define pyk of rule r four as text "rule r four" end text end define linebreak define pyk of rule r five as text "rule r five" end text end define linebreak define pyk of rule r six as text "rule r six" end text end define linebreak define pyk of conjel1 as text "conjel1" end text end define linebreak define pyk of conjel2 as text "conjel2" end text end define linebreak define pyk of conjin as text "conjin" end text end define linebreak define pyk of disjin1 as text "disjin1" end text end define linebreak define pyk of disjin2 as text "disjin2" end text end define linebreak define pyk of t one as text "t one" end text end define linebreak define pyk of h zero a as text "h zero a" end text end define linebreak define pyk of h zero b as text "h zero b" end text end define linebreak define pyk of h one as text "h one" end text end define linebreak define pyk of h two as text "h two" end text end define linebreak define pyk of h three as text "h three" end text end define linebreak define pyk of h four as text "h four" end text end define linebreak define pyk of h four mark as text "h four mark" end text end define linebreak define pyk of h five as text "h five" end text end define linebreak define pyk of h six as text "h six" end text end define linebreak define pyk of h seven as text "h seven" end text end define linebreak define pyk of h eight as text "h eight" end text end define linebreak define pyk of h nine as text "h nine" end text end define linebreak define pyk of h ten as text "h ten" end text end define linebreak define pyk of h eleven as text "h eleven" end text end define linebreak define pyk of h twelwe as text "h twelwe" end text end define linebreak define pyk of modus tollens as text "modus tollens" end text end define linebreak define pyk of axiom s ten as text "axiom s ten" end text end define linebreak define pyk of prop three two as text "prop three two" end text end define linebreak define pyk of prop three two i as text "prop three two i" end text end define linebreak define pyk of prop three two j one as text "prop three two j one" end text end define linebreak define pyk of prop three two j two as text "prop three two j two" end text end define linebreak define pyk of prop three two j as text "prop three two j" end text end define linebreak define pyk of prop three two k one as text "prop three two k one" end text end define linebreak define pyk of prop three two k two as text "prop three two k two" end text end define linebreak define pyk of prop three two k as text "prop three two k" end text end define linebreak define pyk of prop three two l one as text "prop three two l one" end text end define linebreak define pyk of prop three two l two as text "prop three two l two" end text end define linebreak define pyk of prop three two l as text "prop three two l" end text end define linebreak define pyk of prop three two m one as text "prop three two m one" end text end define linebreak define pyk of prop three two m two as text "prop three two m two" end text end define linebreak define pyk of prop three two m as text "prop three two m" end text end define linebreak define pyk of prop three two n one as text "prop three two n one" end text end define linebreak define pyk of prop three two n two as text "prop three two n two" end text end define linebreak define pyk of prop three two n as text "prop three two n" end text end define linebreak define pyk of prop three two o as text "prop three two o" end text end define linebreak define pyk of prop three four as text "prop three four" end text end define linebreak define pyk of prop three four a one as text "prop three four a one" end text end define linebreak define pyk of prop three four a two as text "prop three four a two" end text end define linebreak define pyk of prop three four a as text "prop three four a" end text end define linebreak define pyk of prop three four b as text "prop three four b" end text end define linebreak define pyk of prop three four c one as text "prop three four c one" end text end define linebreak define pyk of prop three four c two as text "prop three four c two" end text end define linebreak define pyk of prop three four c as text "prop three four c" end text end define linebreak define pyk of prop three four d one as text "prop three four d one" end text end define linebreak define pyk of prop three four d two as text "prop three four d two" end text end define linebreak define pyk of prop three four d as text "prop three four d" end text end define linebreak define pyk of prop three five as text "prop three five" end text end define linebreak define pyk of prop three five a as text "prop three five a" end text end define linebreak define pyk of prop three five b as text "prop three five b" end text end define linebreak define pyk of prop three five c as text "prop three five c" end text end define linebreak define pyk of prop three five d one as text "prop three five d one" end text end define linebreak define pyk of prop three five d two as text "prop three five d two" end text end define linebreak define pyk of prop three five d as text "prop three five d" end text end define linebreak define pyk of prop three five e one as text "prop three five e one" end text end define linebreak define pyk of prop three five e two as text "prop three five e two" end text end define linebreak define pyk of prop three five e as text "prop three five e" end text end define linebreak define pyk of prop three five f one as text "prop three five f one" end text end define linebreak define pyk of prop three five f two as text "prop three five f two" end text end define linebreak define pyk of prop three five f as text "prop three five f" end text end define linebreak define pyk of prop three five g one as text "prop three five g one" end text end define linebreak define pyk of prop three five g two as text "prop three five g two" end text end define linebreak define pyk of prop three five g three as text "prop three five g three" end text end define linebreak define pyk of prop three five g four as text "prop three five g four" end text end define linebreak define pyk of prop three five g as text "prop three five g" end text end define linebreak define pyk of prop three five h one as text "prop three five h one" end text end define linebreak define pyk of prop three five h two as text "prop three five h two" end text end define linebreak define pyk of prop three five h as text "prop three five h" end text end define linebreak define pyk of prop three five i one as text "prop three five i one" end text end define linebreak define pyk of prop three five i two as text "prop three five i two" end text end define linebreak define pyk of prop three five i as text "prop three five i" end text end define linebreak define pyk of prop three five j one as text "prop three five j one" end text end define linebreak define pyk of prop three five j two as text "prop three five j two" end text end define linebreak define pyk of prop three five j as text "prop three five j" end text end define linebreak define pyk of prop three seven as text "prop three seven" end text end define linebreak define pyk of prop three seven a as text "prop three seven a" end text end define linebreak define pyk of prop three seven b as text "prop three seven b" end text end define linebreak define pyk of prop three seven c as text "prop three seven c" end text end define linebreak define pyk of prop three seven d as text "prop three seven d" end text end define linebreak define pyk of prop three seven e as text "prop three seven e" end text end define linebreak define pyk of prop three seven f as text "prop three seven f" end text end define linebreak define pyk of prop three seven g as text "prop three seven g" end text end define linebreak define pyk of prop three seven g mark as text "prop three seven g mark" end text end define linebreak define pyk of prop three seven h as text "prop three seven h" end text end define linebreak define pyk of prop three seven i as text "prop three seven i" end text end define linebreak define pyk of prop three seven j as text "prop three seven j" end text end define linebreak define pyk of prop three seven k as text "prop three seven k" end text end define linebreak define pyk of prop three seven k mark as text "prop three seven k mark" end text end define linebreak define pyk of prop three seven l as text "prop three seven l" end text end define linebreak define pyk of prop three seven l mark as text "prop three seven l mark" end text end define linebreak define pyk of prop three seven m as text "prop three seven m" end text end define linebreak define pyk of prop three seven n as text "prop three seven n" end text end define linebreak define pyk of prop three seven o as text "prop three seven o" end text end define linebreak define pyk of prop three seven p as text "prop three seven p" end text end define linebreak define pyk of prop three seven q as text "prop three seven q" end text end define linebreak define pyk of prop three seven r as text "prop three seven r" end text end define linebreak define pyk of prop three seven s as text "prop three seven s" end text end define linebreak define pyk of prop three seven t as text "prop three seven t" end text end define linebreak define pyk of prop three seven u as text "prop three seven u" end text end define linebreak define pyk of prop three seven u mark as text "prop three seven u mark" end text end define linebreak define pyk of prop three seven v as text "prop three seven v" end text end define linebreak define pyk of prop three seven w as text "prop three seven w" end text end define linebreak define pyk of prop three seven x as text "prop three seven x" end text end define linebreak define pyk of prop three seven x mark as text "prop three seven x mark" end text end define linebreak define pyk of prop three seven y as text "prop three seven y" end text end define linebreak define pyk of prop three seven y mark as text "prop three seven y mark" end text end define linebreak define pyk of prop three seven z as text "prop three seven z" end text end define linebreak define pyk of prop three seven z mark as text "prop three seven z mark" end text end define linebreak define pyk of prop three ten as text "prop three ten" end text end define linebreak define pyk of prop three ten a as text "prop three ten a" end text end define linebreak define pyk of prop three ten b as text "prop three ten b" end text end define linebreak define pyk of prop three ten c as text "prop three ten c" end text end define linebreak define pyk of prop three ten d as text "prop three ten d" end text end define linebreak define pyk of prop three ten e as text "prop three ten e" end text end define linebreak define pyk of prop three ten f as text "prop three ten f" end text end define linebreak define pyk of prop three ten g as text "prop three ten g" end text end define linebreak define pyk of prop three ten h as text "prop three ten h" end text end define linebreak define pyk of prop three eleven as text "prop three eleven" end text end define linebreak define pyk of x ist x as text ""! ist "!" end text end define linebreak define pyk of x istq x as text ""! istq "!" end text end define linebreak define pyk of x inst x as text ""! inst "!" end text end define linebreak define pyk of x igt x as text ""! igt "!" end text end define linebreak define pyk of x igtq x as text ""! igtq "!" end text end define linebreak define pyk of x ingt x as text ""! ingt "!" end text end define linebreak define pyk of x neq x as text ""! neq "!" end text end define linebreak define pyk of x and1 x as text ""! and1 "!" end text end define linebreak define pyk of x or1 x as text ""! or1 "!" end text end define linebreak define pyk of exists x indeed x as text "exists "! indeed "!" end text end define linebreak define pyk of x divides x as text ""! divides "!" end text end define linebreak define pyk of x ldots as text ""! ldots" end text end define linebreak define pyk of opgave as text "opgave" end text end define linebreak unicode end of text end math ] "
\end{flushleft}



\section{\TeX\ definitions}

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



\item " [ math define tex of exists var x indeed var y as text "
\exists #1.
\colon #2." end text end define end math ] "

\item " [ math define tex of axiom s ten as text "
S10" end text end define end math ] "

\item " [ math define tex of var x divides var y as text "#1.
\mathrel{|} #2." end text end define end math ] "
\item " [ math define tex of prop three two as text "
Prop\ 3.2" end text end define end math ] "

\item " [ math define tex of prop three two i as text "
Prop\ 3.2i" end text end define end math ] "

\item " [ math define tex of prop three two j as text "
Prop\ 3.2j" end text end define end math ] "
\item " [ math define tex of prop three two j one as text "
Prop\ 3.2j_1" end text end define end math ] "
\item " [ math define tex of prop three two j two as text "
Prop\ 3.2j_2" end text end define end math ] "

\item " [ math define tex of prop three two k as text "
Prop\ 3.2k" end text end define end math ] "
\item " [ math define tex of prop three two k one as text "
Prop\ 3.2k_1" end text end define end math ] "
\item " [ math define tex of prop three two k two as text "
Prop\ 3.2k_2" end text end define end math ] "

\item " [ math define tex of prop three two l as text "
Prop\ 3.2l" end text end define end math ] "
\item " [ math define tex of prop three two l one as text "
Prop\ 3.2l_1" end text end define end math ] "
\item " [ math define tex of prop three two l two as text "
Prop\ 3.2l_2" end text end define end math ] "

\item " [ math define tex of prop three two m as text "
Prop\ 3.2m" end text end define end math ] "
\item " [ math define tex of prop three two m one as text "
Prop\ 3.2m_1" end text end define end math ] "
\item " [ math define tex of prop three two m two as text "
Prop\ 3.2m_2" end text end define end math ] "

\item " [ math define tex of prop three two n as text "
Prop\ 3.2n" end text end define end math ] "
\item " [ math define tex of prop three two n one as text "
Prop\ 3.2n_1" end text end define end math ] "
\item " [ math define tex of prop three two n two as text "
Prop\ 3.2n_2" end text end define end math ] "

\item " [ math define tex of prop three two o as text "
Prop\ 3.2o" end text end define end math ] "

\item " [ math define tex of prop three four as text "
Prop\ 3.4" end text end define end math ] "
\item " [ math define tex of prop three four a one as text "
Prop\ 3.4a_1" end text end define end math ] "
\item " [ math define tex of prop three four a two as text "
Prop\ 3.4a_2" end text end define end math ] "
\item " [ math define tex of prop three four a as text "
Prop\ 3.4a" end text end define end math ] "
\item " [ math define tex of prop three four b as text "
Prop\ 3.4b" end text end define end math ] "
\item " [ math define tex of prop three four c one as text "
Prop\ 3.4c_1" end text end define end math ] "
\item " [ math define tex of prop three four c two as text "
Prop\ 3.4c_2" end text end define end math ] "
\item " [ math define tex of prop three four c as text "
Prop\ 3.4c" end text end define end math ] "
\item " [ math define tex of prop three four d one as text "
Prop\ 3.4d_1" end text end define end math ] "
\item " [ math define tex of prop three four d two as text "
Prop\ 3.4d_2" end text end define end math ] "
\item " [ math define tex of prop three four d as text "
Prop\ 3.4d" end text end define end math ] "

\item " [ math define tex of prop three five as text "
Prop\ 3.5" end text end define end math ] "
\item " [ math define tex of prop three five a as text "
Prop\ 3.5a" end text end define end math ] "
\item " [ math define tex of prop three five b as text "
Prop\ 3.5b" end text end define end math ] "
\item " [ math define tex of prop three five c as text "
Prop\ 3.5c" end text end define end math ] "
\item " [ math define tex of prop three five d one as text "
Prop\ 3.5d_1" end text end define end math ] "
\item " [ math define tex of prop three five d two as text "
Prop\ 3.5d_2" end text end define end math ] "
\item " [ math define tex of prop three five d as text "
Prop\ 3.5d" end text end define end math ] "
\item " [ math define tex of prop three five e one as text "
Prop\ 3.5e_1" end text end define end math ] "
\item " [ math define tex of prop three five e two as text "
Prop\ 3.5e_2" end text end define end math ] "
\item " [ math define tex of prop three five e as text "
Prop\ 3.5e" end text end define end math ] "
\item " [ math define tex of prop three five f one as text "
Prop\ 3.5f_1" end text end define end math ] "
\item " [ math define tex of prop three five f two as text "
Prop\ 3.5f_2" end text end define end math ] "
\item " [ math define tex of prop three five f as text "
Prop\ 3.5f" end text end define end math ] "
\item " [ math define tex of prop three five g one as text "
Prop\ 3.5g_1" end text end define end math ] "
\item " [ math define tex of prop three five g two as text "
Prop\ 3.5g_4" end text end define end math ] "
\item " [ math define tex of prop three five g three as text "
Prop\ 3.5g_2" end text end define end math ] "
\item " [ math define tex of prop three five g four as text "
Prop\ 3.5g_3" end text end define end math ] "
\item " [ math define tex of prop three five g as text "
Prop\ 3.5g" end text end define end math ] "
\item " [ math define tex of prop three five h one as text "
Prop\ 3.5h_1" end text end define end math ] "
\item " [ math define tex of prop three five h two as text "
Prop\ 3.5h_2" end text end define end math ] "
\item " [ math define tex of prop three five h as text "
Prop\ 3.5h" end text end define end math ] "
\item " [ math define tex of prop three five i one as text "
Prop\ 3.5i_1" end text end define end math ] "
\item " [ math define tex of prop three five i two as text "
Prop\ 3.5i_2" end text end define end math ] "
\item " [ math define tex of prop three five i as text "
Prop\ 3.5i" end text end define end math ] "
\item " [ math define tex of prop three five j one as text "
Prop\ 3.5j_1" end text end define end math ] "
\item " [ math define tex of prop three five j two as text "
Prop\ 3.5j_2" end text end define end math ] "
\item " [ math define tex of prop three five j as text "
Prop\ 3.5j" end text end define end math ] "

\item " [ math define tex of prop three seven as text "
Prop\ 3.7" end text end define end math ] "
\item " [ math define tex of prop three seven a as text "
Prop\ 3.7a" end text end define end math ] "
\item " [ math define tex of prop three seven b as text "
Prop\ 3.7b" end text end define end math ] "
\item " [ math define tex of prop three seven c as text "
Prop\ 3.7c" end text end define end math ] "
\item " [ math define tex of prop three seven d as text "
Prop\ 3.7d" end text end define end math ] "
\item " [ math define tex of prop three seven e as text "
Prop\ 3.7e" end text end define end math ] "
\item " [ math define tex of prop three seven f as text "
Prop\ 3.7f" end text end define end math ] "
\item " [ math define tex of prop three seven g as text "
Prop\ 3.7g" end text end define end math ] "
\item " [ math define tex of prop three seven g mark as text "
Prop\ 3.7g'" end text end define end math ] "
\item " [ math define tex of prop three seven h as text "
Prop\ 3.7h" end text end define end math ] "
\item " [ math define tex of prop three seven i as text "
Prop\ 3.7i" end text end define end math ] "
\item " [ math define tex of prop three seven j as text "
Prop\ 3.7j" end text end define end math ] "
\item " [ math define tex of prop three seven k as text "
Prop\ 3.7k" end text end define end math ] "
\item " [ math define tex of prop three seven k mark as text "
Prop\ 3.7k'" end text end define end math ] "
\item " [ math define tex of prop three seven l as text "
Prop\ 3.7l" end text end define end math ] "
\item " [ math define tex of prop three seven l mark as text "
Prop\ 3.7l'" end text end define end math ] "
\item " [ math define tex of prop three seven m as text "
Prop\ 3.7m" end text end define end math ] "
\item " [ math define tex of prop three seven n as text "
Prop\ 3.7n" end text end define end math ] "
\item " [ math define tex of prop three seven o as text "
Prop\ 3.7o" end text end define end math ] "
\item " [ math define tex of prop three seven p as text "
Prop\ 3.7p" end text end define end math ] "
\item " [ math define tex of prop three seven q as text "
Prop\ 3.7q" end text end define end math ] "
\item " [ math define tex of prop three seven r as text "
Prop\ 3.7r" end text end define end math ] "
\item " [ math define tex of prop three seven s as text "
Prop\ 3.7s" end text end define end math ] "
\item " [ math define tex of prop three seven t as text "
Prop\ 3.7t" end text end define end math ] "
\item " [ math define tex of prop three seven u as text "
Prop\ 3.7u" end text end define end math ] "
\item " [ math define tex of prop three seven u mark as text "
Prop\ 3.7u'" end text end define end math ] "
\item " [ math define tex of prop three seven v as text "
Prop\ 3.7v" end text end define end math ] "
\item " [ math define tex of prop three seven w as text "
Prop\ 3.7w" end text end define end math ] "
\item " [ math define tex of prop three seven x as text "
Prop\ 3.7x" end text end define end math ] "
\item " [ math define tex of prop three seven x mark as text "
Prop\ 3.7x'" end text end define end math ] "
\item " [ math define tex of prop three seven y as text "
Prop\ 3.7y" end text end define end math ] "
\item " [ math define tex of prop three seven y mark as text "
Prop\ 3.7y'" end text end define end math ] "
\item " [ math define tex of prop three seven z as text "
Prop\ 3.7z" end text end define end math ] "
\item " [ math define tex of prop three seven z mark as text "
Prop\ 3.7z'" end text end define end math ] "

\item " [ math define tex of prop three ten as text "
Prop\ 3.10" end text end define end math ] "
\item " [ math define tex of prop three ten a as text "
Prop\ 3.10a" end text end define end math ] "
\item " [ math define tex of prop three ten b as text "
Prop\ 3.10b" end text end define end math ] "
\item " [ math define tex of prop three ten c as text "
Prop\ 3.10c" end text end define end math ] "
\item " [ math define tex of prop three ten d as text "
Prop\ 3.10d" end text end define end math ] "
\item " [ math define tex of prop three ten e as text "
Prop\ 3.10e" end text end define end math ] "
\item " [ math define tex of prop three ten f as text "
Prop\ 3.10f" end text end define end math ] "
\item " [ math define tex of prop three ten g as text "
Prop\ 3.10g" end text end define end math ] "
\item " [ math define tex of prop three ten h as text "
Prop\ 3.10h" end text end define end math ] "

\item " [ math define tex of prop three eleven as text "
Prop\ 3.11" end text end define end math ] "

\item " [ math define tex of rule r as text "
R" end text end define end math ] "
\item " [ math define tex of rule r one as text "
R1" end text end define end math ] "
\item " [ math define tex of rule r two as text "
R2" end text end define end math ] "
\item " [ math define tex of rule r three as text "
R3" end text end define end math ] "
\item " [ math define tex of rule r four as text "
R4" end text end define end math ] "
\item " [ math define tex of rule r five as text "
R5" end text end define end math ] "
\item " [ math define tex of rule r six as text "
R6" end text end define end math ] "

\item " [ math define tex of conjel1 as text "
Con1" end text end define end math ] "
\item " [ math define tex of conjel2 as text "
Con2" end text end define end math ] "
\item " [ math define tex of disjin1 as text "
Dis1" end text end define end math ] "
\item " [ math define tex of disjin2 as text "
Dis2" end text end define end math ] "
\item " [ math define tex of conjin as text "
Con" end text end define end math ] "
\item " [ math define tex of t one as text "
Lem 1.11c" end text end define end math ] "
\item " [ math define tex of h one as text "
Lem 1.11a" end text end define end math ] "
\item " [ math define tex of h two as text "
Lem 1.11b" end text end define end math ] "
\item " [ math define tex of h three as text "
H3" end text end define end math ] "
\item " [ math define tex of h four as text "
Prop 3.2c'" end text end define end math ] "
\item " [ math define tex of h four mark as text "
S1''" end text end define end math ] "
\item " [ math define tex of h five as text "
Neg'" end text end define end math ] "
\item " [ math define tex of h six as text "
Repetition'" end text end define end math ] "
\item " [ math define tex of h seven as text "
Lem 1.11e" end text end define end math ] "
\item " [ math define tex of h eight as text "
Lem 1.11d" end text end define end math ] "
\item " [ math define tex of h nine as text "
Prop 3.2b'" end text end define end math ] "
\item " [ math define tex of h ten as text "
H10" end text end define end math ] "
\item " [ math define tex of h eleven as text "
H11" end text end define end math ] "
\item " [ math define tex of h twelwe as text "
Lem 1.11g" end text end define end math ] "
\item " [ math define tex of h zero a as text "
Cor 1.10a" end text end define end math ] "
\item " [ math define tex of h zero b as text "
Cor 1.10b" end text end define end math ] "
\item " [ math define tex of modus tollens as text "
MT" end text end define end math ] "



\item " [ math define tex of var x ist var y as text "#1.
< #2." end text end define end math ] "
\item " [ math define tex of var x istq var y as text "#1.
\leq #2." end text end define end math ] "
\item " [ math define tex of var x inst var y as text "#1.
\not < #2." end text end define end math ] "
\item " [ math define tex of var x igt var y as text "#1.
> #2." end text end define end math ] "
\item " [ math define tex of var x igtq var y as text "#1.
\geq #2." end text end define end math ] "
\item " [ math define tex of var x ingt var y as text "#1.
\not > #2." end text end define end math ] "
\item " [ math define tex of var x neq var y as text "#1.
\neq #2." end text end define end math ] "
\item " [ math define tex of var x ldots as text "#1.
\ldots" end text end define end math ] "

\item " [ math define tex of var x and1 var y as text "#1.
\wedge #2." end text end define end math ] "
\item " [ math define tex of var x or1 var y as text "#1.
\vee #2." end text end define end math ] "

\end{list}


\subsection{Variables}


\section{Numerals}
" [ math define macro of var x neq var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x neq var y as not parenthesis var x equal var y end parenthesis end define end quote end define end define end math ] "

" [ math define macro of numeral zero as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define numeral zero as zero end define end quote end define end define end math ] "
" [ math define macro of numeral one as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define numeral one as zero suc end define end quote end define end define end math ] "
" [ math define macro of numeral two as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define numeral two as zero suc suc end define end quote end define end define end math ] "
" [ math define macro of numeral three as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define numeral three as zero suc suc suc end define end quote end define end define end math ] "
" [ math define macro of numeral four as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define numeral four as zero suc suc suc suc end define end quote end define end define end math ] "
" [ math define macro of numeral five as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define numeral five as zero suc suc suc suc suc end define end quote end define end define end math ] "
" [ math define macro of numeral six as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define numeral six as zero suc suc suc suc suc suc end define end quote end define end define end math ] "
" [ math define macro of numeral seven as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define numeral seven as zero suc suc suc suc suc suc suc end define end quote end define end define end math ] "
" [ math define macro of numeral eight as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define numeral eight as zero suc suc suc suc suc suc suc suc end define end quote end define end define end math ] "
" [ math define macro of numeral nine as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define numeral nine as zero suc suc suc suc suc suc suc suc suc end define end quote end define end define end math ] "


" [ math define tex of numeral zero as text "
\overline{0}" end text end define end math ] "
" [ math define tex of numeral one as text "
\overline{1}" end text end define end math ] "
" [ math define tex of numeral two as text "
\overline{2}" end text end define end math ] "
" [ math define tex of numeral three as text "
\overline{3}" end text end define end math ] "
" [ math define tex of numeral four as text "
\overline{4}" end text end define end math ] "
" [ math define tex of numeral five as text "
\overline{5}" end text end define end math ] "
" [ math define tex of numeral six as text "
\overline{6}" end text end define end math ] "
" [ math define tex of numeral seven as text "
\overline{7}" end text end define end math ] "
" [ math define tex of numeral eight as text "
\overline{8}" end text end define end math ] "
" [ math define tex of numeral nine as text "
\overline{9}" end text end define end math ] "
" [ math define tex of numeral n as text "
\overline{n}" end text end define end math ] "



\section{Priority table}

" [ flush left math define priority of opgave as preassociative priority opgave equal priority base equal priority bracket x end bracket equal priority big bracket x end bracket equal priority math x end math equal priority flush left x end left equal priority var x equal priority var y equal priority var z equal priority proclaim x as x end proclaim equal priority define x of x as x end define equal priority pyk equal priority tex equal priority tex name equal priority priority equal priority x equal priority true equal priority if x then x else x end if equal priority introduce x of x as x end introduce equal priority value equal priority claim equal priority bottom equal priority function f of x end function equal priority identity x end identity equal priority false equal priority untagged zero equal priority untagged one equal priority untagged two equal priority untagged three equal priority untagged four equal priority untagged five equal priority untagged six equal priority untagged seven equal priority untagged eight equal priority untagged nine equal priority zero equal priority one equal priority two equal priority three equal priority four equal priority five equal priority six equal priority seven equal priority eight equal priority nine equal priority var a equal priority var b equal priority var c equal priority var d equal priority var e equal priority var f equal priority var g equal priority var h equal priority var i equal priority var j equal priority var k equal priority var l equal priority var m equal priority var n equal priority var o equal priority var p equal priority var q equal priority var r equal priority var s equal priority var t equal priority var u equal priority var v equal priority var w equal priority tagged parenthesis x end tagged equal priority tagged if x then x else x end if equal priority array x is x end array equal priority left equal priority center equal priority right equal priority empty equal priority substitute x set x to x end substitute equal priority map tag x end tag equal priority raw map untag x end untag equal priority map untag x end untag equal priority normalizing untag x end untag equal priority apply x to x end apply equal priority apply one x to x end apply equal priority identifier x end identifier equal priority identifier one x plus id x end identifier equal priority array plus x and x end plus equal priority array remove x array x level x end remove equal priority array put x value x array x level x end put equal priority array add x value x index x value x level x end add equal priority bit x of x end bit equal priority bit one x of x end bit equal priority example rack equal priority vector hook equal priority bibliography hook equal priority dictionary hook equal priority body hook equal priority codex hook equal priority expansion hook equal priority code hook equal priority cache hook equal priority diagnose hook equal priority pyk aspect equal priority tex aspect equal priority texname aspect equal priority value aspect equal priority message aspect equal priority macro aspect equal priority definition aspect equal priority unpack aspect equal priority claim aspect equal priority priority aspect equal priority lambda identifier equal priority apply identifier equal priority true identifier equal priority if identifier equal priority quote identifier equal priority proclaim identifier equal priority define identifier equal priority introduce identifier equal priority hide identifier equal priority pre identifier equal priority post identifier equal priority eval x stack x cache x end eval equal priority eval two x ref x id x stack x cache x end eval equal priority eval three x function x stack x cache x end eval equal priority eval four x arguments x stack x cache x end eval equal priority lookup x stack x default x end lookup equal priority abstract x term x stack x cache x end abstract equal priority quote x end quote equal priority expand x state x cache x end expand equal priority expand two x definition x state x cache x end expand equal priority expand list x state x cache x end expand equal priority macro equal priority macro state equal priority zip x with x end zip equal priority assoc one x address x index x end assoc equal priority protect x end protect equal priority self equal priority macro define x as x end define equal priority value define x as x end define equal priority intro define x as x end define equal priority pyk define x as x end define equal priority tex define x as x end define equal priority tex name define x as x end define equal priority priority table x end table equal priority macro define one equal priority macro define two x end define equal priority macro define three x end define equal priority macro define four x state x cache x definition x end define equal priority state expand x state x cache x end expand equal priority quote expand x term x stack x end expand equal priority quote expand two x term x stack x end expand equal priority quote expand three x term x stack x value x end expand equal priority quote expand star x term x stack x end expand equal priority parenthesis x end parenthesis equal priority big parenthesis x end parenthesis equal priority display x end display equal priority statement x end statement equal priority spying test x end test equal priority false spying test x end test equal priority aspect x subcodex x end aspect equal priority aspect x term x cache x end aspect equal priority tuple x end tuple equal priority tuple one x end tuple equal priority tuple two x end tuple equal priority let two x apply x end let equal priority let one x apply x end let equal priority claim define x as x end define equal priority checker equal priority check x cache x end check equal priority check two x cache x def x end check equal priority check three x cache x def x end check equal priority check list x cache x end check equal priority check list two x cache x value x end check equal priority test x end test equal priority false test x end test equal priority raw test x end test equal priority message equal priority message define x as x end define equal priority the statement aspect equal priority statement equal priority statement define x as x end define equal priority example axiom equal priority example scheme equal priority example rule equal priority absurdity equal priority contraexample equal priority example theory primed equal priority example lemma equal priority metavar x end metavar equal priority meta a equal priority meta b equal priority meta c equal priority meta d equal priority meta e equal priority meta f equal priority meta g equal priority meta h equal priority meta i equal priority meta j equal priority meta k equal priority meta l equal priority meta m equal priority meta n equal priority meta o equal priority meta p equal priority meta q equal priority meta r equal priority meta s equal priority meta t equal priority meta u equal priority meta v equal priority meta w equal priority meta x equal priority meta y equal priority meta z equal priority sub x set x to x end sub equal priority sub star x set x to x end sub equal priority the empty set equal priority example remainder equal priority make visible x end visible equal priority intro x index x pyk x tex x end intro equal priority intro x pyk x tex x end intro equal priority error x term x end error equal priority error two x term x end error equal priority proof x term x cache x end proof equal priority proof two x term x end proof equal priority sequent eval x term x end eval equal priority seqeval init x term x end eval equal priority seqeval modus x term x end eval equal priority seqeval modus one x term x sequent x end eval equal priority seqeval verify x term x end eval equal priority seqeval verify one x term x sequent x end eval equal priority sequent eval plus x term x end eval equal priority seqeval plus one x term x sequent x end eval equal priority seqeval minus x term x end eval equal priority seqeval minus one x term x sequent x end eval equal priority seqeval deref x term x end eval equal priority seqeval deref one x term x sequent x end eval equal priority seqeval deref two x term x sequent x def x end eval equal priority seqeval at x term x end eval equal priority seqeval at one x term x sequent x end eval equal priority seqeval infer x term x end eval equal priority seqeval infer one x term x premise x sequent x end eval equal priority seqeval endorse x term x end eval equal priority seqeval endorse one x term x side x sequent x end eval equal priority seqeval est x term x end eval equal priority seqeval est one x term x name x sequent x end eval equal priority seqeval est two x term x name x sequent x def x end eval equal priority seqeval all x term x end eval equal priority seqeval all one x term x variable x sequent x end eval equal priority seqeval cut x term x end eval equal priority seqeval cut one x term x forerunner x end eval equal priority seqeval cut two x term x forerunner x sequent x end eval equal priority computably true x end true equal priority claims x cache x ref x end claims equal priority claims two x cache x ref x end claims equal priority the proof aspect equal priority proof equal priority lemma x says x end lemma equal priority proof of x reads x end proof equal priority in theory x lemma x says x end lemma equal priority in theory x antilemma x says x end antilemma equal priority in theory x rule x says x end rule equal priority in theory x antirule x says x end antirule equal priority verifier equal priority verify one x end verify equal priority verify two x proofs x end verify equal priority verify three x ref x sequents x diagnose x end verify equal priority verify four x premises x end verify equal priority verify five x ref x array x sequents x end verify equal priority verify six x ref x list x sequents x end verify equal priority verify seven x ref x id x sequents x end verify equal priority cut x and x end cut equal priority head x end head equal priority tail x end tail equal priority rule one x theory x end rule equal priority rule x subcodex x end rule equal priority rule tactic equal priority plus x and x end plus equal priority theory x end theory equal priority theory two x cache x end theory equal priority theory three x name x end theory equal priority theory four x name x sum x end theory equal priority example axiom lemma primed equal priority example scheme lemma primed equal priority example rule lemma primed equal priority contraexample lemma primed equal priority example axiom lemma equal priority example scheme lemma equal priority example rule lemma equal priority contraexample lemma equal priority example theory equal priority ragged right equal priority ragged right expansion equal priority parameter term x stack x seed x end parameter equal priority parameter term star x stack x seed x end parameter equal priority instantiate x with x end instantiate equal priority instantiate star x with x end instantiate equal priority occur x in x substitution x end occur equal priority occur star x in x substitution x end occur equal priority unify x with x substitution x end unify equal priority unify star x with x substitution x end unify equal priority unify two x with x substitution x end unify equal priority ell a equal priority ell b equal priority ell c equal priority ell d equal priority ell e equal priority ell f equal priority ell g equal priority ell h equal priority ell i equal priority ell j equal priority ell k equal priority ell l equal priority ell m equal priority ell n equal priority ell o equal priority ell p equal priority ell q equal priority ell r equal priority ell s equal priority ell t equal priority ell u equal priority ell v equal priority ell w equal priority ell x equal priority ell y equal priority ell z equal priority ell big a equal priority ell big b equal priority ell big c equal priority ell big d equal priority ell big e equal priority ell big f equal priority ell big g equal priority ell big h equal priority ell big i equal priority ell big j equal priority ell big k equal priority ell big l equal priority ell big m equal priority ell big n equal priority ell big o equal priority ell big p equal priority ell big q equal priority ell big r equal priority ell big s equal priority ell big t equal priority ell big u equal priority ell big v equal priority ell big w equal priority ell big x equal priority ell big y equal priority ell big z equal priority ell dummy equal priority sequent reflexivity equal priority tactic reflexivity equal priority sequent commutativity equal priority tactic commutativity equal priority the tactic aspect equal priority tactic equal priority tactic define x as x end define equal priority proof expand x state x cache x end expand equal priority proof expand list x state x cache x end expand equal priority proof state equal priority conclude one x cache x end conclude equal priority conclude two x proves x cache x end conclude equal priority conclude three x proves x lemma x substitution x end conclude equal priority conclude four x lemma x end conclude equal priority check equal priority general macro define x as x end define equal priority make root visible x end visible equal priority sequent example axiom equal priority sequent example rule equal priority sequent example contradiction equal priority sequent example theory equal priority sequent example lemma equal priority set x end set equal priority object var x end var equal priority object a equal priority object b equal priority object c equal priority object d equal priority object e equal priority object f equal priority object g equal priority object h equal priority object i equal priority object j equal priority object k equal priority object l equal priority object m equal priority object n equal priority object o equal priority object p equal priority object q equal priority object r equal priority object s equal priority object t equal priority object u equal priority object v equal priority object w equal priority object x equal priority object y equal priority object z equal priority sub x is x where x is x end sub equal priority sub zero x is x where x is x end sub equal priority sub one x is x where x is x end sub equal priority sub star x is x where x is x end sub equal priority deduction x conclude x end deduction equal priority deduction zero x conclude x end deduction equal priority deduction one x conclude x condition x end deduction equal priority deduction two x conclude x condition x end deduction equal priority deduction three x conclude x condition x bound x end deduction equal priority deduction four x conclude x condition x bound x end deduction equal priority deduction four star x conclude x condition x bound x end deduction equal priority deduction five x condition x bound x end deduction equal priority deduction six x conclude x exception x bound x end deduction equal priority deduction six star x conclude x exception x bound x end deduction equal priority deduction seven x end deduction equal priority deduction eight x bound x end deduction equal priority deduction eight star x bound x end deduction equal priority system s equal priority double negation equal priority rule mp equal priority rule gen equal priority deduction equal priority axiom s one equal priority axiom s two equal priority axiom s three equal priority axiom s four equal priority axiom s five equal priority axiom s six equal priority axiom s seven equal priority axiom s eight equal priority axiom s nine equal priority repetition equal priority lemma a one equal priority lemma a two equal priority lemma a four equal priority lemma a five equal priority prop three two a equal priority prop three two b equal priority prop three two c equal priority prop three two d equal priority prop three two e one equal priority prop three two e two equal priority prop three two e equal priority prop three two f one equal priority prop three two f two equal priority prop three two f equal priority prop three two g one equal priority prop three two g two equal priority prop three two g equal priority prop three two h one equal priority prop three two h two equal priority prop three two h equal priority block one x state x cache x end block equal priority block two x end block equal priority numeral zero equal priority numeral one equal priority numeral two equal priority numeral three equal priority numeral four equal priority numeral five equal priority numeral six equal priority numeral seven equal priority numeral eight equal priority numeral nine equal priority numeral n equal priority rule div equal priority rule r equal priority rule r one equal priority rule r two equal priority rule r three equal priority rule r four equal priority rule r five equal priority rule r six equal priority conjel1 equal priority conjel2 equal priority conjin equal priority disjin1 equal priority disjin2 equal priority t one equal priority h zero a equal priority h zero b equal priority h one equal priority h two equal priority h three equal priority h four equal priority h four mark equal priority h five equal priority h six equal priority h seven equal priority h eight equal priority h nine equal priority h ten equal priority h eleven equal priority h twelwe equal priority modus tollens equal priority axiom s ten equal priority prop three two equal priority prop three two i equal priority prop three two j one equal priority prop three two j two equal priority prop three two j equal priority prop three two k one equal priority prop three two k two equal priority prop three two k equal priority prop three two l one equal priority prop three two l two equal priority prop three two l equal priority prop three two m one equal priority prop three two m two equal priority prop three two m equal priority prop three two n one equal priority prop three two n two equal priority prop three two n equal priority prop three two o equal priority prop three four equal priority prop three four a one equal priority prop three four a two equal priority prop three four a equal priority prop three four b equal priority prop three four c one equal priority prop three four c two equal priority prop three four c equal priority prop three four d one equal priority prop three four d two equal priority prop three four d equal priority prop three five equal priority prop three five a equal priority prop three five b equal priority prop three five c equal priority prop three five d one equal priority prop three five d two equal priority prop three five d equal priority prop three five e one equal priority prop three five e two equal priority prop three five e equal priority prop three five f one equal priority prop three five f two equal priority prop three five f equal priority prop three five g one equal priority prop three five g two equal priority prop three five g three equal priority prop three five g four equal priority prop three five g equal priority prop three five h one equal priority prop three five h two equal priority prop three five h equal priority prop three five i one equal priority prop three five i two equal priority prop three five i equal priority prop three five j one equal priority prop three five j two equal priority prop three five j equal priority prop three seven equal priority prop three seven a equal priority prop three seven b equal priority prop three seven c equal priority prop three seven d equal priority prop three seven e equal priority prop three seven f equal priority prop three seven g equal priority prop three seven g mark equal priority prop three seven h equal priority prop three seven i equal priority prop three seven j equal priority prop three seven k equal priority prop three seven k mark equal priority prop three seven l equal priority prop three seven l mark equal priority prop three seven m equal priority prop three seven n equal priority prop three seven o equal priority prop three seven p equal priority prop three seven q equal priority prop three seven r equal priority prop three seven s equal priority prop three seven t equal priority prop three seven u equal priority prop three seven u mark equal priority prop three seven v equal priority prop three seven w equal priority prop three seven x equal priority prop three seven x mark equal priority prop three seven y equal priority prop three seven y mark equal priority prop three seven z equal priority prop three seven z mark equal priority prop three ten equal priority prop three ten a equal priority prop three ten b equal priority prop three ten c equal priority prop three ten d equal priority prop three ten e equal priority prop three ten f equal priority prop three ten g equal priority prop three ten h equal priority prop three eleven end priority greater than preassociative priority x sub x end sub equal priority x intro x index x pyk x tex x end intro equal priority x intro x pyk x tex x end intro equal priority x intro x index x pyk x tex x name x end intro equal priority x intro x pyk x tex x name x end intro equal priority x prime equal priority x assoc x end assoc equal priority x set x to x end set equal priority x set multi x to x end set equal priority x bit nil equal priority x bit one equal priority binary equal priority x color x end color equal priority x color star x end color equal priority x raw head equal priority x raw tail equal priority x cardinal untag equal priority x head equal priority x tail equal priority x is singular equal priority x is cardinal equal priority x is data equal priority x is atomic equal priority x cardinal retract equal priority x tagged retract equal priority x boolean retract equal priority x ref equal priority x id equal priority x debug equal priority x root equal priority x zeroth equal priority x first equal priority x second equal priority x third equal priority x fourth equal priority x fifth equal priority x sixth equal priority x seventh equal priority x eighth equal priority x ninth equal priority x is error equal priority x is metavar equal priority x is metaclosed equal priority x is metaclosed star equal priority x hide end priority greater than preassociative priority unicode start of text x end unicode text equal priority unicode end of text equal priority text x end text equal priority text x plus x equal priority text x plus indent x equal priority unicode newline x equal priority unicode space x equal priority unicode exclamation mark x equal priority unicode quotation mark x equal priority unicode number sign x equal priority unicode dollar sign x equal priority unicode percent x equal priority unicode ampersand x equal priority unicode apostrophe x equal priority unicode left parenthesis x equal priority unicode right parenthesis x equal priority unicode asterisk x equal priority unicode plus sign x equal priority unicode comma x equal priority unicode hyphen x equal priority unicode period x equal priority unicode slash x equal priority unicode zero x equal priority unicode one x equal priority unicode two x equal priority unicode three x equal priority unicode four x equal priority unicode five x equal priority unicode six x equal priority unicode seven x equal priority unicode eight x equal priority unicode nine x equal priority unicode colon x equal priority unicode semicolon x equal priority unicode less than x equal priority unicode equal sign x equal priority unicode greater than x equal priority unicode question mark x equal priority unicode commercial at x equal priority unicode capital a x equal priority unicode capital b x equal priority unicode capital c x equal priority unicode capital d x equal priority unicode capital e x equal priority unicode capital f x equal priority unicode capital g x equal priority unicode capital h x equal priority unicode capital i x equal priority unicode capital j x equal priority unicode capital k x equal priority unicode capital l x equal priority unicode capital m x equal priority unicode capital n x equal priority unicode capital o x equal priority unicode capital p x equal priority unicode capital q x equal priority unicode capital r x equal priority unicode capital s x equal priority unicode capital t x equal priority unicode capital u x equal priority unicode capital v x equal priority unicode capital w x equal priority unicode capital x x equal priority unicode capital y x equal priority unicode capital z x equal priority unicode left bracket x equal priority unicode backslash x equal priority unicode right bracket x equal priority unicode circumflex x equal priority unicode underscore x equal priority unicode grave accent x equal priority unicode small a x equal priority unicode small b x equal priority unicode small c x equal priority unicode small d x equal priority unicode small e x equal priority unicode small f x equal priority unicode small g x equal priority unicode small h x equal priority unicode small i x equal priority unicode small j x equal priority unicode small k x equal priority unicode small l x equal priority unicode small m x equal priority unicode small n x equal priority unicode small o x equal priority unicode small p x equal priority unicode small q x equal priority unicode small r x equal priority unicode small s x equal priority unicode small t x equal priority unicode small u x equal priority unicode small v x equal priority unicode small w x equal priority unicode small x x equal priority unicode small y x equal priority unicode small z x equal priority unicode left brace x equal priority unicode vertical line x equal priority unicode right brace x equal priority unicode tilde x equal priority preassociative x greater than x equal priority postassociative x greater than x equal priority priority x equal x equal priority priority x end priority equal priority newline x equal priority macro newline x equal priority macro indent x end priority greater than preassociative priority x apply x equal priority x tagged apply x end priority greater than preassociative priority x suc end priority greater than preassociative priority x times x equal priority x times zero x end priority greater than preassociative priority x plus x equal priority x plus zero x equal priority x plus one x equal priority x minus x equal priority x minus zero x equal priority x minus one x end priority greater than preassociative priority x term plus x end plus equal priority x term union x equal priority x term minus x end minus end priority greater than postassociative priority x raw pair x equal priority x eager pair x equal priority x tagged pair x equal priority x untagged double x equal priority x pair x equal priority x double x end priority greater than postassociative priority x comma x end priority greater than preassociative priority x boolean equal x equal priority x data equal x equal priority x cardinal equal x equal priority x peano equal x equal priority x tagged equal x equal priority x math equal x equal priority x reduce to x equal priority x term equal x equal priority x term list equal x equal priority x term root equal x equal priority x term in x equal priority x term subset x equal priority x term set equal x equal priority x sequent equal x equal priority x free in x equal priority x free in star x equal priority x free for x in x equal priority x free for star x in x equal priority x claim in x equal priority x less x equal priority x less zero x equal priority x less one x equal priority x equal x equal priority x unequal x equal priority x is object var equal priority x avoid zero x equal priority x avoid one x equal priority x avoid star x equal priority x ist x equal priority x istq x equal priority x inst x equal priority x igt x equal priority x igtq x equal priority x ingt x equal priority x neq x end priority greater than preassociative priority not x end priority greater than preassociative priority x and x equal priority x macro and x equal priority x simple and x equal priority x claim and x equal priority x and1 x end priority greater than preassociative priority x or x equal priority x parallel x equal priority x macro or x equal priority x or1 x end priority greater than preassociative priority exist x indeed x equal priority for all x indeed x equal priority for all objects x indeed x equal priority exists x indeed x end priority greater than postassociative priority x macro imply x equal priority x imply x equal priority x if and only if x end priority greater than postassociative priority x guard x equal priority x spy x equal priority x tagged guard x end priority greater than preassociative priority x select x else x end select end priority greater than preassociative priority lambda x dot x equal priority tagged lambda x dot x equal priority tagging x equal priority open if x then x else x equal priority let x be x in x equal priority let x abbreviate x in x end priority greater than preassociative priority x avoid x end priority greater than preassociative priority x init equal priority x modus equal priority x verify equal priority x curry plus equal priority x curry minus equal priority x dereference end priority greater than preassociative priority x at x equal priority x modus ponens x equal priority x modus probans x equal priority x conclude x equal priority x object modus ponens x end priority greater than postassociative priority x infer x equal priority x endorse x equal priority x id est x end priority greater than preassociative priority all x indeed x equal priority for all terms x indeed x end priority greater than postassociative priority x rule plus x end priority greater than postassociative priority x cut x end priority greater than preassociative priority x proves x end priority greater than preassociative priority x proof of x reads x equal priority line x because x indeed x end line x equal priority because x indeed x qed equal priority line x premise x end line x equal priority line x side condition x end line x equal priority arbitrary x end line x equal priority locally define x as x end line x equal priority block x line x end block x equal priority because x indeed x end line equal priority any term x end line x end priority greater than postassociative priority x alternative x end priority greater than postassociative priority x , x equal priority x [ x ] x end priority greater than preassociative priority x tab x equal priority evaluates to end priority greater than preassociative priority x row x equal priority x linebreak x equal priority x safe row x equal priority x divides x equal priority x ldots end priority greater than unicode end of text end define end math end left ] "

\end{document}
End of file
latex chores
latex chores
dvipdfm chores"