Logiweb body of pogave 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{url}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle=Logiweb sequent calculus}
\hypersetup{colorlinks=true}

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

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

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

" [ ragged right expansion ] "



\begin{abstract}

\end{abstract}




\section{Introduction}\label{sec:Introduction}
In this paper we will prove the propositions regarding " [ math system s end math ] " starting with proposition " [ math prop three two i end math ] ". continuing to 3.4, bevise 3.5,
%tilf\o je aksiomet %$ x < y <=> E z : z 0 \& z + x = y$, bevise 3.7, tilf\o je
aksiomer, der definerer x|y, bevise 3.10, og bevise 3.11.


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


\section{}


A modified version of Mendelsons system " [ math system s end math ] " (Peano arithmetic) \cite{mendelson} may be formulated thus:

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

\item \makebox[0.45\textwidth][l]{" [ math theory system s end theory end math ] "}" [ math in theory system s rule rule mp says for all terms meta a comma meta b indeed meta a imply meta b infer meta a infer meta b end rule end math ] "

\item \makebox[0.45\textwidth][l]{" [ math in theory system s rule rule gen says for all terms meta x comma meta a indeed meta a infer for all meta x indeed meta a end rule end math ] "}" [ math in theory system s rule deduction says for all terms meta a comma meta b indeed deduction meta a conclude meta b end deduction endorse meta a infer meta b end rule end math ] "

\item \makebox[0.45\textwidth][l]{}" [ math in theory system s rule axiom s two says for all terms meta a comma meta b indeed meta a equal meta b infer meta a suc equal meta b suc end rule end math ] "

\item \makebox[0.45\textwidth][l]{" [ math in theory system s rule axiom s three says for all terms meta a indeed not zero equal meta a suc end rule end math ] "}" [ math in theory system s rule axiom s four says for all terms meta a comma meta b indeed meta a suc equal meta b suc infer meta a equal meta b end rule end math ] "

\item \makebox[0.45\textwidth][l]{" [ math in theory system s rule axiom s five says for all terms meta a indeed meta a plus zero equal meta a end rule end math ] "}" [ math in theory system s rule axiom s six says for all terms meta a comma meta b indeed meta a plus meta b suc equal parenthesis meta a plus meta b end parenthesis suc end rule end math ] "

\item \makebox[0.45\textwidth][l]{" [ math in theory system s rule axiom s seven says for all terms meta a indeed meta a times zero equal zero end rule end math ] "}" [ math in theory system s rule axiom s eight says for all terms meta a comma meta b indeed meta a times parenthesis meta b suc end parenthesis equal parenthesis meta a times meta b end parenthesis plus meta a end rule end math ] "

\item " [ math in theory system s rule double negation says for all terms meta a indeed for all terms meta b indeed not meta b imply not meta a infer not meta b imply meta a infer meta b end rule end math ] "

\item " [ math in theory system s rule axiom s one says for all terms meta a comma meta b comma meta c indeed meta a equal meta b infer meta a equal meta c infer meta b equal meta c end rule end math ] "

\item " [ math in theory system s rule axiom s nine says for all terms meta x comma meta a comma meta b comma meta c indeed sub meta b is meta a where meta x is zero end sub endorse sub meta c is meta a where meta x is meta x suc end sub endorse meta b infer meta a imply meta c infer meta a end rule end math ] "


\end{list}


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

\item " [ math in theory system s lemma prop three two a says for all terms meta a indeed meta a equal meta a end lemma end math ] "

\item " [ math in theory system s lemma prop three two b says for all terms meta a comma meta b indeed meta a equal meta b infer meta b equal meta a end lemma end math ] "

\item " [ math in theory system s lemma prop three two c says for all terms meta a comma meta b comma meta c indeed meta a equal meta b infer meta b equal meta c infer meta a equal meta c end lemma end math ] "

\item " [ math in theory system s lemma prop three two d says for all terms meta a comma meta b comma meta c indeed meta a equal meta c infer meta b equal meta c infer meta a equal meta b end lemma end math ] "

