Logiweb expansion of ijcar in pyk

Up Help

"File page.tex
\documentstyle[url]{llncs}

\everymath{\rm}
\everydisplay{\rm}
\input{lgwinclude}

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

\newcommand{\liberalUrlBreak}[1]{{%
\mathcode`\/="!262F%
\mathcode`\0="!2630%
\mathcode`\1="!2631%
\mathcode`\2="!2632%
\mathcode`\3="!2633%
\mathcode`\4="!2634%
\mathcode`\5="!2635%
\mathcode`\6="!2636%
\mathcode`\7="!2637%
\mathcode`\8="!2638%
\mathcode`\9="!2639%
\mathcode`\:="!263A%
\mathcode`\A="!2641%
\mathcode`\B="!2642%
\mathcode`\C="!2643%
\mathcode`\D="!2644%
\mathcode`\E="!2645%
\mathcode`\F="!2646%
%\thinmuskip=0mu%
\medmuskip=0mu plus 2mu minus 0mu%
%\thickmuskip=0mu%
%\def\thinspace{\kern 0em}%
$#1$}}

\let\oldmathbf=\mathbf
\renewcommand{\mathbf}[1]{{\oldmathbf #1}}
\let\oldmathit=\mathit
\renewcommand{\mathit}[1]{{\oldmathit #1}}
\let\oldmathsf=\mathsf
\renewcommand{\mathsf}[1]{{\oldmathsf #1}}

\begin {document}
\title {Something different}
\author {Poul J. Clementsen\inst{1}}
\institute {Department of Computer Science, University of Copenhagen (DIKU)}
\date {\today}
\maketitle

"

begin ragged right

end "



\begin{abstract}
\end{abstract}



\section{Introduction}\label{sec:Introduction}


\section{Conclusion and further work}




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

\end{document}
End of file
File page.bib
@incollection{bruijn80,
author = {Nicolaas Govert de Bruijn},
title = {A Survey of the Project {AUTOMATH}},
editor = {J.P. Seldin and J. R. Hindley},
booktitle = {To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus
and Formalism},
publisher = {Academic Press},
year = {1980},
pages = {579--606}}

@book {church41,
author = {A. Church},
title = {The Calculi of Lambda-Conversion},
publisher = {Princeton University Press},
year = {1941}}

@book {constable86,
author = {Robert L. Constable and S. Allen and H. Bromly and
W. Cleaveland and J. Cremer and R. Harper and D. Howe and
T. Knoblock and N. Mendler and P. Panangaden and J. Sasaki and
S. Smith},
title = {Implementing Mathematics with the Nuprl Proof Development
System},
publisher = {Prentice-Hall},
address = {Englewood Cliffs, New Jersey},
year = {1986}}

@inproceedings{dobbertin96,
author = {Hans Dobbertin and Antoon Bosselaers and Bart Preneel},
title = {{RIPEMD}-160: A Strengthened Version of {RIPEMD}},
booktitle = {Fast Software Encryption},
pages = {71-82},
year = {1996},
note = {\url{http://citeseer.nj.nec.com/dobbertin96ripemd.html}}}

@article {godel31,
author = {K. G{\"!o}del},
title = {{\"!U}ber for\-mal un\-ent\-scheid\-ba\-re
{S\"!at}\-ze der {Prin}\-ci\-pia
{Mathe}\-ma\-ti\-ca und ver\-wand\-ter
{Sys}\-teme {I}},
journal = {Mo\-nats\-hef\-te f{\"!u}r {Mathe}\-ma\-tik und {Phy}\-sik},
year = {19\-31},
volume = {12},
number = {{XXXVIII}},
pages = {173-198}}

@book {gordon79,
author = {M. J. Gordon, A. J. Milner, C. P. Wadsworth},
title = {Edinburgh {LCF}, A mechanised logic of computation},
publisher = {Springer-Verlag},
year = {1979},
volume = {78},
series = {Lecture Notes in Computer Science}}

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

@misc {MathML,
author = {Robert Miner and Jeff Schaeffer},
title = {A Gentle Introduction to {MathML}},
TYPE = {Tutorial},
note = {\url
{http://www.dessci.com/en/support/tutorials/mathml/default.htm}},
year = {2001}}

@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 = {2005},
title = {A Logiweb base page},
institution={Logiweb},
note = {\liberalUrlBreak{\lgwIjcarBaseUrl}}}

@techreport{appendix,
author = {K. Grue},
year = {2006},
title = {Logiweb sequent calculus, appendix},
institution={Logiweb},
note = {\liberalUrlBreak{\lgwIjcarUrl body/tex/appendix.pdf}}}

@misc {kohlhase03,
author = {Michael Kohlhase},
title = {{OMDoc}: An Open Markup Format for Mathematical Documents
(Version 1.1)},
type = {Open Specification},
note = {\url{http://www.mathweb.org/omdoc.ps}},
year = {2003}}

@article {mccarthy60,
author = {J. McCarthy},
title = {Recursive functions of symbolic expressions and their
computation by machine},
journal = {Communications of the ACM},
year = {1960},
pages = {184--195}}

@book {mendelson,
author = {E. Mendelson},
title = {Introduction to Mathematical Logic},
publisher = {Wadsworth and Brooks},
year = {1987},
edition = {3.}}

@manual {matuszewski93,
title = {An Outline of PC Mizar},
author = {Micha{\l} Muzalewski},
editor = {Roman Matuszewski},
year = {1993},
address = {Brussels},
organization
= {Foundation of Logic, Mathematics and Informatics,
Mizar User Group},
file = {/home/mostynm/papers/mizarmanual.ps.gz}}

@techreport {paulson98a,
author = {Lawrence C. Paulson},
title = {Introduction to {Isabelle}},
institution
= {University of Cambridge, Computer Laboratory},
year = {1998}}

@techreport {paulson98b,
author = {Lawrence C. Paulson},
title = {The {Isabelle} Reference Manual},
institution
= {University of Cambridge, Computer Laboratory},
year = {1998}}

@phdthesis {skalberg02,
author = {Sebastian C. Skalberg},
title = {An Interactive Proof System for Map Theory},
school = {University of Copenhagen},
year = {2002},
month = {oct},
note = {\url{http://www.mangust.dk/skalberg/phd/}},
postscript= {\url{http://www.mangust.dk/skalberg/phd/skalberg-phd.ps}}}

@Book {steele,
author = {Guy L. Steele},
title = {Common Lisp---The Language},
publisher = {Digital Press},
year = {1990},
edition = {2.}}

@book {TeXbook,
author = {D. Knuth},
title = {The TeXbook},
publisher = {Addison Wesley},
year = {1983}}

@inproceedings{trybulec85a,
author = {Andrzej Trybulec and Howard Blair},
title = {Computer Assisted Reasoning with {MIZAR}},
pages = {26--28},
booktitle = {Proceedings of the 9th International Joint Conference on
Artificial Intelligence},
editor = {Aravind Joshi},
month = {aug},
year = {1985},
address = {Los Angeles, CA},
publisher = {Morgan Kaufmann},
note = {\url{http://www.mizar.org/}}}

@book {vallee03,
author = {Thierry Vall\'{e}e},
title = {``{Map Theory}'' et Antifondation},
series = {Electronic Notes in Theoretical Computer Science},
volume = {79},
publisher = {Elsevier},
year = {2003},
pages = {1-258}}

End of file
File llncs.sty
% LLNCS DOCUMENT STYLE -- version 1.2
"

then "% for LaTeX version 2.09
"

then "
"

then "% This style file is an adaptation of
"

then "% the original LaTeX article.sty
"

then "
"

then "\typeout{Document Style `llncs', <version 1.2>}
"

then "
"

then "\frenchspacing
"

then "\def~{\penalty\@M\kern3pt}
"

then "
"

then "% Language dependant section
"

then "\def\literaturename{References}
"

then "\def\contentsname{Table of Contents}
"

then "\def\listoffiguresname{List of Figures}
"

then "\def\figurename{Fig.\thinspace}
"

then "\def\listoftablesname{List of Tables}
"

then "\def\tablename{Table }
"

then "\def\abstractname{Abstract.}
"

then "\newif\if@deutsch\@deutschfalse
"

then "%
"

then "\def\ds@deutsch{\typeout{German version}
"

then "\def\literaturename{Literatur}
"

then "\def\contentsname{Inhaltsverzeichnis}
"

then "\def\listoffiguresname{Abbildungsverzeichnis}
"

then "\def\figurename{Abb.\thinspace}
"

then "\def\listoftablesname{Tabellenverzeichnis}
"

then "\def\tablename{Tabelle }
"

then "\def\abstractname{Zusammenfassung.}
"

then "\@deutschtrue}
"

then "
"

then "\def\thebibliography#1{\section*{\literaturename}\small\list
"

then " {\arabic{enumi}.}{\settowidth\labelwidth{#1.}\leftmargin\labelwidth
"

then " \advance\leftmargin\labelsep
"

then " \usecounter{enumi}}
"

then " \def\newblock{\hskip .11em plus .33em minus -.07em}
"

then " \sloppy
"

then " \sfcode`\.=1000\relax}
"

then "
"

then "\def\ds@citeauthoryear{\def\thebibliography##1{\section*{\literaturename}%
"

then " \small\list{}{\settowidth\labelwidth{}\leftmargin\parindent
"

then " \itemindent=-\parindent
"

then " \labelsep=\z@
"

then " \usecounter{enumi}}%
"

then " \def\newblock{\hskip .11em plus .33em minus -.07em}%
"

then " \sloppy
"

then " \sfcode`\.=1000\relax}%
"

then " \def\@cite##1{##1}%
"

then " \def\@lbibitem[##1]##2{\item[]\if@filesw
"

then " {\def\protect####1{\string ####1\space}\immediate
"

then " \write\@auxout{\string\bibcite{##2}{##1}}}\fi\ignorespaces}}%
"

then "
"

then "\newif\if@envcountreset\@envcountresetfalse
"

then "\def\ds@envcountreset{\@envcountresettrue}
"

then "
"

then "\def\@mbi{cmmib10}
"

then "\def\@ptsize{0} \@namedef{ds@11pt}{\def\@ptsize{1}}
"

then "\@namedef{ds@12pt}{\def\@ptsize{2}}
"

then "\def\ds@twoside{\@twosidetrue \@mparswitchtrue}
"

then "\def\ds@draft{\overfullrule
"

then "5pt}
"

then "\@options
"

then "
"

then "\ds@twoside
"

then "
"

then "\lineskip 1pt \normallineskip 1pt
"

then "\def\baselinestretch{1}
"

then "
"

then "\def\@normalsize{\@setsize\normalsize{12pt}\xpt\@xpt
"

then "\abovedisplayskip=3 mm plus6pt minus 4pt
"

then "\belowdisplayskip=3 mm plus6pt minus 4pt
"

then "\abovedisplayshortskip=0mm plus6pt minus 2pt
"

then "\belowdisplayshortskip=2 mm plus4pt minus 4pt}
"

then "
"

then "\mathchardef\Gamma="!0100
"

then "\mathchardef\Delta="!0101
"

then "\mathchardef\Theta="!0102
"

then "\mathchardef\Lambda="!0103
"

then "\mathchardef\Xi="!0104
"

then "\mathchardef\Pi="!0105
"

then "\mathchardef\Sigma="!0106
"

then "\mathchardef\Upsilon="!0107
"

then "\mathchardef\Phi="!0108
"

then "\mathchardef\Psi="!0109
"

then "\mathchardef\Omega="!010A
"

then "
"

then "\def\small{\@setsize\small{11pt}\ixpt\@ixpt
"

then "\abovedisplayskip=2.5 mm plus5pt minus 3pt
"

then "\belowdisplayskip=2.5 mm plus5pt minus 3pt
"

then "\abovedisplayshortskip=0mm plus6pt minus 2pt
"

then "\belowdisplayshortskip=2 mm plus4pt minus 4pt
"

then "\def\@listi{\leftmargin\leftmargini\topsep 4pt plus 2pt minus 2pt}}
"

then "
"

then "\def\footnotesize{\@setsize\footnotesize{11pt}\ixpt\@ixpt
"

then "\abovedisplayskip=2.5 mm plus5pt minus 3pt
"

then "\belowdisplayskip=2.5 mm plus5pt minus 3pt
"

then "\abovedisplayshortskip=0mm plus6pt minus 2pt
"

then "\belowdisplayshortskip=2 mm plus4pt minus 4pt
"

then "\def\@listi{\leftmargin\leftmargini\topsep 4pt plus 2pt minus 2pt}}
"

then "
"

then "\def\scriptsize{\@setsize\scriptsize{8.4pt}\viipt\@viipt}
"

then "
"

then "\def\tiny{\@setsize\tiny{6pt}\vpt\@vpt}
"

then "\def\large{\@setsize\large{13.2pt}\xipt\@xipt}
"

then "\def\Large{\@setsize\Large{14.4pt}\xiipt\@xiipt}
"

then "\def\LARGE{\@setsize\LARGE{16.8pt}\xivpt\@xivpt}
"

then "\def\huge{\@setsize\huge{22pt}\xxpt\@xxpt}
"

then "\def\Huge{\@setsize\Huge{30pt}\xxvpt\@xxvpt}
"

then "\@normalsize
"

then "
"

then "\if@twoside
"

then " \oddsidemargin 44pt
"

then " \evensidemargin 82pt
"

then " \marginparwidth 107pt
"

then "\else \oddsidemargin 63pt \evensidemargin 63pt
"

then " \marginparwidth 90pt
"

then "\fi
"

then "\marginparsep 11pt
"

then "\topmargin 11pt \headheight 12pt \headsep 13.66pt
"

then "\footheight 12pt \footskip 30pt
"

then "\textwidth 12.2truecm
"

then "\textheight 19.3truecm
"

then "\columnsep 1cc \columnseprule 0pt
"

then "
"

then "\footnotesep 7.7pt
"

then "\skip\footins 9pt plus 4pt minus 2pt
"

then "\floatsep 12pt plus 2pt minus 2pt
"

then "\textfloatsep 8mm plus 2pt minus 4pt
"

then "\intextsep 8mm plus 2pt minus 2pt
"

then "\@maxsep 8mm
"

then "
"

then "\dblfloatsep 12pt plus 2pt minus 2pt
"

then "\dbltextfloatsep 20pt plus 2pt minus 4pt
"

then "\@dblmaxsep 20pt
"

then "
"

then "\@fptop 0pt plus 1fil \@fpsep 8pt plus 2fil \@fpbot 0pt plus 1fil
"

then "\@dblfptop0pt plus1fil \@dblfpsep8pt plus2fil\@dblfpbot 0pt plus1fil
"

then "\marginparpush 5pt
"

then "
"

then "\parskip 0pt plus 1pt \parindent 1.5em \topsep 8pt plus 2pt minus 4pt
"

then "\partopsep 2pt plus 1pt minus 1pt \itemsep \z@
"

then "\@lowpenalty 51 \@medpenalty 151 \@highpenalty 301
"

then "\@beginparpenalty-\@lowpenalty\@endparpenalty -\@lowpenalty\@itempenalty
"

then "-\@lowpenalty
"

then "
"

then "\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle\bf#1$}}
"

then "{\mbox{\boldmath$\textstyle\bf#1$}}
"

then "{\mbox{\boldmath$\scriptstyle\bf#1$}}
"

then "{\mbox{\boldmath$\scriptscriptstyle\bf#1$}}}
"

then "
"

then "\def\@sect#1#2#3#4#5#6[#7]#8{\ifnum #2>\c@secnumdepth
"

then " \def\@svsec{}\else
"

then " \refstepcounter{#1}\edef\@svsec{\csname the#1\endcsname\quad }\fi
"

then " \@tempskipa #5\relax
"

then " \ifdim \@tempskipa>\z@
"

then " \begingroup #6\relax
"

then " \noindent{\hskip #3\relax\@svsec}{\interlinepenalty \@M #8\par}
"

then " \endgroup
"

then " \csname #1mark\endcsname{#7}\addcontentsline
"

then " {toc}{#1}{\ifnum #2>\c@secnumdepth \else
"

then " \protect\numberline{\csname the#1\endcsname}\fi
"

then " #7}\else
"

then " \def\@svsechd{#6\hskip #3\@svsec #8\csname #1mark\endcsname
"

then " {#7}\addcontentsline
"

then " {toc}{#1}{\ifnum #2>\c@secnumdepth \else
"

then " \protect\numberline{\csname the#1\endcsname}\fi
"

then " #7}}\fi
"

then " \@xsect{#5}}
"

then "
"

then "\def\part{\par \addvspace{4ex} \@afterindentfalse \secdef\@part\@spart}
"

then "
"

then "\def\@part[#1]#2{\ifnum \c@secnumdepth >\m@ne \refstepcounter{part}
"

then "\addcontentsline{toc}{part}{\thepart \hspace{1em}#1}\else
"

then "\addcontentsline{toc}{part}{#1}\fi { \parindent 0pt \raggedright
"

then " \ifnum \c@secnumdepth >\m@ne \Large \bf
"

then " Part\thepart\par\nobreak\fi\huge
"

then "\bf #2\markboth{}{}\par } \nobreak \vskip 3ex \@afterheading }
"

then "
"

then "\def\@spart#1{{\parindent 0pt \raggedright
"

then " \huge \bf
"

then " #1\par} \nobreak \vskip 3ex \@afterheading }
"

then "
"

then "\def\section{\@startsection {section}{1}{\z@}{-18pt plus -4pt minus
"

then "-4pt}{12pt plus 4pt minus 4pt}{\Large\bf\boldmath
"

then "\pretolerance=10000\relax\rightskip=0pt plus8em}}
"

then "\def\subsection{\@startsection{subsection}{2}{\z@}{-18pt plus-4pt minus
"

then " -4pt}{8pt plus 4pt minus 4pt}{\normalsize\bf\boldmath
"

then "\pretolerance=10000\relax\rightskip=0pt plus8em}}
"

then "\def\subsubsection{\@startsection{subsubsection}{3}{\z@}{-18pt plus-4pt
"

then " minus -4pt}{-0.5em plus -.22em minus -0.1em}{\normalsize\bf\boldmath}}
"

then "\def\paragraph{\@startsection{paragraph}{4}{\z@}{-12pt plus -4pt minus
"

then " -4pt}{-0.5em plus -.22em minus -0.1em}{\normalsize\it}}
"

then "\def\subparagraph#1{\typeout{LLNCS Warning: You should not use
"

then "\protect\subparagraph \space in this style.}\vskip0.5cm
"

then "You should not use $\backslash${\tt subparagraph} in this
"

then "style.\vskip0.5cm}
"

then "
"

then "\setcounter{secnumdepth}{2}
"

then "
"

then "\def\appendix{\par
"

then " \setcounter{section}{0}
"

then " \setcounter{subsection}{0}
"

then " \def\thesection{\Alph{section}}}
"

then "
"

then "\leftmargini 17pt \leftmarginii 17pt
"

then "\leftmarginiii 17pt \leftmarginiv 17pt
"

then "\leftmarginv 10pt \leftmarginvi 10pt
"

then "\leftmargin\leftmargini \labelwidth\leftmargini
"

then "\advance\labelwidth-\labelsep
"

then "\labelsep 5pt
"

then "\parsep 0pt plus 1pt
"

then "\def\@listi{\leftmargin\leftmargini}
"

then "\def\@listii{\leftmargin\leftmarginii
"

then " \labelwidth\leftmarginii\advance\labelwidth-\labelsep
"

then " \topsep 0pt plus 1pt}
"

then "\def\@listiii{\leftmargin\leftmarginiii
"

then " \labelwidth\leftmarginiii\advance\labelwidth-\labelsep
"

then " \topsep 0pt plus 1pt}
"

then "\def\@listiv{\leftmargin\leftmarginiv
"

then " \labelwidth\leftmarginiv\advance\labelwidth-\labelsep
"

then " \topsep 0pt plus 1pt}
"

then "\def\@listv{\leftmargin\leftmarginv
"

then " \labelwidth\leftmarginv\advance\labelwidth-\labelsep
"

then " \topsep 0pt plus 1pt}
"

then "\def\@listvi{\leftmargin\leftmarginvi
"

then " \labelwidth\leftmarginvi\advance\labelwidth-\labelsep
"

then " \topsep 0pt plus 1pt}
"

then "
"

then "\def\labelenumi{\arabic{enumi}.}
"

then "\def\theenumi{\arabic{enumi}}
"

then "\def\labelenumii{(\alph{enumii})}
"

then "\def\theenumii{\alph{enumii}}
"

then "\def\p@enumii{\theenumi}
"

then "\def\labelenumiii{\roman{enumiii}.}
"

then "\def\theenumiii{\roman{enumiii}}
"

then "\def\p@enumiii{\theenumi(\theenumii)}
"

then "\def\labelenumiv{\Alph{enumiv}.}
"

then "\def\theenumiv{\Alph{enumiv}}
"

then "\def\p@enumiv{\p@enumiii\theenumiii}
"

then "
"

then "\def\labelitemi{\bf --}
"

then "\def\labelitemii{$\bullet$}
"

then "\def\labelitemiii{$\ast$}
"

then "\def\labelitemiv{$\cdot$}
"

then "
"

then "\def\verse{\let\\=\@centercr
"

then " \list{}{\itemsep\z@ \itemindent -1.5em\listparindent \itemindent
"

then " \rightmargin\leftmargin\advance\leftmargin 1.5em}\item[]}
"

then "\let\endverse\endlist
"

then "\def\quotation{\list{}{\listparindent 1.5em
"

then " \itemindent\listparindent
"

then " \rightmargin\leftmargin}\item[]}
"

then "\let\endquotation=\endlist
"

then "\def\quote{\list{}{\rightmargin\leftmargin}\item[]}
"

then "\let\endquote=\endlist
"

then "
"

then "\def\descriptionlabel#1{\hspace\labelsep \bf #1}
"

then "\def\description{\list{}{\labelwidth\z@ \itemindent-\leftmargin
"

then " \let\makelabel\descriptionlabel}}
"

then "\let\enddescription\endlist
"

then "
"

then "\def\theequation{\arabic{equation}}
"

then "
"

then "\def\titlepage{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
"

then " \else \newpage \fi \thispagestyle{empty}\c@page\z@}
"

then "\def\endtitlepage{\if@restonecol\twocolumn \else \newpage \fi}
"

then "
"

then "\arraycolsep 1.4pt \tabcolsep 1.4pt \arrayrulewidth .4pt \doublerulesep
"

then "2pt
"

then "\tabbingsep \labelsep
"

then "
"

then "\skip\@mpfootins = \skip\footins
"

then "\fboxsep = 3pt \fboxrule = .4pt
"

then "
"

then "\newcounter{part}
"

then "\newcounter {section}
"

then "\newcounter {subsection}[section]
"

then "\newcounter {subsubsection}[subsection]
"

then "\newcounter {paragraph}[subsubsection]
"

then "
"

then "\def\thepart{\Roman{part}}
"

then "\def\thesection {\arabic{section}}
"

then "\def\thesubsection {\thesection.\arabic{subsection}}
"

then "\def\thesubsubsection {\thesubsection.\arabic{subsubsection}}
"

then "\def\theparagraph {\thesubsubsection.\arabic{paragraph}}
"

then "
"

then "\def\@pnumwidth{1.55em}
"

then "\def\@tocrmarg {2.55em}
"

then "\def\@dotsep{4.5}
"

then "\setcounter{tocdepth}{3}
"

then "
"

then "\def\tableofcontents{\section*{\contentsname}
"

then " \@starttoc{toc}}
"

then "\def\l@part#1#2{\addpenalty{\@secpenalty}
"

then " \addvspace{2.25em plus 1pt} \begingroup
"

then " \@tempdima 3em \parindent \z@ \rightskip \@pnumwidth \parfillskip
"

then "-\@pnumwidth
"

then " {\Large \bf \leavevmode #1\hfil \hbox to\@pnumwidth{\hss #2}}\par
"

then " \nobreak \endgroup}
"

then "%
"

then "\def\numberline#1{\advance\hangindent by\@tempdima%
"

then "\hbox to\@tempdima{\hss#1\enspace}}
"

then "%
"

then "\def\bf@dottedtocline#1#2#3#4#5{\ifnum #1>\c@tocdepth \else
"

then " \vskip \z@ plus .2pt
"

then " {\leftskip #2\relax \rightskip \@tocrmarg \parfillskip -\rightskip
"

then " \parindent #2\relax\@afterindenttrue
"

then " \interlinepenalty\@M
"

then " \leavevmode
"

then " \@tempdima #3\relax \advance\leftskip \@tempdima \hbox{}\hskip
"

then " -\leftskip
"

then "{\bf#4}\nobreak\leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern \@dotsep
"

then " mu$}\hfill \nobreak \hbox to\@pnumwidth{\hfil\rm #5}\par}\fi}
"

then "%
"

then "\def\l@section{\vskip2mm\bf@dottedtocline{1}{0em}{1.7em}}
"

then "\def\l@subsection{\@dottedtocline{2}{1.7em}{2.3em}}
"

then "\def\l@subsubsection{\@dottedtocline{3}{4em}{2em}}
"

then "\def\l@paragraph{\@dottedtocline{4}{6em}{2em}}
"

then "\def\l@subparagraph{\@dottedtocline{5}{8em}{2em}}
"

then "\def\listoffigures{\section*{\listoffiguresname\markboth
"

then " {\listoffiguresname}{\listoffiguresname}}\@starttoc{lof}}
"

then "\def\l@figure{\@dottedtocline{1}{1.5em}{2.3em}}
"

then "\def\listoftables{\section*{\listoftablesname\markboth
"

then " {\listoftablesname}{\listoftablesname}}\@starttoc{lot}}
"

then "\let\l@table\l@figure
"

then "
"

then "\def\endthebibliography{\endlist\normalsize}
"

then "
"

then "\newif\if@restonecol
"

then "\def\theindex{\@restonecoltrue\if@twocolumn\@restonecolfalse\fi
"

then "\columnseprule \z@
"

then "\columnsep 35pt\twocolumn[\section*{Index}]
"

then " \markboth{Index}{Index}\thispagestyle{plain}\parindent\z@
"

then " \parskip\z@ plus .3pt\relax\let\item\@idxitem}
"

then "\def\@idxitem{\par\hangindent 40pt}
"

then "\def\subitem{\par\hangindent 40pt \hspace*{20pt}}
"

then "\def\subsubitem{\par\hangindent 40pt \hspace*{30pt}}
"

then "\def\endtheindex{\if@restonecol\onecolumn\else\clearpage\fi}
"

then "\def\indexspace{\par \vskip 10pt plus 5pt minus 3pt\relax}
"

then "
"

then "\def\footnoterule{\kern-3\p@\hrule width 2 true cm\kern 2.6\p@}
"

then "
"

then "\long\def\@makefntext#1{\@setpar{\@@par\@tempdima \hsize
"

then " \advance\@tempdima-1em\parshape \@ne 1em\@tempdima}\par
"

then " \parindent 1em\noindent \hbox to \z@{\hss$^{\@thefnmark}$\ }#1}
"

then "
"

then "\setcounter{topnumber}{2}
"

then "\def\topfraction{.9}
"

then "\setcounter{bottomnumber}{1}
"

then "\def\bottomfraction{.3}
"

then "\setcounter{totalnumber}{3}
"

then "\def\textfraction{.15}
"

then "\def\floatpagefraction{.85}
"

then "\setcounter{dbltopnumber}{2}
"

then "\def\dbltopfraction{.85}
"

then "\def\dblfloatpagefraction{.85}
"

then "
"

then "\long\def\@makecaption#1#2{
"

then " \vskip 10pt
"

then " \setbox\@tempboxa\hbox{{\bf #1} #2}
"

then " \ifdim \wd\@tempboxa >\hsize \unhbox\@tempboxa\par \else \hbox
"

then "to\hsize{\hfil\box\@tempboxa\hfil}
"

then " \fi\vskip5pt}
"

then "
"

then "\long\def\@caption#1[#2]#3{\addcontentsline{\csname
"

then " ext@#1\endcsname}{#1}{\protect\numberline{\csname
"

then " the#1\endcsname}{\ignorespaces #2}}\par
"

then " \begingroup
"

then " \@parboxrestore
"

then " \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
"

then " \endgroup}
"

then "
"

then "\newcounter{figure}
"

then "\def\thefigure{\@arabic\c@figure}
"

then "
"

then "\def\fps@figure{htbp}
"

then "\def\ftype@figure{1}
"

then "\def\ext@figure{lof}
"

then "\def\fnum@figure{\figurename\thefigure.}
"

then "\def\figure{\small\rm\@float{figure}}
"

then "\def\endfigure{\vskip-5pt\end@float}
"

then "\@namedef{figure*}{\@dblfloat{figure}}
"

then "\@namedef{endfigure*}{\end@dblfloat}
"

then "
"

then "\newcounter{table}
"

then "\def\thetable{\@arabic\c@table}
"

then "\def\fps@table{htbp}
"

then "\def\ftype@table{2}
"

then "\def\ext@table{lot}
"

then "\def\fnum@table{\tablename\thetable.}
"

then "\def\table{\small\rm\@float{table}}
"

then "\let\endtable\end@float
"

then "\@namedef{table*}{\@dblfloat{table}}
"

then "\@namedef{endtable*}{\end@dblfloat}
"

then "
"

then "% LaTeX does not provide a command to enter the authors institute
"

then "% addresses. The \institute command is defined here.
"

then "
"

then "\newcounter{@inst}
"

then "\newcounter{@auth}
"

then "
"

then "\def\institute#1{\gdef\@institute{#1}}
"

then "
"

then "\def\institutename{\par
"

then " \begingroup
"

then " \parskip=\z@
"

then " \parindent=\z@
"

then " \setcounter{@inst}{1}%
"

then " \def\and{\par\stepcounter{@inst}%
"

then " \noindent$^{\the@inst}$\enspace\ignorespaces}%
"

then " \setbox0=\vbox{\def\thanks##1{}\@institute}%
"

then " \ifnum\c@@inst=1\relax
"

then " \else
"

then " \setcounter{footnote}{\c@@inst}%
"

then " \setcounter{@inst}{1}%
"

then " \noindent$^{\the@inst}$\enspace
"

then " \fi
"

then " \ignorespaces
"

then " \@institute\par
"

then " \endgroup}
"

then "
"

then "\def\@thanks{}
"

then "
"

then "\def\@fnsymbol#1{\ifcase#1\or\star\or{\star\star}\or{\star\star\star}%
"

then " \or \dagger\or \ddagger\or
"

then " \mathchar "!278\or \mathchar "!27B\or \|\or **\or \dagger\dagger
"

then " \or \ddagger\ddagger\else\@ctrerr\fi\relax}
"

then "
"

then "\def\inst#1{\unskip$^{#1}$}
"

then "
"

then "\def\subtitle#1{\gdef\@subtitle{#1}}
"

then "\def\@subtitle{}
"

then "
"

then "\def\maketitle{\par
"

then " \begingroup
"

then " \parindent=\z@
"

then " \def\thefootnote{\fnsymbol{footnote}}
"

then " \if@twocolumn
"

then " \twocolumn[\@maketitle]
"

then " \else \newpage
"

then " \global\@topnum\z@ \@maketitle \fi\thispagestyle{empty}\@thanks
"

then " \endgroup
"

then " \let\maketitle\relax
"

then " \let\@maketitle\relax
"

then " \gdef\@thanks{}\gdef\@author{}\gdef\@title{}\gdef\@subtitle{}%
"

then " \let\thanks\relax}
"

then "
"

then "\def\@maketitle{\newpage
"

then " \begin{center}%
"

then " {\LARGE \bf\boldmath
"

then " \pretolerance=10000
"

then " \@title \par}\vskip .8cm
"

then "\if!\@subtitle!\else {\Large \bf\boldmath
"

then " \vskip -.65cm
"

then " \pretolerance=10000
"

then " \@subtitle \par}\vskip .8cm\fi
"

then "{\normalsize\rm\lineskip .5em
"

then "\@author\vskip.35cm}
"

then " {\small\rm\institutename}
"

then " \end{center}%
"

then " }
"

then "
"

then "\mark{{}{}}
"

then "
"

then "% Define `abstract' environment
"

then "\def\abstract{%
"

then "\list{}{\advance\topsep by0.35cm\relax\small\rm
"

then " \leftmargin=1cm
"

then " \labelwidth=\z@
"

then " \listparindent=\z@
"

then " \itemindent\listparindent
"

then " \rightmargin\leftmargin}\item[\hskip\labelsep\bf\abstractname]}
"

then "\let\endabstract=\endlist
"

then "\def\quote{\list{}{\rightmargin\leftmargin}\item[]}
"

then "\let\endquote=\endlist
"

then "
"

then "\def\ps@headings{\def\@evenhead{}%
"

then "\let\@oddhead\@evenhead
"

then "\let\@evenfoot\@evenhead
"

then "\let\@oddfoot\@evenhead
"

then "\def\sectionmark##1{}%
"

then "\def\subsectionmark##1{}}
"

then "\def\ps@myheadings{\let\@mkboth\@gobbletwo
"

then "\def\@oddhead{\hbox{}\small\rm\rightmark \hfil\thepage}%
"

then "\def\@oddfoot{}\def\@evenhead{\small\rm\thepage\hfil
"

then "\leftmark\hbox {}}%
"

then "\def\@evenfoot{}\def\sectionmark##1{}\def\subsectionmark##1{}}
"

then "
"

then "\def\today{\ifcase\month\or
"

then " January\or February\or March\or April\or May\or June\or
"

then " July\or August\or September\or October\or November\or December\fi
"

then " \space\number\day, \number\year}
"

then "
"

then "\ps@headings \pagenumbering{arabic} \onecolumn
"

then "\if@twoside\else\raggedbottom\fi
"

then "
"

then "% new environments and theorems
"

then "% borrowed form the LTMP-style of Springer-Verlag
"

then "% designed by Dr. Christoph Ender
"

then "%
"

then "% define the new theorem like environments
"

then "% define a new style of environments where it is possible to define
"

then "% the font % used as the theorem name and the fontfamily for the text.
"

then "%
"

then "% \newstytheorem{name}{thefont}{txtfont}{Text}[Counter]
"

then "% \newstytheorem{name}{thefont}{txtfont}[oldname]{Text}
"

then "%
"

then "% #1 - name of theorem
"

then "% #2 - theorem font
"

then "% #3 - text font
"

then "%
"

then "\def\newstytheorem#1#2#3{%
"

then "\@ifnextchar[{\che@othm{#1}{#2}{#3}}{\che@nthm{#1}{#2}{#3}}}
"

then "%
"

then "% #1 - name of theorem
"

then "% #2 - theorem font
"

then "% #3 - text font
"

then "% #4 - text string of thorem name
"

then "%
"

then "\def\che@nthm#1#2#3#4{%
"

then "\@ifnextchar[{\che@xnthm{#1}{#2}{#3}{#4}}{\che@ynthm{#1}{#2}{#3}{#4}}}
"

then "%
"

then "% #1 - name of theorem
"

then "% #2 - theorem font
"

then "% #3 - text font
"

then "% #4 - text string of thorem name
"

then "% #5 - add theorem counter to reset list of another counter
"

then "%
"

then "\def\che@xnthm#1#2#3#4[#5]{\expandafter
"

then "\@ifdefinable\csname #1\endcsname
"

then "{\@definecounter{#1}\if@envcountreset\@addtoreset{#1}{#5}\fi
"

then "\expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
"

then "\global\@namedef{#1}{\che@thm{#1}{#4}{#2}{#3}}\global
"

then "\@namedef{end#1}{\@endtheorem}}}
"

then "%
"

then "% #1 - name of theorem
"

then "% #2 - theorem font
"

then "% #3 - text font
"

then "% #4 - text string of thorem name
"

then "%
"

then "\def\che@ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
"

then "{\@definecounter{#1}%
"

then "\expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
"

then "\global\@namedef{#1}{\che@thm{#1}{#2}{#3}{#4}}\global
"

then "\@namedef{end#1}{\@endtheorem}}}
"

then "%
"

then "% change oldthm if oldname in specification is '*'
"

then "% then don't use a counter
"

then "% #1 - countername
"

then "% #2 - theorem font
"

then "% #3 - text font
"

then "% #4 - counter used
"

then "% #5 - string containing theorem name to print
"

then "%
"

then "\def\che@othm#1#2#3[#4]#5{\expandafter\@ifdefinable
"

then "\csname#1\endcsname%
"

then "{\@@othm@{#1}{#2}{#3}{#4}{#5}\global\@namedef{end#1}{\@endtheorem}}}
"

then "%
"

then "\def\@@othm@#1#2#3#4#5{\if *#4{\global\@namedef{the#1}{\relax}
"

then "\global\@namedef{#1}{\@bthm@{}{#5}{#2}{#3}}}\else
"

then "{\global\@namedef{the#1}{\@nameuse{the#4}}% define the counter
"

then "\global\@namedef{#1}{\che@thm{#4}{#5}{#2}{#3}}}\fi}
"

then "%
"

then "% new defs for theorem environment che 17-MAR-1989
"

then "% it improves the option possible
"

then "%
"

then "% #1 - countername = theorem name
"

then "% #2 - string containing theorem name to print
"

then "% #3 - theorem font
"

then "% #4 - text font
"

then "\def\che@thm#1#2#3#4{\@ifnextchar({\@athm{#1}{#2}{#3}{#4}}{%
"

then "\@ifnextchar *{\@bthm{#1}{#2}{#3}{#4}}%
"

then "{\@@thm{#1}{#2}{#3}{#4}}}}
"

then "%
"

then "% \begin{thm}(A.1)[test] results in:
"

then "% \end{thm} thm A.1 (test) ....
"

then "% #1 - theorem
"

then "% #2 - string of theorem name
"

then "% #3 - font for theorem name and label
"

then "% #4 - Text font
"

then "% #5 - is the new label
"

then "% #6 - optional string
"

then "%
"

then "\def\@athm#1#2#3#4(#5){\@ifnextchar[{%
"

then "\@aythm{#1}{#2}{#3}{#4}{#5}}{\@axthm{#1}{#2}{#3}{#4}{#5}}}
"

then "\def\@axthm#1#2#3#4#5{\@@locthmlab{#1}{#5}%
"

then "\@begintheorem{#2}{#5}{#3}{#4}\ignorespaces}
"

then "\def\@aythm#1#2#3#4#5[#6]{\@@locthmlab{#1}{#5}%
"

then "\fuh@opargbegintheorem{#2}{#5}{#6}{#3}{#4}\ignorespaces}
"

then "%
"

then "% \begin{thm}*[xytest] results in:
"

then "% \end{thm} thm (xytest) ....
"

then "% #1 - theorem
"

then "% #2 - string of theorem name
"

then "% #3 - font for theorem name and label
"

then "% #4 - Text font
"

then "% #5 - optional string
"

then "%
"

then "\def\@bthm@#1#2#3#4{\@ifnextchar[{\@bythm{#1}{#2}{#3}{#4}}{%
"

then "\@bxthm{#1}{#2}{#3}{#4}}}
"

then "\def\@bthm#1#2#3#4*{\@ifnextchar[{\@bythm{#1}{#2}{#3}{#4}}{%
"

then "\@bxthm{#1}{#2}{#3}{#4}}}
"

then "\def\@bxthm#1#2#3#4{\if !#1!\relax\else\@@locthmlab{#1}{}\fi
"

then "\@@begintheorem{#2}{#3}{#4}\ignorespaces}
"

then "\def\@bythm#1#2#3#4[#5]{%
"

then "\@@opargbegintheorem{#2}{#3}{#4}{#5}\ignorespaces}
"

then "%
"

then "% define local label
"

then "% if no number or a user specified label occured
"

then "%
"

then "\def\@@locthmlab#1#2{\expandafter\def\csname the#1\endcsname{#2}
"

then "\let\@chetempa\protect\def\protect{\noexpand\protect\noexpand}%
"

then "\edef\@currentlabel{\csname p@#1\endcsname\csname the#1\endcsname}%
"

then "\let\protect\@chetempa}
"

then "%
"

then "% #1 - counter = theorem name
"

then "% #2 - string with name
"

then "% #3 - font for theorem name and label
"

then "% #4 - font for text
"

then "\def\@@thm#1#2#3#4{\refstepcounter
"

then " {#1}\@ifnextchar[{\che@ythm{#1}{#2}{#3}{#4}}{%
"

then " \che@xthm{#1}{#2}{#3}{#4}}}
"

then "%
"

then "\def\che@xthm#1#2#3#4{\che@begintheorem{#2}{\csname
"

then "the#1\endcsname}{#3}{#4}\ignorespaces}
"

then "\def\che@ythm#1#2#3#4[#5]{\che@opargbegintheorem{#2}{\csname
"

then " the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
"

then "%
"

then "% #1 - name of theorem
"

then "% #2 - label string
"

then "% #3 - font for name and lable
"

then "% #4 - text fomt
"

then "%
"

then "\def\che@begintheorem#1#2#3#4{#4\trivlist\item[\hskip\labelsep
"

then "#3#1\ts #2.]}
"

then "%
"

then "% #1 - name of theorem
"

then "% #2 - label string
"

then "% #3 - additonal text
"

then "% #4 - font for name and lable
"

then "% #5 - text fomt
"

then "%
"

then "\def\che@opargbegintheorem#1#2#3#4#5{#5\trivlist
"

then "\item[\hskip\labelsep#4#1\ts #2\ #3.]}
"

then "%
"

then "\def\fuh@opargbegintheorem#1#2#3{\it \trivlist
"

then " \item[\hskip \labelsep{\bf #1\ #2\ (#3).}]}
"

then "%
"

then "\def\@@begintheorem#1#2#3{#3\trivlist\item[\hskip\labelsep
"

then "#2#1.]}
"

then "\def\@@opargbegintheorem#1#2#3#4{#3\trivlist\item[\hskip\labelsep
"

then "#2#1 #4.]}
"

then "
"

then "\if@deutsch
"

then "\newstytheorem{theorem}{\bf}{\it}{Theorem}[section]
"

then "\newstytheorem{example}{\it}{\rm}{Beispiel}[section]
"

then "\newstytheorem{proposition}{\bf}{\it}[theorem]{Proposition}
"

then "\newstytheorem{corollary}{\bf}{\it}[theorem]{Korollar}
"

then "\newstytheorem{lemma}{\bf}{\it}[theorem]{Lemma}
"

then "\newstytheorem{proof}{\it}{\rm}[*]{Beweis}
"

then "\newstytheorem{definition}{\bf}{\rm}[theorem]{Definition}
"

then "\newstytheorem{remark}{\it}{\rm}[*]{Anmerkung}
"

then "\newstytheorem{exercise}{\it}{\rm}[theorem]{\"!{U}bung}
"

then "\newstytheorem{problem}{\it}{\rm}[theorem]{Problem}
"

then "\newstytheorem{solution}{\it}{\rm}[theorem]{L\"!{o}sung}
"

then "\newstytheorem{note}{\it}{\rm}[theorem]{Hinweis}
"

then "\newstytheorem{question}{\it}{\rm}[theorem]{Frage}
"

then "\else
"

then "\newstytheorem{theorem}{\bf}{\it}{Theorem}[section]
"

then "\newstytheorem{example}{\it}{\rm}{Example}[section]
"

then "\newstytheorem{proposition}{\bf}{\it}[theorem]{Proposition}
"

then "\newstytheorem{corollary}{\bf}{\it}[theorem]{Corollary}
"

then "\newstytheorem{lemma}{\bf}{\it}[theorem]{Lemma}
"

then "\newstytheorem{proof}{\it}{\rm}[*]{Proof}
"

then "\newstytheorem{definition}{\bf}{\rm}[theorem]{Definition}
"

then "\newstytheorem{remark}{\it}{\rm}[*]{Remark}
"

then "\newstytheorem{exercise}{\it}{\rm}[theorem]{Exercise}
"

then "\newstytheorem{problem}{\it}{\rm}[theorem]{Problem}
"

then "\newstytheorem{solution}{\it}{\rm}[theorem]{Solution}
"

then "\newstytheorem{note}{\it}{\rm}[theorem]{Note}
"

then "\newstytheorem{question}{\it}{\rm}[theorem]{Question}
"

then "\fi
"

then "
"

then "\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
"

then "\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
"

then "\penalty50\hskip1em\null\nobreak\hfil\squareforqed
"

then "\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}
"

then "
"

then "\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
"

then "\halign{\hfil
"

then "$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
"

then "{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
"

then "\cr\to\cr}}}
"

then "{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
"

then "\cr\to\cr}}}
"

then "{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
"

then "\gets\cr\to\cr}}}}}
"

then "\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
"

then "$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
"

then "{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
"

then "\noalign{\vskip1.2pt}=\cr}}}
"

then "{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
"

then "\noalign{\vskip1pt}=\cr}}}
"

then "{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
"

then "<\cr
"

then "\noalign{\vskip0.9pt}=\cr}}}}}
"

then "\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
"

then "$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
"

then "{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
"

then "\noalign{\vskip1.2pt}=\cr}}}
"

then "{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
"

then "\noalign{\vskip1pt}=\cr}}}
"

then "{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
"

then ">\cr
"

then "\noalign{\vskip0.9pt}=\cr}}}}}
"

then "\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
"

then "\halign{\hfil
"

then "$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
"

then "{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
"

then ">\cr\noalign{\vskip-1pt}<\cr}}}
"

then "{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
"

then ">\cr\noalign{\vskip-0.8pt}<\cr}}}
"

then "{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
"

then ">\cr\noalign{\vskip-0.3pt}<\cr}}}}}
"

then "\def\bbbr{{\rm I\!R}} %reelle Zahlen
"

then "\def\bbbm{{\rm I\!M}}
"

then "\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
"

then "\def\bbbf{{\rm I\!F}}
"

then "\def\bbbh{{\rm I\!H}}
"

then "\def\bbbk{{\rm I\!K}}
"

then "\def\bbbp{{\rm I\!P}}
"

then "\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
"

then "{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
"

then "\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
"

then "to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
"

then "{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
"

then "to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
"

then "{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
"

then "to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
"

then "{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
"

then "to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
"

then "\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
"

then "Q$}\hbox{\raise
"

then "0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
"

then "{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
"

then "0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
"

then "{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
"

then "0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
"

then "{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
"

then "0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
"

then "\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
"

then "T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
"

then "{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
"

then "to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
"

then "{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
"

then "to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
"

then "{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
"

then "to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
"

then "\def\bbbs{{\mathchoice
"

then "{\setbox0=\hbox{$\displaystyle \rm S$}\hbox{\raise0.5\ht0\hbox
"

then "to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
"

then "to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
"

then "{\setbox0=\hbox{$\textstyle \rm S$}\hbox{\raise0.5\ht0\hbox
"

then "to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
"

then "to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
"

then "{\setbox0=\hbox{$\scriptstyle \rm S$}\hbox{\raise0.5\ht0\hbox
"

then "to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
"

then "to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
"

then "{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
"

then "to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
"

then "to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
"

then "\def\bbbz{{\mathchoice {\hbox{$\sf\textstyle Z\kern-0.4em Z$}}
"

then "{\hbox{$\sf\textstyle Z\kern-0.4em Z$}}
"

then "{\hbox{$\sf\scriptstyle Z\kern-0.3em Z$}}
"

then "{\hbox{$\sf\scriptscriptstyle Z\kern-0.2em Z$}}}}
"

then "\def\ts{\thinspace}
"

then "
"

then "\if@deutsch
"

then "\def\typeset{\vfill\small\noindent Dieser Artikel wurde mit
"

then "dem \LaTeX\ Makro-Paket und dem LLNCS-Style formatiert.\par}
"

then "\else
"

then "\def\typeset{\vfill\small\noindent This article was processed using
"

then "the \LaTeX\ macro package with LLNCS style\par}
"

then "\fi
"

then "
"

then "\def\enddocument{\par\typeset
"

then "\@checkend{document}\clearpage\begingroup
"

then "\if@filesw \immediate\closeout\@mainaux
"

then "\def\global\@namedef##1##2{}\def\newlabel{\@testdef r}%
"

then "\def\bibcite{\@testdef b}\@tempswafalse\makeatletter\input \jobname.aux
"

then "\if@tempswa \@warning{Label(s) may have changed. Rerun to get
"

then "cross-references right}\fi\fi\endgroup\deadcycles\z@\@@end}
"

then "\endinput
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



\section{Introduction}

The present appendix is part of the {\em Logiweb page} available at

\begin{raggedright}
\begin{sloppypar}
\noindent \url{\lgwIjcarUrl body/tex/page.pdf}.
\end{sloppypar}
\end{raggedright}

The hex number which contains a RIPEMD-160 \cite{dobbertin96} hash key and a time stamp identifies the present paper uniquely on Logiweb. The part before the hex number is the address of a {\em Logiweb relay} which redirects the users browser to the paper. That part can be replaced by the address of any Logiweb relay. The part after the hex number indicates the address of the body of the paper relative to the official, binary representation (2/ is shorthand for ../../).

Actually, the present page is rendered as three pdf files present at \href{\lgwIjcarUrl body/tex/page.pdf}{2\linebreak [0]/\linebreak [0]body\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]page.pdf}, \href{\lgwIjcarUrl body/tex/appendix.pdf}{2\linebreak [0]/\linebreak [0]body\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]appendix.pdf}, and \href{\lgwIjcarUrl body/tex/chores.pdf}{2\linebreak [0]/\linebreak [0]body\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]chores.pdf} where appendix.pdf is the present appendix. Many proofs and definitions are deferred to the present appendix to spare the reader of the main paper in the page.pdf file. The chores.pdf file defines how to render each construct in \TeX. A good place to start browsing is \href{\lgwIjcarUrl index.html}{2\linebreak [0]/\linebreak [0]index.html}.

Each Logiweb page has a Logiweb bibliography which lists previously published pages which the present page relies on. The present Logiweb page references the \href{\lgwIjcarBaseUrl index.html}{base} page at

\begin{raggedright}
\begin{sloppypar}
\noindent \url{\lgwIjcarBaseUrl body/tex/page.pdf}.
\end{sloppypar}
\end{raggedright}

\noindent which defines the proof system used to verify the present page (c.f. \href{\lgwIjcarUrl bibliography/tex/page.pdf}{2\linebreak [0]/\linebreak [0]bibliography\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]page.pdf}).

As mentioned in the main paper, the user friendliness of the Logiweb sequent calculus is achieved by using the Turing complete macro expansion facility of Logiweb. To see the proofs present in the main paper after macro expansion, consult \href{\lgwIjcarUrl expansion/tex/page.pdf}{2\linebreak [0]/\linebreak [0]expansion\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]page.pdf}. To see the proofs of the present appendix after macro expansion, consult \href{\lgwIjcarUrl expansion/tex/appendix.pdf}{2\linebreak [0]/\linebreak [0]expansion\linebreak [0]/\linebreak [0]tex\linebreak [0]/\linebreak [0]appendix.pdf}.



\section{Notation}

\subsection{Hiding construct}

"

begin math proclaim var x hide as text "hide" end text end proclaim end math

end " proclaims "

begin math var x hide end math

end " to denote hiding. We introduce it here to have a visible hiding construct instead of the invisible `unicode start of text' operator normally used for hiding, c.f.\ the \href{\lgwIjcarBaseUrl index.html}{base} page. The use of hiding in "

begin math define macro of var x 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 as var y end define end quote end define end define hide end math

end " later in this appendix is play for the gallery since the "

begin math var x end math

end " is introduced on the \href{\lgwIjcarBaseUrl index.html}{base} page and since macro definitions only have effect when they occur on the home page of the construct being macro defined.



\subsection{Metaquantification}\label{section:Metaquantification}

The following macro definition makes e.g.\ "

begin math all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var d end metavar end math

end " expand into "

begin math all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var d end metavar end math

end ". Note that "

begin math all var x indeed var y end math

end " is meta quantification as defined on the \href{\lgwIjcarBaseUrl index.html}{base} page which, unfortunately, is rendered exactly like object quantification in the present document. Such notational clashes are unavoidable in mathematics in general but becomes extremely visible in a system like Logiweb where referenced papers are only a click away. To avoid confusion between the two, identically looking quantifiers, we only use the meta quantifier from the base page in the macro definition below and otherwise use "

begin math for all objects var x indeed var y end math

end " to denote object quantification. The "

begin math var x end math

end " operator used in the definition protects against macro expansion. The left hand side of the macro definition is protected against macro expansion as is the `recursive' call of the macro that occurs in the right hand side.

\vspace{1ex}

\noindent "

begin math define macro of for all terms var x indeed var y as lambda var t dot lambda var s dot lambda var c dot state expand tagged if not var t first term root equal quote var x comma var y end quote then quote expand var t term quote all var x indeed var y end quote stack quote var x end quote pair var t first pair quote var y end quote pair var t second pair true end expand else quote expand var t term quote all var x indeed for all terms var y indeed var z end quote stack quote var x end quote pair var t first first pair quote var y end quote pair var t first second pair quote var z end quote pair var t second pair true end expand end if state var s cache var c end expand end define end math

end "

\vspace{1ex}

\noindent The definition above is a general macro definition as opposed to more restricted macro definitions like "

begin math define macro of any term var i end line var p 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 any term var i end line var p as for all terms var i indeed var p end define end quote end define end define end math

end " which just define a left hand side to expand into a right hand side. The "

begin math define macro of var x 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 as var y end define end quote end define end define hide end math

end " construct itself is defined by a general macro definition and happens to expand into a general macro definition, so the "

begin math define macro of var x 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 as var y end define end quote end define end define hide end math

end " construct is just syntactic sugar.

A general macro definition assigns a `macro' aspect to the principal operator of the right hand side. The definition ignores the parameters of the principal operator. Instead, the right hand side of the general macro definition must take three arguments, "

begin math var t end math

end ", "

begin math var s end math

end ", and "

begin math var c end math

end ". When a macro aspect is invoked, it is applied to the term "

begin math var t end math

end " to be expanded, a `macro state' "

begin math var s end math

end ", and a `Logiweb cache' "

begin math var c end math

end ".

The macro state should itself be a function of three parameters "

begin math var t end math

end ", "

begin math var s end math

end ", and "

begin math var c end math

end " and it is the function to be invoked when continuing the macro expansion. A macro like the macro protection macro "

begin math var x end math

end " protects its argument "

begin math var x end math

end " against macro expansion by returning it instead of calling "

begin math var s end math

end " on it. The construct above calls the general macro expansion invokation function "

begin math state expand var t state var s cache var c end expand end math

end " which simply applies "

begin math var s end math

end " to "

begin math var t end math

end ", "

begin math var s end math

end ", and "

begin math var c end math

end ". So the definition above does something to "

begin math var t end math

end " and then continues macro expansion.

The Logiweb cache "

begin math var c end math

end " is the cache of the home page of "

begin math var t end math

end ", i.e.\ the page on which "

begin math var t end math

end " occurs. The cache contains, among other, all definitions present on the home page and all pages transitively referenced by the home page. It also contains other things like compiled versions of all value defined constructs. This is badly needed for efficiency reasons because macro expansion is done not by the Logiweb computing engine itself but by a self-interpretter which is run by the Logiweb engine and simulates the Logiweb engine. This self-interpretter, which resides inside the macro state "

begin math var s end math

end ", fetches compiled versions of constructs from the cache "

begin math var c end math

end " for efficiency reasons.

The term "

begin math var t end math

end " has the structure described in Section \ref{section:LogiwebTerms}. "

begin math var t second end math

end " is the second subtree of "

begin math var t end math

end " and "

begin math var t first second end math

end " is the second subtree of the first subtree of "

begin math var t end math

end ". "

begin math var t term root equal var t prime end math

end " is true when "

begin math var t end math

end " and "

begin math var t prime end math

end " have the same principal operator.

The "

begin math quote expand var t term var p stack var a end expand end math

end " construct expands the pattern "

begin math var p end math

end " according to the association list "

begin math var a end math

end ". Some day, when the author has some spare time, a new version of "

begin math quote expand var t term var p stack var a end expand end math

end " will be implemented in which the association list is replaced by a facility like the `comma' in Lisp backquotes.

The construct "

begin math quote expand var t term var p stack var a end expand end math

end " not only expands the pattern "

begin math var p end math

end " according to the association list "

begin math var a end math

end ", it also extracts the `debugging information' of the principal operator of "

begin math var t end math

end " and installs that debugging information in all operators that come from the pattern "

begin math var p end math

end ". The debugging information indicates the exact location of the construct before macro expansion.

The "

begin math quote var t end quote end math

end " construct evaluates to the Logiweb representation of the term "

begin math var t end math

end ".



\subsection{The `Arbitrary' proof constructor}

The `Arbitrary' proof constructor defined on the \href{\lgwIjcarBaseUrl index.html}{base} page does not take advantage of the meta quantification macro above. For that reason we introduce a new construct for introducing arbitrary meta variables:

"

begin math define macro of any term var i end line var p 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 any term var i end line var p as for all terms var i indeed var p end define end quote end define end define end math

end "

Actually, the definition above was used as an example of a simple macro in Section \ref{section:Metaquantification}. When the same aspect of the same construct is defined more than once (e.g.\ the macro aspect of "

begin math all var i indeed var p end math

end "), only the first definition has effect. But the Logiweb compiler prints a warning if the same aspect of the same construct have definitions that contradict each other. The repeated definition of "

begin math all var i indeed var p end math

end " above gives no warnings since the two definitions have identical right hand sides.



\subsection{Macro indentation}

The following construct increases the left margin. Should be used in inline math mode only. Should be replaced by automatic indentation inside blocks as soon as possible.

"

begin math define macro of macro indent var x 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 macro indent var x as var x end define end quote end define end define end math

end "



\subsection{Protected macro expansion}

The following construct is a general macro definition construct which both protects its left hand side against macro expansion and renders its left hand side using the tex name aspect. To see the definitions of the tex and tex name aspects of "

begin math define macro of var x as var y end define hide end math

end " consult the \href{\lgwIjcarUrl body/tex/chores.pdf}{chores} part of the present Logiweb page.

"

begin math define macro of general macro define var x as var y end define 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 general macro define var x as var y end define as define macro of protect var x end protect as var y end define end define end quote end define end define end math

end "



\subsection{Object quantification}

The following is a repetion of Section \ref{section:Metaquantification} but concerns object quantification. It allows to write "

begin math for all objects var x indeed for all objects var y indeed for all objects var z indeed var u end math

end " for "

begin math for all objects var x indeed for all objects var y indeed for all objects var z indeed var u end math

end ".

\vspace{1ex}

\noindent "

begin math define macro of for all var x indeed var y as lambda var t dot lambda var s dot lambda var c dot state expand tagged if not var t first term root equal quote var x comma var y end quote then quote expand var t term quote for all objects var x indeed var y end quote stack quote var x end quote pair var t first pair quote var y end quote pair var t second pair true end expand else quote expand var t term quote for all objects var x indeed for all var y indeed var z end quote stack quote var x end quote pair var t first first pair quote var y end quote pair var t first second pair quote var z end quote pair var t second pair true end expand end if state var s cache var c end expand end define end math

end "



\subsection{Proof constructs}

The "

begin math var b cut var p end math

end " construct puts a parenthesis around the block "

begin math var b end math

end " and places a cut operator between "

begin math var b end math

end " and "

begin math var p end math

end ". The construct is complicated by the line number "

begin math var l end math

end " which should be macro defined locally to denote the conclusion of the block "

begin math var b end math

end ". This is non-trivial since the conclusion is the last line prefixed by all premises, side-conditions, and meta-quantifiers introduced in earlier lines.

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

\item "

begin math define macro of block var b line var l end block var p as lambda var t dot lambda var s dot lambda var c dot block one var t state var s cache var c end block end define end math

end "

\item "

begin math define value of block one var t state var s cache var c end block as var t tagged guard var s tagged guard var c tagged guard let one lambda var b dot let one lambda var x dot let one lambda var q dot let one lambda var q dot quote expand var t term quote var b cut var q end quote stack quote var b end quote pair var b pair quote var q end quote pair var q pair true end expand apply state expand var q state var s cache var c end expand end let apply quote expand var t term quote let var l abbreviate var x in var p end quote stack quote var l end quote pair var t second pair quote var p end quote pair var t third pair quote var x end quote pair var x pair true end expand end let apply block two var b end block end let apply state expand var t first state var s cache var c end expand end let end define end math

end "

\item "

begin math define value of block two var b end block as tagged if var b term root equal quote var x infer var y end quote then quote expand var b term quote var x infer var y end quote stack quote var x end quote pair var b first pair quote var y end quote pair block two var b second end block pair true end expand else tagged if var b term root equal quote var x endorse var y end quote then quote expand var b term quote var x endorse var y end quote stack quote var x end quote pair var b first pair quote var y end quote pair block two var b second end block pair true end expand else tagged if var b term root equal quote all var x indeed var y end quote then quote expand var b term quote all var x indeed var y end quote stack quote var x end quote pair var b first pair quote var y end quote pair block two var b second end block pair true end expand else tagged if var b term root equal quote var x cut var y end quote then block two var b second end block else tagged if var b term root equal quote var x conclude var y end quote then var b second else absurdity end if end if end if end if end if end define end math

end "

\item "

begin math define macro of because var a indeed var i end line 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 because var a indeed var i end line as parenthesis var a conclude var i end parenthesis end define end quote end define end define end math

end "

\end{list}



\subsection{Modus ponens at the object level}

We shall apply modus ponens to two arguments so often that this idiom deserves its own macro:

"

begin math define macro of var x object modus ponens 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 object modus ponens var y as rule mp modus ponens var x modus ponens var y end define end quote end define end define end math

end "



\section{Side conditions}

\subsection{Logiweb terms}\label{section:LogiwebTerms}

Metavariables, object terms, statements, and sequent terms are all implemented as Logiweb terms which essentially have the following syntax:

\newcommand{\literal}[1]{\mbox{``#1''}}
\[\begin{array}{lll}

pdigit & ::= & \literal{1} \mathrel{|} \literal{2} \mathrel{|} \literal{3} \mathrel{|} \literal{4} \mathrel{|} \literal{5} \mathrel{|} \literal{6} \mathrel{|} \literal{7} \mathrel{|} \literal{8} \mathrel{|} \literal{9} \\

digit & ::= & \literal{0} \mathrel{|} pdigit \\

positive & ::= & pdigit \mathrel{|} positive \ digit \\

cardinal & ::= & \literal{0} \mathrel{|} positive \\

reference & ::= & cardinal \\

identifier & ::= & cardinal \\

symbol & ::= & \literal{(} \ reference \literal{\mbox {\tt \char32 }} \ identifier \ \literal{)} \\

arglist & ::= & \literal{)} \mathrel{|} \literal{\mbox {\tt \char32 }} \ term \ arglist \\

term & ::= & \literal{(} \ symbol \ arglist \\

\end{array}\]

\noindent The only thing omitted from the syntax is a third element of symbols which contains debugging information. For details on debugging information, consult the \href{\lgwIjcarBaseUrl index.html}{base} page.

Each Logiweb page introduces one or more new constructs. As an example, the present page introduces the binary operation "

begin math var x imply var y end math

end ".

Each Logiweb page has a unique reference, and each construct introduced by a page has an identifier which is unique within the page. Hence, reference and identifier together determine a construct uniquely.



\subsection{Deduction}

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

\item "

begin math define macro of deduction var p conclude var c end deduction 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 deduction var p conclude var c end deduction as lambda var x dot deduction zero quote var p end quote conclude quote var c end quote end deduction end define end quote end define end define end math

end " \newline True if the premise "

begin math var p end math

end " implies the conclusion "

begin math var c end math

end " according to the deduction rule. The construct quotes its arguments and pass them on to "

begin math deduction zero var p conclude var c end deduction end math

end ". The quoting and the "

begin math lambda var x dot "\cdots" end math

end " makes "

begin math lambda var x dot deduction zero quote var p end quote conclude quote var c end quote end deduction end math

end " suited as a side condition. The present side condition ignores "

begin math var x end math

end ". But when a side condition is invoked, it is applied to the cache of the home page of the side condition (the page on which the side condition occurs). That way the side condition gets access to all definitions present on the home page and all pages transitively referenced by the home page. As an example, that has allowed to define an `axiom of definition' in another theory on another Logiweb page in which all value definitions automatically become axiom schemes. This possibility has been excluded from the present paper because of the Ijcar page limitation and because the facility is not particularly useful in Peano arithmetic. It is much more useful in theories that build on lambda calculus.

\item "

begin math define value of deduction zero var p conclude var c end deduction as var c tagged guard tagged if deduction eight var p bound true end deduction then deduction one deduction seven var p end deduction conclude var c condition true end deduction else false end if end define end math

end " \newline True if the premise "

begin math var p end math

end " implies the conclusion "

begin math var c end math

end " according to the deduction rule. The function checks the premise for meta-closedness, strips meta-quantifiers from "

begin math var p end math

end " and then calls "

begin math deduction one var p conclude var c condition var s end deduction end math

end " with an empty list "

begin math var s end math

end " of side conditions. The "

begin math var x tagged guard var y end math

end " construct evaluates and discards "

begin math var x end math

end " and then returns "

begin math var y end math

end ". It is included to ensure strictness of "

begin math deduction zero var p conclude var c end deduction end math

end " which in turn increases the efficiency. Some day the present author will define a `strict value definition' operator so that users don't have to add "

begin math var x tagged guard var y end math

end " operators manually. The "

begin math var x tagged guard var y end math

end " construct takes zero CPU-time when used in functions that are `fit' for optimization. See the \href{\lgwIjcarBaseUrl index.html}{base} page for details on `fitness' analysis.

\item "

begin math define value of deduction one var p conclude var c condition var s end deduction as tagged if var c term root equal quote var x endorse var y end quote then deduction one var p conclude var c second condition var c first pair var s end deduction else deduction two var p conclude var c condition var s end deduction end if end define end math

end " \newline Move side conditions from the conclusion "

begin math var c end math

end " to the list "

begin math var s end math

end ". "

begin math var x term root equal var y end math

end " is true if the terms "

begin math var x end math

end " and "

begin math var y end math

end " have the same root (i.e.\ the same principal operator) so "

begin math var c term root equal quote var x endorse var y end quote end math

end " is true if the principal operator of "

begin math var c end math

end " is an endorsement. "

begin math var c first end math

end " and "

begin math var c second end math

end " are the first and second argument, respectively, of the endorsement.

\item "

begin math define value of deduction two var p conclude var c condition var s end deduction as var s tagged guard var p term root equal quote var x infer var y end quote and var c term root equal quote var x imply var y end quote select deduction three var p first conclude var c first condition var s bound true end deduction and deduction two var p second conclude var c second condition var s end deduction else deduction four var p conclude var c condition var s bound deduction six var p conclude var c exception true bound true end deduction end deduction end select end define end math

end " \newline This function is true if the premise "

begin math var p end math

end " is equal to the conclusion "

begin math var c end math

end " except that inferences are replaced by implications. "

begin math tagged if var x then var y else var z end if end math

end " and "

begin math var x select var y else var z end select end math

end " express the same conditional construct. Choosing between the two is a purely stylistic choice.

\item "

begin math define value of deduction three var p conclude var c condition var s bound var b end deduction as tagged if not var c term root equal quote for all objects var x indeed var y end quote then deduction four var p conclude var c condition var s bound var b end deduction else tagged if var p term root equal quote for all objects var x indeed var y end quote and var p first term equal var c first then deduction four var p conclude var c condition var s bound var b end deduction else deduction three var p conclude var c second condition var s bound var c first pair var c first pair var b end deduction end if end if end define end math

end " \newline "

begin math deduction three var p conclude var c condition var s bound var b end deduction end math

end " moves quantified variables from the premise "

begin math var p end math

end " to the association list "

begin math var b end math

end " of `bindings'. Each quantified variable "

begin math var x end math

end " is added to "

begin math var b end math

end " as the pair "

begin math var x pair var x end math

end " indicating the "

begin math var x end math

end " should be replaced by "

begin math var x end math

end " (which is a way of saying that the variable cannot be instantiated). Moving of bound variables stops when there are no more bound variables to move or when the premise and conclusion happen to quantify the same variable. In both cases we have reached a point where premise and conclusion should be identical except for instantaition of variables. "

begin math var x term equal var y end math

end " is true if the terms "

begin math var x end math

end " and "

begin math var y end math

end " are identical. Logiweb terms contain debugging information which indicates the precise location each operator before macro expansion. "

begin math var x term equal var y end math

end " ignores this debugging information when it tests two terms for identity.

\item "

begin math define value of deduction four var p conclude var c condition var s bound var b end deduction as var s tagged guard var b tagged guard tagged if var p term root equal quote object var var x end var end quote then lookup var p stack var b default true end lookup term equal var c else tagged if not var p term root equal var c then false else tagged if var p term root equal quote for all objects var x indeed var y end quote then var p first term equal var c first and deduction four var p second conclude var c second condition var s bound var p first pair var p first pair var b end deduction else tagged if not var p term root equal quote metavar var x end metavar end quote then deduction four star var p tail conclude var c tail condition var s bound var b end deduction else var p first term equal var c first and deduction five var p condition var s bound var b end deduction end if end if end if end if end define end math

end " \newline Test that the premise "

begin math var p end math

end " is identical to the conclusion "

begin math var c end math

end " except for instantiation of object variables as specified by the association list "

begin math var b end math

end ". A term is an object variable if the root of the term is the `object variable operator'. For that reason, one can test whether or not a variable is an object variable by comparing its root to the root of an arbitrary object variable. For each meta variable, check that there are side conditions which ensure that the meta variables denote terms whose free object variables do not get caught in the context. Meta variables are recognized the same way as object variables. The object variable "

begin math object var var x end var end math

end " and the meta variable "

begin math metavar var x end metavar end math

end " macro expand into "

begin math object var var x end var end math

end " and "

begin math metavar var x end metavar end math

end ", respectively, adding the object and meta variable operator, respectively, to the term "

begin math var x end math

end ". The term "

begin math var x end math

end " is neither an object nor a meta variable. "

begin math var x end math

end " is a Logiweb programming language variable because no Logiweb definition assigns a value to it.

\item "

begin math define value of deduction four star var p conclude var c condition var s bound var b end deduction as var c tagged guard var s tagged guard var b tagged guard tagged if var p then true else deduction four var p head conclude var c head condition var s bound var b end deduction and deduction four star var p tail conclude var c tail condition var s bound var b end deduction end if end define end math

end " \newline Elementwise application of "

begin math deduction four var p conclude var c condition var s bound var b end deduction end math

end ". "

begin math var x head end math

end " and "

begin math var x tail end math

end " denote the head and tail, respectively, of the pair "

begin math var x end math

end ". Terms are represented as lists comprising the principal operator followed by arguments just like Lisp S-expressions. The principal operator in turn is a list whose first two elements are cardinals that identify the operator followed by debugging information.

\item "

begin math define value of deduction five var p condition var s bound var b end deduction as var p tagged guard var s tagged guard tagged if var b then true else quote quote var x end quote avoid zero quote var y end quote end quote head pair quote quote x end quote end quote head pair var b head head pair true pair quote quote var x end quote end quote head pair var p pair true pair true term in var s and deduction five var p condition var s bound var b tail end deduction end if end define end math

end " \newline For each variable that is bound in the context according to the association list "

begin math var b end math

end ", check that the list "

begin math var s end math

end " of side conditions ensures that the meta variables "

begin math var p end math

end " denotes a term whose free variables do not get caught in the context. "

begin math var x term in var y end math

end " is true if the term "

begin math var x end math

end " belongs to the list "

begin math var y end math

end " of terms.

\item "

begin math define value of deduction six var p conclude var c exception var e bound var b end deduction as var p tagged guard var c tagged guard var b tagged guard var e tagged guard tagged if var p term root equal quote object var var x end var end quote then var p term in var e select var b else var p pair var c pair var b end select else tagged if not var p term root equal var c then true else tagged if var p term root equal quote metavar var a end metavar end quote then var b else tagged if var p term root equal quote for all objects var x indeed var y end quote then deduction six var p second conclude var c second exception var c first pair var e bound var b end deduction else deduction six star var p tail conclude var c tail exception var e bound var b end deduction end if end if end if end if end define end math

end "

\item "

begin math define value of deduction six star var p conclude var c exception var e bound var b end deduction as var p tagged guard var c tagged guard var b tagged guard var e tagged guard tagged if var p then var b else deduction six star var p tail conclude var c tail exception var e bound deduction six var p head conclude var c head exception var e bound var b end deduction end deduction end if end define end math

end " \newline Elementwise application of "

begin math deduction six var p conclude var c exception var e bound var b end deduction end math

end ".

\item "

begin math define value of deduction seven var p end deduction as var p term root equal quote all var x indeed var y end quote select deduction seven var p second end deduction else var p end select end define end math

end " \newline Removal of all metaquantifiers.

\item "

begin math define value of deduction eight var p bound var b end deduction as tagged if var p term root equal quote all var x indeed var y end quote then deduction eight var p second bound var p first pair var b end deduction else tagged if var p term root equal quote metavar var a end metavar end quote then var p term in var b else deduction eight var p tail bound var b end deduction end if end if end define end math

end " \newline True if all free meta variables of "

begin math var p end math

end " occur in the list "

begin math var b end math

end " of meta variables.

\item "

begin math define value of deduction eight var p bound var b end deduction as var b tagged guard tagged if var p then true else tagged if deduction eight var p head bound var b end deduction then deduction eight var p tail bound var b end deduction else false end if end if end define end math

end " \newline Elementwise application of "

begin math deduction eight var p bound var b end deduction end math

end ".

\end{list}



\subsection{Avoidance}

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

\item "

begin math define value of var x is object var as var x term root equal quote object var var x end var end quote end define end math

end "

\item "

begin math define macro of var x avoid 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 avoid var y as quote var x end quote avoid zero quote var y end quote end define end quote end define end define end math

end "

\item "

begin math define value of var x avoid zero var y as lambda var c dot var x is object var and var y is metaclosed and var x avoid one var y end define end math

end "

\item "

begin math define value of var x avoid one var y as tagged if var y is object var then not var x term equal var y else newline tagged if not var y term root equal quote for all objects var x indeed var y end quote then var x avoid star var y tail else newline tagged if var x term equal var y first then true else var x avoid one var y second end if end if end if end define end math

end "

\item "

begin math define value of var x avoid star var y as var x tagged guard tagged if var y then true else tagged if var x avoid one var y head then var x avoid star var y tail else false end if end if end define end math

end "

\end{list}



\subsection{Substition}

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

\item "

begin math define macro of sub var a is var b where var x is var t end sub 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 sub var a is var b where var x is var t end sub as sub zero quote var a end quote is quote var b end quote where quote var x end quote is quote var t end quote end sub end define end quote end define end define end math

end "

\item "

begin math define value of sub zero var a is var b where var x is var t end sub as lambda var c dot var x is object var and sub one var a is var b where var x is var t end sub end define end math

end "

\item "

begin math define value of sub one var a is var b where var x is var t end sub as var a tagged guard var x tagged guard var t tagged guard newline tagged if tagged if var b term root equal quote for all objects var u indeed var v end quote then var b first term equal var x else false end if then var a term equal var b else newline tagged if var b is object var and var b term equal var x then var a term equal var t else tagged if newline var a term root equal var b then sub star var a tail is var b tail where var x is var t end sub else false end if end if end if end define end math

end "

\item "

begin math define value of sub star var a is var b where var x is var t end sub as var b tagged guard var x tagged guard var t tagged guard tagged if var a then true else tagged if sub one var a head is var b head where var x is var t end sub then sub star var a tail is var b tail where var x is var t end sub else false end if end if end define end math

end "

\end{list}



\section{Proofs}

\subsection{Proofs of FOL axioms using the inference of deduction}

We now prove axiom schemes A1 and A2 from \cite{mendelson}. Furthermore, we prove two, particular instances of A4 and A5 in a way that generalizes to arbitrary instances of those axiom schemes.

Furthermore, we prove a "

begin math repetition end math

end " lemma which says "

begin math all metavar var a end metavar indeed metavar var a end metavar infer metavar var a end metavar end math

end " by a `hand made proof', i.e.\ by giving a proof metatactic explicitly which generates the sequent proof.

A page is verified by a top level verifier. The top level verifier of the present page is defined on the \href{\lgwIjcarBaseUrl index.html}{base} page. That verifier invokes, among other, a proof verifier. The proof verifier invokes each proof (where each proof is supposed to be a proof metatactic). When it does so, it applies the proof metatactic to a Logiweb cache "

begin math var c end math

end " and a pair "

begin math var n pair var l end math

end ". The cache "

begin math var c end math

end " is the Logiweb cache of the home page of the proof, i.e.\ a structure which contains all definitions present on the home page plus all transitively referenced Logiweb pages. "

begin math var n end math

end " is the identifier of the lemma (a cardinal which identifies the lemma uniquely within the home page) plus the contents of the lemma. The proof metatactic given below for proving "

begin math repetition end math

end " ignores both arguments and just constructs a sequent term that proves "

begin math all metavar var a end metavar indeed metavar var a end metavar infer metavar var a end metavar end math

end ". All other proofs in the present paper macro expand into proofs that are proved by a metatactic which scans the proof for object tactics and invokes those object tactics. The only object tactic used is named $\gg$ and does unification.

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}}

\item "

begin math define statement of repetition as system s infer all metavar var a end metavar indeed metavar var a end metavar infer metavar var a end metavar end define end math

end "

\item "

begin math define statement of lemma 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 imply metavar var b end metavar imply metavar var a end metavar end define end math

end "

\item "

begin math define statement of lemma 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 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 end define end math

end "

\item "

begin math define statement of lemma a four as system s infer for all objects object var var x end var indeed for all objects object var var y end var indeed object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var imply two plus three equal three plus two end define end math

end "

\item "

begin math define statement of lemma a five as system s infer for all objects object var var x end var indeed two plus three equal five imply two plus three plus object var var x end var equal five plus object var var x end var imply two plus three equal five imply for all objects object var var x end var indeed two plus three plus object var var x end var equal five plus object var var x end var end define end math

end "

\end{list}

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

\item "

begin math define proof of repetition as lambda var c dot lambda var x dot quote system s infer all metavar var a end metavar indeed metavar var a end metavar init end quote end define end math

end "

\item "

begin math define proof of lemma 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 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 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 all metavar var b end metavar indeed metavar var a end metavar infer metavar var b end metavar infer metavar var a end metavar conclude metavar var a end metavar imply metavar var b end metavar imply metavar var a end metavar end quote state proof state cache var c end expand end define end math

end "

\item "

begin math define proof of lemma 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 imply metavar var b end metavar imply metavar var c end metavar infer metavar var a end metavar imply metavar var b 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 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 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 imply metavar var c end metavar infer metavar var a end metavar imply metavar var b 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 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 end quote state proof state cache var c end expand end define end math

end "

\item "

begin math define proof of lemma a four as lambda var c dot lambda var x dot proof expand quote system s infer object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var infer repetition modus ponens object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var conclude object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var cut deduction modus ponens object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var infer object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var conclude for all objects object var var x end var indeed for all objects object var var y end var indeed object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var imply two plus three equal three plus two end quote state proof state cache var c end expand end define end math

end "

\item "

begin math define proof of lemma a five as lambda var c dot lambda var x dot proof expand quote system s infer two plus three equal five imply two plus three plus object var var x end var equal five plus object var var x end var infer two plus three equal five infer rule mp modus ponens two plus three equal five imply two plus three plus object var var x end var equal five plus object var var x end var modus ponens two plus three equal five conclude two plus three plus object var var x end var equal five plus object var var x end var cut rule gen modus ponens two plus three plus object var var x end var equal five plus object var var x end var conclude for all objects object var var x end var indeed two plus three plus object var var x end var equal five plus object var var x end var cut deduction modus ponens two plus three equal five imply two plus three plus object var var x end var equal five plus object var var x end var infer two plus three equal five infer for all objects object var var x end var indeed two plus three plus object var var x end var equal five plus object var var x end var conclude for all objects object var var x end var indeed two plus three equal five imply two plus three plus object var var x end var equal five plus object var var x end var imply two plus three equal five imply for all objects object var var x end var indeed two plus three plus object var var x end var equal five plus object var var x end var end quote state proof state cache var c end expand end define end math

end "

\end{list}



\subsection{A proof of "

begin math var x plus var y equal var y plus var x end math

end "}

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

\item "

begin 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

end "

\item "

begin 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

end "

\item "

begin 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

end "

\item "

begin 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

end "

\item "

begin 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

end "

\item "

begin 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

end "

\item "

begin 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

end "

\item "

begin 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 "

\end{list}



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

\item "

begin math define proof of prop three two 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 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 metavar var a end metavar conclude metavar var a end metavar equal metavar var a end metavar end quote state proof state cache var c end expand end define end math

end "



\item "

begin math define proof of prop three two 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 metavar var a end metavar equal metavar var b end metavar infer prop three two a conclude metavar var a end metavar equal metavar var a end metavar cut 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 a end metavar conclude 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

end "



\item "

begin math define proof of prop three two 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 metavar var a end metavar equal metavar var b end metavar infer metavar var b end metavar equal metavar var c 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 axiom s one modus ponens metavar var b end metavar equal metavar var a 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 end quote state proof state cache var c end expand end define end math

end "



\item "

begin math define proof of prop three two 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 metavar var a end metavar equal metavar var c end metavar infer metavar var b end metavar equal metavar var c end metavar infer prop three two b modus ponens metavar var b end metavar equal metavar var c end metavar conclude metavar var c end metavar equal metavar var b end metavar cut prop three two c modus ponens metavar var a end metavar equal metavar var c end metavar modus ponens metavar var c end metavar equal metavar var b end metavar conclude 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 "



\item "

begin math define statement of prop three two e 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 plus zero equal metavar var b end metavar plus zero end define end math

end "



\item "

begin math define proof of prop three two 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 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 five conclude metavar var a end metavar plus zero equal metavar var a end metavar cut prop three two c modus ponens metavar var a end metavar plus zero equal metavar var a end metavar modus ponens 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 cut axiom s five conclude metavar var b end metavar plus zero equal metavar var b end metavar cut prop three two d modus ponens metavar var a end metavar plus zero equal metavar var b end metavar modus ponens metavar var b end metavar plus zero equal metavar var b end metavar conclude metavar var a end metavar plus zero equal metavar var b end metavar plus 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 plus zero equal metavar var b end metavar plus zero conclude metavar var a end metavar equal metavar var b end metavar imply metavar var a end metavar plus zero equal metavar var b end metavar plus zero end quote state proof state cache var c end expand end define end math

end "



\item "

begin math define statement of prop three two e 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 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 end define end math

end "



\item "

begin math define proof of prop three two 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 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 plus metavar var c end metavar equal metavar var b end metavar plus 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 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 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 axiom s two 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 plus metavar var c end metavar suc equal 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 c end metavar suc equal metavar var a 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 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 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 d 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 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 plus metavar var c end metavar equal metavar var b end metavar plus metavar var c end metavar infer 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 conclude metavar var a end metavar equal metavar var b 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 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 end quote state proof state cache var c end expand end define end math

end "



\item "

begin math define proof of prop three two 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 all metavar var c end metavar indeed metavar var a end metavar equal metavar var b end metavar infer prop three two e one conclude object var var x end var equal object var var y end var imply object var var x end var plus zero equal object var var y end var plus zero cut prop three two e two conclude 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 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 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 plus zero equal object var var y end var plus zero modus ponens 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 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 conclude 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 equal object var var y end var plus 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 plus object var var z end var equal object var var y end var plus object var var z end var conclude metavar var a end metavar equal metavar var b 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 cut rule mp modus ponens metavar var a end metavar equal metavar var b 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 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 end quote state proof state cache var c end expand end define end math

end "



\item "

begin math define statement of prop three two f one as system s infer zero equal zero plus zero end define end math

end "



\item "

begin math define proof of prop three two f one as lambda var c dot lambda var x dot proof expand quote system s infer axiom s five conclude zero plus zero equal zero cut prop three two b modus ponens zero plus zero equal zero conclude zero equal zero plus zero end quote state proof state cache var c end expand end define end math

end "



\item "

begin math define statement of prop three two f two as system s infer all metavar var a end metavar indeed metavar var a end metavar equal zero plus metavar var a end metavar imply metavar var a end metavar suc equal zero plus metavar var a end metavar suc end define end math

end "



\item "

begin math define proof of prop three two 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 a end metavar indeed metavar var a end metavar equal zero plus metavar var a end metavar infer axiom s two modus ponens metavar var a end metavar equal zero plus metavar var a end metavar conclude metavar var a end metavar suc equal zero plus metavar var a end metavar suc cut axiom s six conclude zero plus metavar var a end metavar suc equal zero plus metavar var a end metavar suc cut prop three two d modus ponens metavar var a end metavar suc equal zero plus metavar var a end metavar suc modus ponens zero plus metavar var a end metavar suc equal zero plus metavar var a end metavar suc conclude metavar var a end metavar suc equal zero plus metavar var a end metavar suc cut deduction modus ponens all metavar var a end metavar indeed metavar var a end metavar equal zero plus metavar var a end metavar infer metavar var a end metavar suc equal zero plus metavar var a end metavar suc conclude metavar var a end metavar equal zero plus metavar var a end metavar imply metavar var a end metavar suc equal zero plus metavar var a end metavar suc end quote state proof state cache var c end expand end define end math

end "



\item "

begin math define proof of prop three two f as lambda var c dot lambda var x dot proof expand quote system s infer all metavar var a end metavar indeed prop three two f one conclude zero equal zero plus zero cut prop three two f two conclude object var var x end var equal zero plus object var var x end var imply object var var x end var suc equal zero plus object var var x end var suc cut axiom s nine at object var var x end var modus ponens zero equal zero plus zero modus ponens object var var x end var equal zero plus object var var x end var imply object var var x end var suc equal zero plus object var var x end var suc conclude object var var x end var equal zero plus object var var x end var cut deduction modus ponens object var var x end var equal zero plus object var var x end var conclude metavar var a end metavar equal zero plus metavar var a end metavar end quote state proof state cache var c end expand end define end math

end "



\item "

begin math define statement of prop three two g one as system s infer all metavar var a end metavar indeed metavar var a end metavar suc plus zero equal metavar var a end metavar plus zero suc end define end math

end "



\item "

begin math define proof of prop three two g 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 five conclude metavar var a end metavar suc plus zero equal metavar var a end metavar 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 d modus ponens metavar var a end metavar suc plus zero equal metavar var a end metavar suc modus ponens metavar var a end metavar plus zero suc equal metavar var a end metavar suc conclude metavar var a end metavar suc plus zero equal metavar var a end metavar plus zero suc end quote state proof state cache var c end expand end define end math

end "



\item "

begin math define statement of prop three two 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 suc plus metavar var b end metavar equal metavar var a end metavar plus metavar var b end metavar suc imply metavar var a end metavar suc plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc suc end define end math

end "



\item "

begin math define proof of prop three two 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 suc plus metavar var b end metavar equal metavar var a end metavar plus metavar var b end metavar suc infer axiom s two modus ponens 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 conclude metavar var a end metavar suc plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc suc cut axiom s six conclude metavar var a end metavar suc plus metavar var b end metavar suc equal metavar var a end metavar suc plus metavar var b end metavar suc cut prop three two c modus ponens metavar var a end metavar suc plus metavar var b end metavar suc equal metavar var a end metavar suc plus metavar var b end metavar suc modus ponens metavar var a end metavar suc plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc suc conclude metavar var a end metavar suc plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc suc 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 axiom s two 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 conclude metavar var a end metavar plus metavar var b end metavar suc suc equal metavar var a end metavar plus metavar var b end metavar suc suc cut prop three two d modus ponens metavar var a end metavar suc plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc suc modus ponens metavar var a end metavar plus metavar var b end metavar suc suc equal metavar var a end metavar plus metavar var b end metavar suc suc conclude metavar var a end metavar suc plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc 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 plus metavar var b end metavar equal metavar var a end metavar plus metavar var b end metavar suc infer metavar var a end metavar suc plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc suc conclude 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 imply metavar var a end metavar suc plus metavar var b end metavar suc equal metavar var a end metavar plus metavar var b end metavar suc suc end quote state proof state cache var c end expand end define end math

end "



\item "

begin math define proof of prop three two 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 two g one conclude object var var x end var suc plus zero equal object var var x end var plus zero suc cut prop three two g two conclude object var var x end var suc plus object var var y end var equal object var var x end var plus object var var y end var suc imply object var var x end var suc plus object var var y end var suc equal object var var x end var plus object var var y end var suc suc cut axiom s nine at object var var y end var modus ponens object var var x end var suc plus zero equal object var var x end var plus zero suc modus ponens object var var x end var suc plus object var var y end var equal object var var x end var plus object var var y end var suc imply object var var x end var suc plus object var var y end var suc equal object var var x end var plus object var var y end var suc suc conclude object var var x end var suc plus object var var y end var equal object var var x end var plus object var var y end var suc cut deduction modus ponens object var var x end var suc plus object var var y end var equal object var var x end var plus object var var y end var suc conclude 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 quote state proof state cache var c end expand end define end math

end "



\item "

begin math define statement of prop three two h one as system s infer all metavar var a end metavar indeed metavar var a end metavar plus zero equal zero plus metavar var a end metavar end define end math

end "



\item "

begin math define proof of prop three two h 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 five conclude metavar var a end metavar plus zero equal 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 c modus ponens metavar var a end metavar plus zero equal metavar var a end metavar modus ponens metavar var a end metavar equal zero plus metavar var a end metavar conclude metavar var a end metavar plus zero equal zero plus metavar var a end metavar end quote state proof state cache var c end expand end define end math

end "



\item "

begin math define statement of prop three two h 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 metavar var b end metavar plus metavar var a end metavar imply metavar var a end metavar plus metavar var b end metavar suc equal metavar var b end metavar suc plus metavar var a end metavar end define end math

end "



\item "

begin math define proof of prop three two h 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 metavar var b end metavar plus metavar var a end metavar infer axiom s two modus ponens metavar var a end metavar plus metavar var b end metavar equal metavar var b end metavar plus metavar var a end metavar conclude metavar var a end metavar plus metavar var b end metavar suc equal metavar var b end metavar plus metavar var a end metavar suc 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 prop three two c 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 metavar var b end metavar plus metavar var a end metavar suc conclude metavar var a end metavar plus metavar var b 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 a end metavar plus metavar var b 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 a end metavar plus metavar var b end metavar suc equal metavar var b end metavar suc plus 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 plus metavar var b end metavar equal metavar var b end metavar plus metavar var a end metavar infer metavar var a end metavar plus metavar var b end metavar suc equal metavar var b end metavar suc plus metavar var a end metavar conclude metavar var a end metavar plus metavar var b end metavar equal metavar var b end metavar plus metavar var a end metavar imply metavar var a end metavar plus metavar var b end metavar suc equal metavar var b end metavar suc plus metavar var a end metavar end quote state proof state cache var c end expand end define end math

end "



\item "

begin math define proof of prop three two h 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 h one conclude object var var x end var plus zero equal zero plus object var var x end var cut prop three two h two conclude object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var imply object var var x end var plus object var var y end var suc equal object var var y end var suc plus 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 plus zero equal zero plus object var var x end var modus ponens object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var imply object var var x end var plus object var var y end var suc equal object var var y end var suc plus object var var x end var conclude object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var cut deduction modus ponens object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var conclude metavar var a end metavar plus metavar var b end metavar equal metavar var b end metavar plus metavar var a end metavar end quote state proof state cache var c end expand end define end math

end "

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

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

\item "

begin math test quote object var var x end var end quote avoid zero quote object var var y end var equal object var var z end var imply for all objects object var var x end var indeed object var var x end var equal object var var y end var end quote apply ijcar end test end math

end "

\item "

begin math false test quote object var var x end var end quote avoid zero quote object var var x end var equal object var var z end var imply for all objects object var var x end var indeed object var var x end var equal object var var y end var end quote apply ijcar end test end math

end "

\item "

begin math false test quote object var var x end var end quote avoid zero quote object var var y end var equal object var var x end var imply for all objects object var var x end var indeed object var var x end var equal object var var y end var end quote apply ijcar end test end math

end "

\item "

begin math false test quote object var var x end var end quote avoid zero quote object var var y end var equal object var var z end var imply for all objects object var var y end var indeed object var var x end var equal object var var y end var end quote apply ijcar end test end math

end "

\item "

begin math test sub zero quote object var var a end var end quote is quote object var var a end var end quote where quote object var var b end var end quote is quote object var var c end var end quote end sub apply ijcar end test end math

end "

\item "

begin math false test sub zero quote object var var b end var end quote is quote object var var a end var end quote where quote object var var b end var end quote is quote object var var c end var end quote end sub apply ijcar end test end math

end "

\item "

begin math false test sub zero quote object var var c end var end quote is quote object var var a end var end quote where quote object var var b end var end quote is quote object var var c end var end quote end sub apply ijcar end test end math

end "

\item "

begin math false test sub zero quote object var var a end var end quote is quote object var var b end var end quote where quote object var var b end var end quote is quote object var var c end var end quote end sub apply ijcar end test end math

end "

\item "

begin math false test sub zero quote object var var b end var end quote is quote object var var b end var end quote where quote object var var b end var end quote is quote object var var c end var end quote end sub apply ijcar end test end math

end "

\item "

begin math test sub zero quote object var var c end var end quote is quote object var var b end var end quote where quote object var var b end var end quote is quote object var var c end var end quote end sub apply ijcar end test end math

end "

\item "

begin math test sub zero quote for all objects object var var a end var indeed object var var a end var equal object var var b end var end quote is quote for all objects object var var a end var indeed object var var a end var equal object var var b end var end quote where quote object var var a end var end quote is quote object var var c end var end quote end sub apply ijcar end test end math

end "

\item "

begin math test sub zero quote for all objects object var var a end var indeed object var var a end var equal object var var c end var end quote is quote for all objects object var var a end var indeed object var var a end var equal object var var b end var end quote where quote object var var b end var end quote is quote object var var c end var end quote end sub apply ijcar end test end math

end "

\item "

begin math test sub zero quote for all objects object var var a end var indeed object var var a end var equal zero plus object var var a end var imply object var var c end var times object var var d end var equal zero plus object var var c end var times object var var d end var end quote is quote for all objects object var var a end var indeed object var var a end var equal zero plus object var var a end var imply object var var b end var equal zero plus object var var b end var end quote where quote object var var b end var end quote is quote object var var c end var times object var var d end var end quote end sub apply ijcar end test end math

end "

\item "

begin math test sub zero quote for all objects object var var a end var indeed object var var a end var equal zero plus object var var a end var imply object var var b end var equal zero plus object var var b end var end quote is quote for all objects object var var a end var indeed object var var a end var equal zero plus object var var a end var imply object var var b end var equal zero plus object var var b end var end quote where quote object var var a end var end quote is quote object var var c end var end quote end sub apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote zero end quote conclude quote zero end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote zero end quote conclude quote one end quote end deduction apply ijcar end test end math

end "

\item "

begin math test deduction eight quote all metavar var a end metavar indeed metavar var a end metavar end quote bound true end deduction end test end math

end "

\item "

begin math test deduction seven quote all metavar var a end metavar indeed metavar var a end metavar end quote end deduction term equal quote metavar var a end metavar end quote end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote all metavar var a end metavar indeed metavar var a end metavar end quote conclude quote metavar var a end metavar end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test 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 apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote all metavar var a end metavar indeed metavar var a end metavar end quote conclude quote metavar var b end metavar end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote 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 end quote conclude quote metavar var a end metavar imply metavar var b end metavar end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote 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 end quote conclude quote metavar var a end metavar imply metavar var a end metavar end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote 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 end quote conclude quote metavar var b end metavar imply metavar var b end metavar end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote 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 end quote conclude quote zero end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote zero end quote conclude quote metavar var a end metavar imply metavar var a end metavar end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote 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 infer metavar var b end metavar infer metavar var c end metavar end quote conclude quote metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote 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 metavar var a end metavar end quote conclude quote metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote 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 infer metavar var b end metavar infer metavar var c end metavar end quote conclude quote metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote zero end quote conclude quote object var var x end var end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote object var var x end var end quote conclude quote zero end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote object var var x end var end quote conclude quote object var var x end var end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote for all objects object var var x end var indeed object var var x end var end quote conclude quote object var var x end var end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote object var var x end var end quote conclude quote for all objects object var var y end var indeed object var var z end var end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote for all objects object var var x end var indeed object var var x end var end quote conclude quote for all objects object var var x end var indeed object var var x end var end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote zero infer zero end quote conclude quote zero imply zero end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote object var var x end var infer zero end quote conclude quote zero imply zero end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote zero infer object var var x end var end quote conclude quote zero imply zero end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote object var var x end var infer object var var x end var end quote conclude quote zero imply zero end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote zero infer zero end quote conclude quote for all objects object var var x end var indeed zero imply zero end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote object var var x end var infer zero end quote conclude quote for all objects object var var x end var indeed object var var x end var imply zero end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote zero infer object var var x end var end quote conclude quote for all objects object var var x end var indeed zero imply object var var x end var end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote object var var x end var infer object var var x end var end quote conclude quote for all objects object var var x end var indeed object var var x end var imply object var var x end var end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote zero infer zero end quote conclude quote zero imply for all objects object var var x end var indeed zero end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote object var var x end var infer zero end quote conclude quote zero imply for all objects object var var x end var indeed zero end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote zero infer object var var x end var end quote conclude quote zero imply for all objects object var var y end var indeed object var var z end var end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote object var var x end var infer object var var x end var end quote conclude quote zero imply for all objects object var var x end var indeed object var var x end var end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote zero infer zero end quote conclude quote for all objects object var var x end var indeed zero imply for all objects object var var x end var indeed zero end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote object var var x end var infer zero end quote conclude quote for all objects object var var x end var indeed object var var x end var imply for all objects object var var x end var indeed zero end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote zero infer object var var x end var end quote conclude quote for all objects object var var x end var indeed zero imply two end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote object var var x end var infer object var var x end var end quote conclude quote for all objects object var var x end var indeed object var var x end var imply three end quote end deduction apply ijcar end test end math

end "

\item "

begin math test lambda var x dot deduction zero quote object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var end quote conclude quote two plus three equal three plus two end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var end quote conclude quote two plus three equal two plus three end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var end quote conclude quote two plus three equal two plus two end quote end deduction apply ijcar end test end math

end "

\item "

begin math false test lambda var x dot deduction zero quote object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var end quote conclude quote two plus three equal three plus three end quote end deduction apply ijcar end test end math

end "

\end{list}



\section{Pyk definitions}

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

\item "

begin math define pyk of general macro define var x as var y end define as text "general macro define * as * end define" end text end define end math

end "

\item "

begin math define pyk of make root visible var x end visible as text "make root visible * end visible" end text end define end math

end "

\item "

begin math define pyk of ijcar as text "ijcar" end text end define end math

end "

\item "

begin math define pyk of var x hide as text "* hide" end text end define end math

end "

\item "

begin math define pyk of var x suc as text "* suc" end text end define end math

end "

\item "

begin math define pyk of var x equal var y as text "* equal *" end text end define end math

end "

\item "

begin math define pyk of var x unequal var y as text "* unequal *" end text end define end math

end "

\item "

begin math define pyk of var x imply var y as text "* imply *" end text end define end math

end "

\item "

begin math define pyk of var x if and only if var y as text "* if and only if *" end text end define end math

end "

\item "

begin math define pyk of var x alternative var y as text "* alternative *" end text end define end math

end "

\item "

begin math define pyk of exist var x indeed var y as text "exist * indeed *" end text end define end math

end "

\item "

begin math define pyk of for all var x indeed var y as text "for all * indeed *" end text end define end math

end "

\item "

begin math define pyk of for all objects var x indeed var y as text "for all objects * indeed *" end text end define end math

end "

\item "

begin math define pyk of for all terms var x indeed var y as text "for all terms * indeed *" end text end define end math

end "

\item "

begin math define pyk of any term var i end line var p as text "any term * end line *" end text end define end math

end "

\item "

begin math define pyk of var x safe row var y as text "* safe row *" end text end define end math

end "

\item "

begin math define pyk of ijcar example axiom as text "ijcar example axiom" end text end define end math

end "

\item "

begin math define pyk of ijcar example rule as text "ijcar example rule" end text end define end math

end "

\item "

begin math define pyk of ijcar example contradiction as text "ijcar example contradiction" end text end define end math

end "

\item "

begin math define pyk of ijcar example theory as text "ijcar example theory" end text end define end math

end "

\item "

begin math define pyk of ijcar example lemma as text "ijcar example lemma" end text end define end math

end "

\item "

begin math define pyk of set var x end set as text "set * end set" end text end define end math

end "

\item "

begin math define pyk of system s as text "system s" end text end define end math

end "

\item "

begin math define pyk of double negation as text "double negation" end text end define end math

end "

\item "

begin math define pyk of axiom s one as text "axiom s one" end text end define end math

end "

\item "

begin math define pyk of axiom s two as text "axiom s two" end text end define end math

end "

\item "

begin math define pyk of axiom s three as text "axiom s three" end text end define end math

end "

\item "

begin math define pyk of axiom s four as text "axiom s four" end text end define end math

end "

\item "

begin math define pyk of axiom s five as text "axiom s five" end text end define end math

end "

\item "

begin math define pyk of axiom s six as text "axiom s six" end text end define end math

end "

\item "

begin math define pyk of axiom s seven as text "axiom s seven" end text end define end math

end "

\item "

begin math define pyk of axiom s eight as text "axiom s eight" end text end define end math

end "

\item "

begin math define pyk of axiom s nine as text "axiom s nine" end text end define end math

end "

\item "

begin math define pyk of rule mp as text "rule mp" end text end define end math

end "

\item "

begin math define pyk of rule gen as text "rule gen" end text end define end math

end "

\item "

begin math define pyk of deduction as text "deduction" end text end define end math

end "

\item "

begin math define pyk of repetition as text "repetition" end text end define end math

end "

\item "

begin math define pyk of lemma a one as text "lemma a one" end text end define end math

end "

\item "

begin math define pyk of lemma a two as text "lemma a two" end text end define end math

end "

\item "

begin math define pyk of lemma a four as text "lemma a four" end text end define end math

end "

\item "

begin math define pyk of lemma a five as text "lemma a five" end text end define end math

end "

\item "

begin math define pyk of var x is object var as text "* is object var" end text end define end math

end "

\item "

begin math define pyk of var x avoid var y as text "* avoid *" end text end define end math

end "

\item "

begin math define pyk of var x avoid zero var y as text "* avoid zero *" end text end define end math

end "

\item "

begin math define pyk of var x avoid one var y as text "* avoid one *" end text end define end math

end "

\item "

begin math define pyk of var x avoid star var y as text "* avoid star *" end text end define end math

end "

\item "

begin math define pyk of sub var x is var y where var z is var u end sub as text "sub * is * where * is * end sub" end text end define end math

end "

\item "

begin math define pyk of sub zero var x is var y where var z is var u end sub as text "sub zero * is * where * is * end sub" end text end define end math

end "

\item "

begin math define pyk of sub one var x is var y where var z is var u end sub as text "sub one * is * where * is * end sub" end text end define end math

end "

\item "

begin math define pyk of sub star var x is var y where var z is var u end sub as text "sub star * is * where * is * end sub" end text end define end math

end "

\item "

begin math define pyk of deduction var x conclude var y end deduction as text "deduction * conclude * end deduction" end text end define end math

end "

\item "

begin math define pyk of deduction zero var x conclude var y end deduction as text "deduction zero * conclude * end deduction" end text end define end math

end "

\item "

begin math define pyk of deduction one var x conclude var y condition var z end deduction as text "deduction one * conclude * condition * end deduction" end text end define end math

end "

\item "

begin math define pyk of deduction two var x conclude var y condition var z end deduction as text "deduction two * conclude * condition * end deduction" end text end define end math

end "

\item "

begin math define pyk of deduction three var x conclude var y condition var z bound var u end deduction as text "deduction three * conclude * condition * bound * end deduction" end text end define end math

end "

\item "

begin math define pyk of deduction four var x conclude var y condition var z bound var u end deduction as text "deduction four * conclude * condition * bound * end deduction" end text end define end math

end "

\item "

begin math define pyk of deduction four star var x conclude var y condition var z bound var u end deduction as text "deduction four star * conclude * condition * bound * end deduction" end text end define end math

end "

\item "

begin math define pyk of deduction five var x condition var y bound var z end deduction as text "deduction five * condition * bound * end deduction" end text end define end math

end "

\item "

begin math define pyk of deduction six var p conclude var c exception var e bound var b end deduction as text "deduction six * conclude * exception * bound * end deduction" end text end define end math

end "

\item "

begin math define pyk of deduction six star var p conclude var c exception var e bound var b end deduction as text "deduction six star * conclude * exception * bound * end deduction" end text end define end math

end "

\item "

begin math define pyk of deduction seven var p end deduction as text "deduction seven * end deduction" end text end define end math

end "

\item "

begin math define pyk of deduction eight var p bound var b end deduction as text "deduction eight * bound * end deduction" end text end define end math

end "

\item "

begin math define pyk of deduction eight var p bound var b end deduction as text "deduction eight * bound * end deduction" end text end define end math

end "

\item "

begin math define pyk of block var b line var l end block var p as text "block * line * end block *" end text end define end math

end "

\item "

begin math define pyk of because var l indeed var i end line as text "because * indeed * end line" end text end define end math

end "

\item "

begin math define pyk of var x object modus ponens var y as text "* object modus ponens *" end text end define end math

end "

\item "

begin math define pyk of prop three two a as text "prop three two a" end text end define end math

end "

\item "

begin math define pyk of prop three two b as text "prop three two b" end text end define end math

end "

\item "

begin math define pyk of prop three two c as text "prop three two c" end text end define end math

end "

\item "

begin math define pyk of prop three two d as text "prop three two d" end text end define end math

end "

\item "

begin math define pyk of prop three two e one as text "prop three two e one" end text end define end math

end "

\item "

begin math define pyk of prop three two e two as text "prop three two e two" end text end define end math

end "

\item "

begin math define pyk of prop three two e as text "prop three two e" end text end define end math

end "

\item "

begin math define pyk of prop three two f one as text "prop three two f one" end text end define end math

end "

\item "

begin math define pyk of prop three two f two as text "prop three two f two" end text end define end math

end "

\item "

begin math define pyk of prop three two f as text "prop three two f" end text end define end math

end "

\item "

begin math define pyk of prop three two g one as text "prop three two g one" end text end define end math

end "

\item "

begin math define pyk of prop three two g two as text "prop three two g two" end text end define end math

end "

\item "

begin math define pyk of prop three two g as text "prop three two g" end text end define end math

end "

\item "

begin math define pyk of prop three two h one as text "prop three two h one" end text end define end math

end "

\item "

begin math define pyk of prop three two h two as text "prop three two h two" end text end define end math

end "

\item "

begin math define pyk of prop three two h as text "prop three two h" end text end define end math

end "

\item "

begin math define pyk of macro indent var x as text "macro indent *" end text end define end math

end "

\item "

begin math define pyk of block one var t state var s cache var c end block as text "block one * state * cache * end block" end text end define end math

end "

\item "

begin math define pyk of block two var b end block as text "block two * end block" end text end define end math

end "

\item "

begin math define pyk of evaluates to as text "evaluates to" end text end define end math

end "

\end{list}



\section{\TeX\ definitions}

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

\item "

begin math define tex of general macro define var x as var y end define as text "
[#1/tex name/tex.
\stackrel {\circ}{=}#2.
]" end text end define end math

end "

\item "

begin math define tex of make root visible var x end visible as text "#1/tex name/tex." end text end define end math

end "

\item "

begin math define tex name of make root visible var x end visible as text "
RootVisible(#1.
)" end text end define end math

end "

\item "

begin math define tex of var x hide as text "#1.
{}^{hide}" end text end define end math

end "

\item "

begin math define tex of var x suc as text "#1.
{}'" end text end define end math

end "

\item "

begin math define tex of var x equal var y as text "#1.
= #2." end text end define end math

end "

\item "

begin math define tex of var x unequal var y as text "#1.
\neq #2." end text end define end math

end "

\item "

begin math define tex of var x imply var y as text "#1.
\Rightarrow #2." end text end define end math

end "

\item "

begin math define tex of var x if and only if var y as text "#1.
\Leftrightarrow #2." end text end define end math

end "

\item "

begin math define tex of var x alternative var y as text "#1.
\mathrel{|} #2." end text end define end math

end "

\item "

begin math define tex of exist var x indeed var y as text "
\exists #1.
\colon #2." end text end define end math

end "

\item "

begin math define tex of for all var x indeed var y as text "
\forall #1.
\colon #2." end text end define end math

end "

\item "

begin math define tex of for all objects var x indeed var y as text "
\forall_{obj} #1.
\colon #2." end text end define end math

end "

\item "

begin math define tex of for all terms var x indeed var y as text "
\Pi #1.
\colon #2." end text end define end math

end "

\item "

begin math define tex of any term var i end line var p as text "
\newline \makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi
$:}\makebox [0.4\textwidth ][l]{$Arbitrary{}\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$#1.
$\hfill \makebox [0mm][l]{\quad ;}}#2." end text end define end math

end "

\item "

begin math define tex name of any term var i end line var p as text "
Arbitrary \gg #1.
;#2." end text end define end math

end "

\item "

begin math define tex of var x safe row var y as text "#1.
\\{}#2." end text end define end math

end "

\item "

begin math define tex name of var x safe row var y as text "#1.
\backslash \backslash #2." end text end define end math

end "

\item "

begin math define tex of ijcar example axiom as text "
A" end text end define end math

end "

\item "

begin math define tex of ijcar example rule as text "
R" end text end define end math

end "

\item "

begin math define tex of ijcar example contradiction as text "
C" end text end define end math

end "

\item "

begin math define tex of ijcar example theory as text "
T" end text end define end math

end "

\item "

begin math define tex of ijcar example lemma as text "
L" end text end define end math

end "

\item "

begin math define tex of set var x end set as text "
\{#1.
\}" end text end define end math

end "

\item "

begin math define tex of system s as text "
S" end text end define end math

end "

\item "

begin math define tex of double negation as text "
Neg" end text end define end math

end "

\item "

begin math define tex of axiom s one as text "
S1" end text end define end math

end "

\item "

begin math define tex of axiom s two as text "
S2" end text end define end math

end "

\item "

begin math define tex of axiom s three as text "
S3" end text end define end math

end "

\item "

begin math define tex of axiom s four as text "
S4" end text end define end math

end "

\item "

begin math define tex of axiom s five as text "
S5" end text end define end math

end "

\item "

begin math define tex of axiom s six as text "
S6" end text end define end math

end "

\item "

begin math define tex of axiom s seven as text "
S7" end text end define end math

end "

\item "

begin math define tex of axiom s eight as text "
S8" end text end define end math

end "

\item "

begin math define tex of axiom s nine as text "
S9" end text end define end math

end "

\item "

begin math define tex of rule mp as text "
MP" end text end define end math

end "

\item "

begin math define tex of rule gen as text "
Gen" end text end define end math

end "

\item "

begin math define tex of deduction as text "
Ded" end text end define end math

end "

\item "

begin math define tex of repetition as text "
Repetition" end text end define end math

end "

\item "

begin math define tex of lemma a one as text "
A1'" end text end define end math

end "

\item "

begin math define tex of lemma a two as text "
A2'" end text end define end math

end "

\item "

begin math define tex of lemma a four as text "
A4'" end text end define end math

end "

\item "

begin math define tex of lemma a five as text "
A5'" end text end define end math

end "

\item "

begin math define tex of var x is object var as text "#1.
{}^{var}" end text end define end math

end "

\item "

begin math define tex of var x avoid var y as text "#1.
\#.#2." end text end define end math

end "

\item "

begin math define tex of var x avoid zero var y as text "#1.
\#.^0#2." end text end define end math

end "

\item "

begin math define tex of var x avoid one var y as text "#1.
\#.^1#2." end text end define end math

end "

\item "

begin math define tex of var x avoid star var y as text "#1.
\#.^*#2." end text end define end math

end "

\item "

begin math define tex of sub var x is var y where var z is var u end sub as text "
\langle #1.
{\equiv} #2.
| #3.
{:=} #4.
\rangle " end text end define end math

end "

\item "

begin math define tex of sub zero var x is var y where var z is var u end sub as text "
\langle #1.
{\equiv}^0 #2.
| #3.
{:=} #4.
\rangle " end text end define end math

end "

\item "

begin math define tex of sub one var x is var y where var z is var u end sub as text "
\langle #1.
{\equiv}^1 #2.
| #3.
{:=} #4.
\rangle " end text end define end math

end "

\item "

begin math define tex of sub star var x is var y where var z is var u end sub as text "
\langle #1.
{\equiv}^* #2.
| #3.
{:=} #4.
\rangle " end text end define end math

end "

\item "

begin math define tex of deduction var x conclude var y end deduction as text "
Ded(#1.
,#2.
)" end text end define end math

end "

\item "

begin math define tex of deduction zero var x conclude var y end deduction as text "
Ded_0(#1.
,#2.
)" end text end define end math

end "

\item "

begin math define tex of deduction one var x conclude var y condition var z end deduction as text "
Ded_1(#1.
,#2.
,#3.
)" end text end define end math

end "

\item "

begin math define tex of deduction two var x conclude var y condition var z end deduction as text "
Ded_2(#1.
,#2.
,#3.
)" end text end define end math

end "

\item "

begin math define tex of deduction three var x conclude var y condition var z bound var u end deduction as text "
Ded_3(#1.
,#2.
,#3.
,#4.
)" end text end define end math

end "

\item "

begin math define tex of deduction four var x conclude var y condition var z bound var u end deduction as text "
Ded_4(#1.
,#2.
,#3.
,#4.
)" end text end define end math

end "

\item "

begin math define tex of deduction four star var x conclude var y condition var z bound var u end deduction as text "
Ded_4^*(#1.
,#2.
,#3.
,#4.
)" end text end define end math

end "

\item "

begin math define tex of deduction five var x condition var y bound var z end deduction as text "
Ded_5(#1.
,#2.
,#3.
)" end text end define end math

end "

\item "

begin math define tex of deduction six var p conclude var c exception var e bound var b end deduction as text "
Ded_6(#1.
,#2.
,#3.
,#4.
)" end text end define end math

end "

\item "

begin math define tex of deduction six star var p conclude var c exception var e bound var b end deduction as text "
Ded_6^*(#1.
,#2.
,#3.
,#4.
)" end text end define end math

end "

\item "

begin math define tex of deduction seven var p end deduction as text "
Ded_7(#1.
)" end text end define end math

end "

\item "

begin math define tex of deduction eight var p bound var b end deduction as text "
Ded_8(#1.
,#2.
)" end text end define end math

end "

\item "

begin math define tex of deduction eight var p bound var b end deduction as text "
Ded_8^*(#1.
,#2.
)" end text end define end math

end "

\item "

begin math define tex of block var b line var l end block var p as text "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi
$:}$Block {}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$Begin
$\hfill \makebox [0mm][l]{\quad ;}}#1.
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#2.
$:}$Block {}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$End
$\hfill \makebox [0mm][l]{\quad ;}}#3." end text end define end math

end "

\item "

begin math define tex name of block var b line var l end block var p as text "
Begin \, #1.
; #2.
: End ; #3." end text end define end math

end "

\item "

begin math define tex of because var a indeed var i end line as text "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi
$:}$#1.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#2.
$\hfill \makebox [0mm][l]{\quad ;}}" end text end define end math

end "

"

begin math define tex name of because var a indeed var i end line as text "
Last\ block\ line \, #1.
\gg #2.
\,;" end text end define end math

end "

\item "

begin math define tex of var x object modus ponens var y as text "#1.
\unrhd #2." end text end define end math

end "

\item "

begin math define tex of prop three two a as text "
Prop\ 3.2a" end text end define end math

end "

\item "

begin math define tex of prop three two b as text "
Prop\ 3.2b" end text end define end math

end "

\item "

begin math define tex of prop three two c as text "
Prop\ 3.2c" end text end define end math

end "

\item "

begin math define tex of prop three two d as text "
Prop\ 3.2d" end text end define end math

end "

\item "

begin math define tex of prop three two e one as text "
Prop\ 3.2e_1" end text end define end math

end "

\item "

begin math define tex of prop three two e two as text "
Prop\ 3.2e_2" end text end define end math

end "

\item "

begin math define tex of prop three two e as text "
Prop\ 3.2e" end text end define end math

end "

\item "

begin math define tex of prop three two f one as text "
Prop\ 3.2f_1" end text end define end math

end "

\item "

begin math define tex of prop three two f two as text "
Prop\ 3.2f_2" end text end define end math

end "

\item "

begin math define tex of prop three two f as text "
Prop\ 3.2f" end text end define end math

end "

\item "

begin math define tex of prop three two g one as text "
Prop\ 3.2g_1" end text end define end math

end "

\item "

begin math define tex of prop three two g two as text "
Prop\ 3.2g_2" end text end define end math

end "

\item "

begin math define tex of prop three two g as text "
Prop\ 3.2g" end text end define end math

end "

\item "

begin math define tex of prop three two h one as text "
Prop\ 3.2h_1" end text end define end math

end "

\item "

begin math define tex of prop three two h two as text "
Prop\ 3.2h_2" end text end define end math

end "

\item "

begin math define tex of prop three two h as text "
Prop\ 3.2h" end text end define end math

end "

\item "

begin math define tex of macro indent var x as text "
$%
\leftskip=1em%
$#1." end text end define end math

end "

\item "

begin math define tex name of macro indent var x as text "
MacroIndent(#1.
)" end text end define end math

end "

\item "

begin math define tex of block one var t state var s cache var c end block as text "
Block_1(#1.
,#2.
,#3.
)" end text end define end math

end "

\item "

begin math define tex of block two var b end block as text "
Block_2(#1.
)" end text end define end math

end "

\item "

begin math define tex of evaluates to as text "
\rightarrow " end text end define end math

end "

\end{list}



\subsection{Variables}

"

begin math define pyk of object var var x end var as text "object var * end var" end text end define end math

end "

"

begin math define tex of object var var x end var as text "\overline{#1.}" end text end define end math

end "



"

begin math define macro of object a 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 object a as object var var a end var end define end quote end define end define end math

end "

"

begin math define macro of object b 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 object b as object var var b end var end define end quote end define end define end math

end "

"

begin math define macro of object c 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 object c as object var var c end var end define end quote end define end define end math

end "

"

begin math define macro of object d 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 object d as object var var d end var end define end quote end define end define end math

end "

"

begin math define macro of object e 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 object e as object var var e end var end define end quote end define end define end math

end "

"

begin math define macro of object f 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 object f as object var var f end var end define end quote end define end define end math

end "

"

begin math define macro of object g 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 object g as object var var g end var end define end quote end define end define end math

end "

"

begin math define macro of object h 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 object h as object var var h end var end define end quote end define end define end math

end "

"

begin math define macro of object i 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 object i as object var var i end var end define end quote end define end define end math

end "

"

begin math define macro of object j 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 object j as object var var j end var end define end quote end define end define end math

end "

"

begin math define macro of object k 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 object k as object var var k end var end define end quote end define end define end math

end "

"

begin math define macro of object l 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 object l as object var var l end var end define end quote end define end define end math

end "

"

begin math define macro of object m 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 object m as object var var m end var end define end quote end define end define end math

end "

"

begin math define macro of object n 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 object n as object var var n end var end define end quote end define end define end math

end "

"

begin math define macro of object o 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 object o as object var var o end var end define end quote end define end define end math

end "

"

begin math define macro of object p 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 object p as object var var p end var end define end quote end define end define end math

end "

"

begin math define macro of object q 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 object q as object var var q end var end define end quote end define end define end math

end "

"

begin math define macro of object r 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 object r as object var var r end var end define end quote end define end define end math

end "

"

begin math define macro of object s 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 object s as object var var s end var end define end quote end define end define end math

end "

"

begin math define macro of object t 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 object t as object var var t end var end define end quote end define end define end math

end "

"

begin math define macro of object u 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 object u as object var var u end var end define end quote end define end define end math

end "

"

begin math define macro of object v 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 object v as object var var v end var end define end quote end define end define end math

end "

"

begin math define macro of object w 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 object w as object var var w end var end define end quote end define end define end math

end "

"

begin math define macro of object x 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 object x as object var var x end var end define end quote end define end define end math

end "

"

begin math define macro of object 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 object y as object var var y end var end define end quote end define end define end math

end "

"

begin math define macro of object z 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 object z as object var var z end var end define end quote end define end define end math

end "



"

begin math define pyk of object a as text "object a" end text end define end math

end "

"

begin math define pyk of object b as text "object b" end text end define end math

end "

"

begin math define pyk of object c as text "object c" end text end define end math

end "

"

begin math define pyk of object d as text "object d" end text end define end math

end "

"

begin math define pyk of object e as text "object e" end text end define end math

end "

"

begin math define pyk of object f as text "object f" end text end define end math

end "

"

begin math define pyk of object g as text "object g" end text end define end math

end "

"

begin math define pyk of object h as text "object h" end text end define end math

end "

"

begin math define pyk of object i as text "object i" end text end define end math

end "

"

begin math define pyk of object j as text "object j" end text end define end math

end "

"

begin math define pyk of object k as text "object k" end text end define end math

end "

"

begin math define pyk of object l as text "object l" end text end define end math

end "

"

begin math define pyk of object m as text "object m" end text end define end math

end "

"

begin math define pyk of object n as text "object n" end text end define end math

end "

"

begin math define pyk of object o as text "object o" end text end define end math

end "

"

begin math define pyk of object p as text "object p" end text end define end math

end "

"

begin math define pyk of object q as text "object q" end text end define end math

end "

"

begin math define pyk of object r as text "object r" end text end define end math

end "

"

begin math define pyk of object s as text "object s" end text end define end math

end "

"

begin math define pyk of object t as text "object t" end text end define end math

end "

"

begin math define pyk of object u as text "object u" end text end define end math

end "

"

begin math define pyk of object v as text "object v" end text end define end math

end "

"

begin math define pyk of object w as text "object w" end text end define end math

end "

"

begin math define pyk of object x as text "object x" end text end define end math

end "

"

begin math define pyk of object y as text "object y" end text end define end math

end "

"

begin math define pyk of object z as text "object z" end text end define end math

end "



"

begin math define tex of object a as text "
\mathit{a}" end text end define end math

end "

"

begin math define tex of object b as text "
\mathit{b}" end text end define end math

end "

"

begin math define tex of object c as text "
\mathit{c}" end text end define end math

end "

"

begin math define tex of object d as text "
\mathit{d}" end text end define end math

end "

"

begin math define tex of object e as text "
\mathit{e}" end text end define end math

end "

"

begin math define tex of object f as text "
\mathit{f}" end text end define end math

end "

"

begin math define tex of object g as text "
\mathit{g}" end text end define end math

end "

"

begin math define tex of object h as text "
\mathit{h}" end text end define end math

end "

"

begin math define tex of object i as text "
\mathit{i}" end text end define end math

end "

"

begin math define tex of object j as text "
\mathit{j}" end text end define end math

end "

"

begin math define tex of object k as text "
\mathit{k}" end text end define end math

end "

"

begin math define tex of object l as text "
\mathit{l}" end text end define end math

end "

"

begin math define tex of object m as text "
\mathit{m}" end text end define end math

end "

"

begin math define tex of object n as text "
\mathit{n}" end text end define end math

end "

"

begin math define tex of object o as text "
\mathit{o}" end text end define end math

end "

"

begin math define tex of object p as text "
\mathit{p}" end text end define end math

end "

"

begin math define tex of object q as text "
\mathit{q}" end text end define end math

end "

"

begin math define tex of object r as text "
\mathit{r}" end text end define end math

end "

"

begin math define tex of object s as text "
\mathit{s}" end text end define end math

end "

"

begin math define tex of object t as text "
\mathit{t}" end text end define end math

end "

"

begin math define tex of object u as text "
\mathit{u}" end text end define end math

end "

"

begin math define tex of object v as text "
\mathit{v}" end text end define end math

end "

"

begin math define tex of object w as text "
\mathit{w}" end text end define end math

end "

"

begin math define tex of object x as text "
\mathit{x}" end text end define end math

end "

"

begin math define tex of object y as text "
\mathit{y}" end text end define end math

end "

"

begin math define tex of object z as text "
\mathit{z}" end text end define end math

end "



\section{Priority table}

"

begin flush left math define priority of ijcar as preassociative priority ijcar equal priority ijcar 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 general macro define x as x end define equal priority make root visible x end visible equal priority ijcar example axiom equal priority ijcar example rule equal priority ijcar example contradiction equal priority ijcar example theory equal priority ijcar 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 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 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

then x equal priority x

begin x

end 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 safe row x end priority greater than unicode end of text end define end math end left

end "

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