\item " [ math in theory system s lemma prop three two e says for all terms meta a comma meta b comma meta c indeed meta a equal meta b infer meta a plus meta c equal meta b plus meta c end lemma end math ] "

\item " [ math in theory system s lemma prop three two f says for all terms meta a indeed meta a equal zero plus meta a end lemma end math ] "

\item " [ math in theory system s lemma prop three two g says for all terms meta a comma meta b indeed meta a suc plus meta b equal parenthesis meta a plus meta b end parenthesis suc end lemma end math ] "

\item " [ math in theory system s lemma prop three two h says for all terms meta a comma meta b indeed meta a plus meta b equal meta b plus meta a end lemma end math ] "

\item " [ math in theory system s lemma prop three two i says for all terms meta a comma meta b comma meta c indeed meta a equal meta b infer meta c plus meta a equal meta c plus meta b end lemma end math ] "

\item " [ math in theory system s lemma prop three two j says for all terms meta a comma meta b comma meta c indeed parenthesis meta a plus meta b end parenthesis plus meta c equal meta a plus parenthesis meta b plus meta c end parenthesis end lemma end math ] "

\item " [ math in theory system s lemma prop three two k says for all terms meta a comma meta b comma meta c indeed meta a equal meta b infer meta a times meta c equal meta b times meta c end lemma end math ] "

\item " [ math in theory system s lemma prop three two l says for all terms meta a indeed zero times meta a equal zero end lemma end math ] "

\item " [ math in theory system s lemma prop three two m says for all terms meta a comma meta b indeed meta a suc times meta b equal meta a times meta b plus meta b end lemma end math ] "

\item " [ math in theory system s lemma prop three two n says for all terms meta a comma meta b indeed meta a times meta b equal meta b times meta a end lemma end math ] "

\item " [ math in theory system s lemma prop three two o says for all terms meta a comma meta b comma meta c indeed meta a equal meta b infer meta c times meta a equal meta c times meta b end lemma end math ] "

\end{list}

we will start by doing " [ math prop three two i end math ] "
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item " [ math in theory system s lemma prop three two i says for all terms meta a comma meta b comma meta c indeed meta a equal meta b infer meta c plus meta a equal meta c plus meta b end lemma end math ] "

\item " [ math system s proof of prop three two i reads any term meta a comma meta b comma meta c end line block any term macro indent meta a comma meta b comma meta c end line line ell a because prop three two e indeed meta a equal meta b imply meta a plus meta c equal meta b plus meta c end line line ell b because prop three two h indeed meta a plus meta c equal meta c plus meta a end line line ell c because prop three two h indeed meta b plus meta c equal meta c plus meta b end line line ell d premise meta a equal meta b end line line ell k because rule mp modus ponens ell a modus ponens ell d indeed meta a plus meta c equal meta b plus meta c end line line ell h because axiom s one indeed meta a plus meta c equal meta b plus meta c imply parenthesis meta a plus meta c equal meta c plus meta a imply meta b plus meta c equal meta c plus meta a end parenthesis end line line ell i because rule mp modus ponens ell h modus ponens ell k indeed meta a plus meta c equal meta c plus meta a imply meta b plus meta c equal meta c plus meta a end line line ell k because rule mp modus ponens ell i modus ponens ell b indeed meta b plus meta c equal meta c plus meta a end line line ell j because prop three two b modus ponens ell k indeed meta c plus meta a equal meta b plus meta c end line line ell e because prop three two e indeed meta c plus meta a equal meta b plus meta c imply parenthesis meta b plus meta c equal meta c plus meta b imply meta c plus meta a equal meta c plus meta b end parenthesis end line line ell f because rule mp modus ponens ell e modus ponens ell j indeed meta b plus meta c equal meta c plus meta b imply meta c plus meta a equal meta c plus meta b end line because rule mp modus ponens ell f modus ponens ell c indeed meta c plus meta a equal meta c plus meta b end line line ell g end block because deduction modus ponens ell g indeed meta a equal meta b imply meta c plus meta a equal meta c plus meta b qed end math ] "

\end{list}

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

\item " [ math in theory system s lemma prop three two j one says for all terms meta a comma meta b indeed parenthesis meta a plus meta b end parenthesis plus zero equal meta a plus parenthesis meta b plus zero end parenthesis end lemma end math ] "

\item " [ math system s proof of prop three two j one reads any term meta a comma meta b end line line ell a because axiom s five indeed parenthesis meta a plus meta b end parenthesis plus zero equal meta a plus meta b end line line ell b because axiom s five indeed meta b plus zero equal meta b end line line ell c because prop three two i modus ponens ell b indeed meta a plus parenthesis meta b plus zero end parenthesis equal meta a plus meta b end line because prop three two d modus ponens ell a modus ponens ell c indeed parenthesis meta a plus meta b end parenthesis plus zero equal meta a plus parenthesis meta b plus zero end parenthesis qed end math ] "

\item " [ math in theory system s lemma prop three two j two says for all terms meta a comma meta b comma meta c indeed parenthesis meta a plus meta b end parenthesis plus meta c equal meta a plus parenthesis meta b plus meta c end parenthesis imply parenthesis meta a plus meta b end parenthesis plus meta c suc equal meta a plus parenthesis meta b plus meta c suc end parenthesis end lemma end math ] "

\item " [ math system s proof of prop three two j two reads any term meta a comma meta b comma meta c end line block any term macro indent meta a comma meta b comma meta c end line line ell a premise macro indent parenthesis meta a plus meta b end parenthesis plus meta c equal meta a plus parenthesis meta b plus meta c end parenthesis end line line ell b because axiom s six indeed macro indent parenthesis meta a plus meta b end parenthesis plus meta c suc equal meta a plus parenthesis meta b plus meta c end parenthesis suc end line line ell c because axiom s two modus ponens ell a indeed macro indent parenthesis parenthesis meta a plus meta b end parenthesis plus meta c end parenthesis suc equal parenthesis meta a plus parenthesis meta b plus meta c end parenthesis end parenthesis suc end line line ell d because prop three two c modus ponens ell b modus ponens ell c indeed macro indent parenthesis meta a plus meta b end parenthesis plus meta c suc equal parenthesis meta a plus parenthesis meta b plus meta c end parenthesis end parenthesis suc end line line ell e because axiom s six indeed macro indent meta b plus meta c suc equal parenthesis meta b plus meta c end parenthesis suc end line line ell f because prop three two i modus ponens ell e indeed macro indent meta a plus parenthesis meta b plus meta c suc end parenthesis equal meta a plus parenthesis meta b plus meta c end parenthesis suc end line line ell g because axiom s six indeed macro indent meta a plus parenthesis meta b plus meta c end parenthesis suc equal parenthesis meta a plus parenthesis meta b plus meta c end parenthesis end parenthesis suc end line line ell h because prop three two c modus ponens ell f modus ponens ell g indeed macro indent meta a plus parenthesis meta b plus meta c suc end parenthesis equal parenthesis meta a plus parenthesis meta b plus meta c end parenthesis end parenthesis suc end line because prop three two d modus ponens ell d modus ponens ell h indeed macro indent parenthesis meta a plus meta b end parenthesis plus meta c suc equal meta a plus parenthesis meta b plus meta c suc end parenthesis end line line ell j end block because deduction modus ponens ell j indeed parenthesis meta a plus meta b end parenthesis plus meta c equal meta a plus parenthesis meta b plus meta c end parenthesis imply parenthesis meta a plus meta b end parenthesis plus meta c suc equal meta a plus parenthesis meta b plus meta c suc end parenthesis qed end math ] "

\item " [ math system s proof of prop three two j reads any term meta a comma meta b comma meta c end line block line ell a because prop three two j one indeed macro indent parenthesis object x plus object y end parenthesis plus zero equal object x plus parenthesis object y plus zero end parenthesis end line line ell b because prop three two j two indeed macro indent parenthesis object x plus object y end parenthesis plus object z equal object x plus parenthesis object y plus object z end parenthesis imply parenthesis object x plus object y end parenthesis plus object z suc equal object x plus parenthesis object y plus object z suc end parenthesis end line because axiom s nine at object z modus ponens ell a modus ponens ell b indeed macro indent parenthesis object x plus object y end parenthesis plus object z equal object x plus parenthesis object y plus object z end parenthesis end line line ell c end block because deduction modus ponens ell c indeed parenthesis meta a plus meta b end parenthesis plus meta c equal meta a plus parenthesis meta b plus meta c end parenthesis qed end math ] "

\end{list}



\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math in theory system s lemma prop three two k one says for all terms meta a comma meta b indeed meta a equal meta b infer meta a times zero equal meta b times zero end lemma end math ] "

\item " [ math system s proof of prop three two k one reads any term meta a comma meta b end line line ell a because axiom s seven indeed meta a times zero equal zero end line line ell b because axiom s seven indeed meta b times zero equal zero end line line ell c because prop three two a indeed zero equal zero end line line ell d because prop three two b modus ponens ell b indeed zero equal meta b times zero end line line ell e because prop three two c indeed meta a times zero equal zero imply zero equal meta b times zero imply meta a times zero equal meta b times zero end line because ell e modus ponens ell a modus ponens ell d indeed meta a times zero equal meta b times zero qed end math ] "

\item " [ math in theory system s lemma prop three two k two says for all terms meta a comma meta b comma meta c indeed meta a equal meta b imply meta a times meta c equal meta b times meta c infer meta a equal meta b imply meta a times meta c suc equal meta b times meta c suc end lemma end math ] "

\item " [ math system s proof of prop three two k two reads any term meta a comma meta b comma meta c end line block any term macro indent meta a comma meta b comma meta c end line line ell a premise macro indent meta a equal meta b imply meta a times meta c equal meta b times meta c end line line ell b premise macro indent meta a equal meta b end line line ell c because ell a modus ponens ell b indeed macro indent meta a times meta c equal meta b times meta c end line line ell d because axiom s eight indeed macro indent meta a times meta c suc equal meta a times meta c plus meta a end line line ell e because axiom s eight indeed macro indent meta b times meta c suc equal meta b times meta c plus meta b end line line ell f because prop three two e indeed macro indent meta a times meta c equal meta b times meta c imply meta a times meta c plus meta a equal meta b times meta c plus meta a end line line ell g because ell f modus ponens ell c indeed macro indent meta a times meta c plus meta a equal meta b times meta c plus meta a end line line ell h because prop three two i indeed macro indent meta a equal meta b imply meta b times meta c plus meta a equal meta b times meta c plus meta b end line line ell i because ell h modus ponens ell c indeed macro indent meta b times meta c plus meta a equal meta b times meta c plus meta b end line line ell j because prop three two c indeed macro indent meta a times meta c plus meta a equal meta b times meta c plus meta a imply meta b times meta c plus meta a equal meta b times meta c plus meta b imply meta a times meta c plus meta a equal meta b times meta c plus meta b end line line ell k because ell j modus ponens ell g modus ponens ell i indeed macro indent meta a times meta c plus meta a equal meta b times meta c plus meta b end line because ell k modus ponens ell d modus ponens ell e indeed macro indent meta a times meta c suc equal meta b times meta c suc end line line ell i end block because deduction modus ponens ell i indeed meta a equal meta b imply meta a times meta c equal meta b times meta c infer meta a equal meta b imply meta a times meta c suc equal meta b times meta c suc qed end math ] "

\item " [ math system s proof of prop three two k reads any term meta a comma meta b comma meta c end line block line ell a because prop three two k one indeed macro indent object x equal object y imply object x times zero equal object y times zero end line line ell b because prop three two k two indeed macro indent object x equal object y imply object x times object z equal object y times object z imply object x equal object y imply object x times object z suc equal object y times object z suc end line because axiom s nine at object z modus ponens ell a modus ponens ell b indeed macro indent object x equal object y imply object x times object z equal object y times object z end line line ell c end block because deduction modus ponens ell c indeed meta a equal meta b infer meta a times meta c equal meta b times meta c qed end math ] "

\end{list}


\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math in theory system s lemma prop three two l one says for all terms meta a indeed zero times zero equal zero end lemma end math ] "
\item " [ math system s proof of prop three two l one reads because axiom s seven indeed zero times zero equal zero qed end math ] "


\item " [ math in theory system s lemma prop three two l two says for all terms meta a indeed zero times meta a equal zero imply zero times meta a suc equal zero end lemma end math ] "

\item " [ math system s proof of prop three two l two reads any term meta a end line block any term macro indent meta a end line line ell a premise macro indent zero times meta a equal zero end line line ell b because axiom s eight indeed macro indent zero times meta a suc equal zero times meta a plus zero end line line ell c because axiom s five indeed macro indent zero times meta a plus zero equal zero times meta a end line line ell d because prop three two c modus ponens ell c modus ponens ell b indeed macro indent zero times meta a suc equal zero times meta a end line because prop three two c modus ponens ell d modus ponens ell a indeed macro indent zero times meta a suc equal zero end line line ell e end block because deduction modus ponens ell e indeed zero times meta a equal zero imply zero times meta a suc equal zero qed end math ] "

\item " [ math system s proof of prop three two l reads any term meta a end line block line ell a because prop three two l one indeed macro indent zero times zero equal zero end line line ell b because prop three two l two indeed macro indent zero times object x equal zero imply zero times object x suc equal zero end line because axiom s nine at object x modus ponens ell a modus ponens ell b indeed macro indent zero times object x equal zero end line line ell c end block because deduction modus ponens ell c indeed zero times meta a equal zero qed end math ] "

\end{list}

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

\item " [ math in theory system s lemma prop three two m one says for all terms meta a indeed meta a suc times zero equal meta t times zero plus zero end lemma end math ] "

\item " [ math system s proof of prop three two m one reads any term meta a end line line ell a because axiom s seven indeed meta a suc times zero equal zero end line line ell b because prop three two f indeed zero equal zero plus zero end line line ell c because axiom s seven indeed zero equal meta a times zero end line line ell d because prop three two e indeed zero equal meta a times zero imply zero plus zero equal meta a times zero plus zero end line line ell e because ell d modus ponens ell c indeed zero plus zero equal meta a times zero plus zero end line line ell g because prop three two c indeed zero equal zero plus zero imply zero plus zero equal meta a times zero plus zero imply zero equal meta a times zero plus zero end line line ell h because ell g modus ponens ell b modus ponens ell e indeed zero equal meta a times zero plus zero end line line ell f because prop three two c indeed meta a suc times zero equal zero imply zero equal meta a times zero plus zero imply meta a suc times zero equal meta a times zero plus zero end line because ell f modus ponens ell a modus ponens ell f indeed meta a suc times zero equal meta a times zero plus zero qed end math ] "

\item " [ math in theory system s lemma prop three two m two says for all terms meta a comma meta b indeed meta a suc times meta b equal meta a times meta b plus meta b imply meta a suc times meta b suc equal meta a times meta b suc plus meta b suc end lemma end math ] "

\item " [ math system s proof of prop three two m two reads any term meta a comma meta b end line block any term macro indent meta a comma meta b end line line ell a premise macro indent meta a suc times meta b equal meta a times meta b plus meta b end line line ell b because axiom s eight indeed macro indent meta a suc times meta b suc equal meta a suc times meta b suc plus meta a suc end line line ell c because prop three two e indeed macro indent meta a suc times meta b equal meta a times meta b plus meta b imply meta a suc times meta b plus meta a suc equal meta a times meta b plus meta b plus meta a suc end line line ell d because ell c modus ponens ell a indeed macro indent meta a suc times meta b plus meta a suc equal meta a times meta b plus meta b plus meta a suc end line line ell e because axiom s six indeed macro indent meta b plus meta a suc equal parenthesis meta b plus meta a end parenthesis suc end line line ell f because prop three two g indeed meta b suc plus meta a equal parenthesis meta b plus meta a end parenthesis suc end line line ell g because prop three two d modus ponens ell e modus ponens ell f indeed macro indent meta b plus meta a suc equal meta b suc plus meta a end line line ell i because prop three two h indeed macro indent meta b suc plus meta a equal meta a plus meta b suc end line line ell l because prop three two c modus ponens ell g modus ponens ell i indeed macro indent meta b plus meta a suc equal meta a plus meta b suc end line line ell h because prop three two i modus ponens ell l indeed macro indent meta a times meta b plus meta b plus meta a suc equal meta a times meta b plus meta a plus meta b suc end line line ell j because axiom s eight indeed macro indent meta a times meta b suc equal meta a times meta b plus meta a end line line ell k because prop three two e modus ponens ell j indeed macro indent meta a times meta b suc plus meta b suc equal meta a times meta b plus meta a plus meta b suc end line line ell m because prop three two d modus ponens ell k modus ponens ell h indeed macro indent meta a times meta b plus meta b plus meta a suc equal meta a times meta b suc plus meta b suc end line line ell n because prop three two c modus ponens ell d modus ponens ell m indeed macro indent meta a suc times meta b plus meta a suc equal meta a times meta b suc plus meta b suc end line because prop three two c modus ponens ell b modus ponens ell n indeed macro indent meta a suc times meta b suc equal meta a times meta b suc plus meta b suc end line line ell o end block because deduction modus ponens ell o indeed meta a suc times meta b equal meta a times meta b plus meta b imply meta a suc times meta b suc equal meta a times meta b suc plus meta b suc qed end math ] "

\item " [ math system s proof of prop three two m reads any term meta a comma meta b end line block line ell a because prop three two m one indeed macro indent object x suc times zero equal object x times zero plus zero end line line ell b because prop three two m two indeed macro indent object x suc times object y equal object x times object y plus object y imply object x suc times object y suc equal object x times object y suc plus object y end line because axiom s nine at object y modus ponens ell a modus ponens ell b indeed macro indent object x suc times object y equal object x times object y plus object y end line line ell c end block because deduction modus ponens ell c indeed meta a suc times meta b equal meta a times meta b plus meta b qed end math ] "

\end{list}

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

\item " [ math in theory system s lemma prop three two n one says for all terms meta a indeed meta a times zero equal zero times meta a end lemma end math ] "

\item " [ math system s proof of prop three two n one reads any term meta a end line line ell a because axiom s seven indeed meta a times zero equal zero end line line ell b because prop three two l indeed zero times meta a equal zero end line because prop three two c modus ponens ell a modus ponens ell b indeed meta a times zero equal zero times meta a qed end math ] "

\item " [ math in theory system s lemma prop three two n two says for all terms meta a comma meta b indeed meta a times meta b equal meta b times meta a imply meta a times meta b suc equal meta b suc times meta a end lemma end math ] "

\item " [ math system s proof of prop three two n two reads any term meta a comma meta b end line block any term macro indent meta a comma meta b end line line ell a premise macro indent meta a times meta b equal meta b times meta a end line line ell b because axiom s eight indeed macro indent meta a times meta b suc equal meta a times meta b plus meta a end line line ell c because prop three two e modus ponens ell a indeed macro indent meta a times meta b plus meta a equal meta b times meta a plus meta a end line line ell d because prop three two b modus ponens prop three two m indeed macro indent meta b times meta a plus meta a equal meta b suc times meta a end line line ell e because prop three two c modus ponens ell e modus ponens ell d indeed macro indent meta a times meta b plus meta a equal meta b suc times meta a end line because prop three two c modus ponens ell b modus ponens ell e indeed macro indent meta a times meta b suc equal meta b suc times meta a end line line ell f end block because deduction modus ponens ell f indeed meta a times meta b equal meta b times meta a imply meta a times meta b suc equal meta b suc times meta s qed end math ] "

\item " [ math system s proof of prop three two n reads any term meta a comma meta b end line block line ell a because prop three two n one indeed macro indent object x times zero equal zero times object x end line line ell b because prop three two n two indeed macro indent object x times object y equal object y times object x imply object x times object y suc equal object y suc times object x end line because axiom s nine at object y modus ponens ell a modus ponens ell b indeed macro indent object x times object y equal object y equal object x end line line ell c end block because deduction modus ponens ell c indeed meta a times meta b equal meta b times meta a qed end math ] "

\end{list}

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math system s proof of prop three two o reads any term meta a comma meta b comma meta c end line block any term macro indent meta a comma meta b comma meta c end line line ell a premise macro indent meta a equal meta b end line line ell b because prop three two k indeed macro indent meta a equal meta b imply meta a times meta c equal meta b times meta c end line line ell c because ell b modus ponens ell a indeed macro indent meta a times meta c equal meta b times meta c end line line ell d because prop three two n indeed macro indent meta a times meta c equal meta c times meta a end line line ell e because prop three two n indeed macro indent meta b times meta c equal meta c times meta b end line line ell f because prop three two c indeed macro indent meta a times meta c equal meta b times meta c imply meta b times meta c equal meta c times meta b imply meta a times meta c equal meta c times meta b end line line ell g because ell f modus ponens ell c modus ponens ell e indeed macro indent meta a times meta c equal meta c times meta b end line line ell h because axiom s one indeed macro indent meta a times meta c equal meta c times meta b imply meta a times meta c equal meta c times meta a imply meta c times meta a equal meta c times meta b end line because ell h modus ponens ell g modus ponens ell d indeed macro indent meta c times meta a equal meta c times meta b end line line ell i end block because deduction modus ponens ell i indeed meta a equal meta b imply meta c times meta a equal meta c times meta b qed end math ] "


\end{list}

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math in theory system s lemma prop three four a says for all terms meta a comma meta b comma meta c indeed meta a times parenthesis meta b plus meta c end parenthesis equal parenthesis meta a times meta b end parenthesis plus parenthesis meta a times meta c end parenthesis end lemma end math ] "

\item " [ math in theory system s lemma prop three four b says for all terms meta a comma meta b comma meta c indeed parenthesis meta b plus meta c end parenthesis times meta a equal parenthesis meta b times meta a end parenthesis plus parenthesis meta c times meta b end parenthesis end lemma end math ] "

\item " [ math in theory system s lemma prop three four c says for all terms meta a comma meta b comma meta c indeed parenthesis meta a times meta b end parenthesis times meta c equal meta a times parenthesis meta b times meta c end parenthesis end lemma end math ] "

\item " [ math in theory system s lemma prop three four d says for all terms meta a comma meta b comma meta c indeed meta a plus meta c equal meta b plus meta c imply meta a equal meta b end lemma 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{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}
\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 {Logiweb sequent calculus, Appendix}
\author {Klaus Grue}
\date {\today}
\maketitle
\tableofcontents








%------------------------------------------------------------------------------
\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{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 protect define pyk of rule div as text "rule div" 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 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 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 x divides x as text ""! divides "!" end text end define linebreak define pyk of pogave as text "pogave" end text end define linebreak unicode end of text end protect end math ] "
\end{flushleft}



\section{\TeX\ definitions}

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

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


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

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

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

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

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

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

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

\item " [ math tex define prop three four a one as "
Prop\ 3.4a_1" end define end math ] "
\item " [ math tex define prop three four a two as "
Prop\ 3.4a_2" end define end math ] "
\item " [ math tex define prop three four a as "
Prop\ 3.4a" end define end math ] "

\item " [ math tex define prop three four b as "
Prop\ 3.4b" end define end math ] "

\item " [ math tex define prop three four c one as "
Prop\ 3.4c_1" end define end math ] "
\item " [ math tex define prop three four c two as "
Prop\ 3.4c_2" end define end math ] "
\item " [ math tex define prop three four c as "
Prop\ 3.4c" end define end math ] "

\item " [ math tex define prop three four d one as "
Prop\ 3.4d_1" end define end math ] "
\item " [ math tex define prop three four d two as "
Prop\ 3.4d_2" end define end math ] "
\item " [ math tex define prop three four d as "
Prop\ 3.4d" end define end math ] "


\item " [ math tex define var x divides var y as "#1.
\| #2." end define end math ] "

\end{list}



\subsection{Variables}
\section{Priority table}

" [ flush left math priority table preassociative priority pogave 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 rule div equal priority axiom s ten 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 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 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 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 end priority greater than preassociative priority x or x equal priority x parallel x equal priority x macro or 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 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 end priority greater than unicode end of text end table end math end left ] "

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