{   Logiweb, a system for electronic distribution of mathematics
    Copyright (C) 2004 Klaus Grue

    This program is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program; if not, write to the Free Software
    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  021111307  USA

    Contact: Klaus Grue, DIKU, Universitetsparken 1, DK2100 Copenhagen,
    Denmark, grue@diku.dk, http://yoa.dk/, http://www.diku.dk/~grue/

    Logiweb is a system for distribution of mathematical definitions,
    lemmas, and proofs. For more on Logiweb, consult http://yoa.dk/.
}

PAGE check

{A bibliography may look like e.g.

 base:               nani
                     seku tisa teki teni neku  sise kati tani sike take
                     kuke nuti sise suka seti  kanu sase nete susu tesu
                     kute susi kunu kinu sana  sese sita nasa natu,
 ground:            "http://yoa.dk/logiweb/page/ground/vector/page.lgw",
 first floor:       "http:first-floor/latest/vector/page.lgw",
 second floor:      "file:page/second-floor/vector/page.lgw"
 third floor:
  "lgw:01A0FFF3C5ACDE30FD3D7FAB8708D230D33DDDFD919184AFC8C9B29A0806"

In general, a bibliography is a comma separated list of bibliographic entries.

Each entry has two elements: A name (like 'base') and then either a reference in mixed endian kana or the url of a page.

The url may start with "http:" in which case it is looked up on the internet. If "http:" is followed by a slash, the url is looked up as it is. Otherwise, it is relative to the "url=..." option of the pyk compiler.

The url may also start with "file:" in which case it is looked up in the local file system.

Finaly, the url may start with "lgw:" in which case the characters following "lgw:" are interpretted as a Logiweb reference in mixed endian kana.}

BIBLIOGRAPHY

base:
nani
suna keke kene kati suka  kiku nena keki neki teke
suse sate nasa kinu nena  kine neki kiki keki sini
sini sata suke kasa kasi  senu sisu nasa natu

PREASSOCIATIVE  base: bracket * end bracket,
parameter term * stack * seed * end parameter,
parameter term star * stack * seed * end parameter,
instantiate * with * end instantiate,
instantiate star * with * end instantiate,
occur * in * end occur,
occur star * in * end occur,
circular * term * substitution * end circular,
circular star * term * substitution * end circular,
unify * with * substitution * end unify,
unify star * with * substitution * end unify,
unify two * with * substitution * end unify,
ell a,
ell b,
ell c,
ell d,
ell e,
ell f,
ell g,
ell h,
ell i,
ell j,
ell k,
ell l,
ell m,
ell n,
ell o,
ell p,
ell q,
ell r,
ell s,
ell t,
ell u,
ell v,
ell w,
ell x,
ell y,
ell z,
ell big a,
ell big b,
ell big c,
ell big d,
ell big e,
ell big f,
ell big g,
ell big h,
ell big i,
ell big j,
ell big k,
ell big l,
ell big m,
ell big n,
ell big o,
ell big p,
ell big q,
ell big r,
ell big s,
ell big t,
ell big u,
ell big v,
ell big w,
ell big x,
ell big y,
ell big z,
ell dummy,
reflexivity lemma,
reflexivity lemma one,
commutativity lemma,
the tactic aspect,
tactic,
tactic define * as * end define,
proof expand * state * cache * end expand,
proof expand list * state * cache * end expand,
proof state,
conclude one * cache * end conclude,
conclude two * proves * cache * end conclude,
conclude three * proves * lemma * substitution * end conclude
PREASSOCIATIVE  base: * sub * end sub
PREASSOCIATIVE  base: unicode start of text * end unicode text
PREASSOCIATIVE  base: * bit nil
PREASSOCIATIVE  base: * apply *
PREASSOCIATIVE  base: * raw head
PREASSOCIATIVE  base: * times *
PREASSOCIATIVE  base: * plus *
PREASSOCIATIVE  base: * term plus * end plus
POSTASSOCIATIVE base: * raw pair *
POSTASSOCIATIVE base: * comma *
PREASSOCIATIVE  base: * boolean equal *
PREASSOCIATIVE  base: not *
PREASSOCIATIVE  base: * and *
PREASSOCIATIVE  base: * or *
POSTASSOCIATIVE base: * macro imply *
POSTASSOCIATIVE base: * guard *
PREASSOCIATIVE  base: * select * else * end select
PREASSOCIATIVE  base: lambda * dot *
PREASSOCIATIVE  base: * init
PREASSOCIATIVE  base: * at *,
* modus ponens *,
* modus probans *,
* conclude *
POSTASSOCIATIVE base: * infer *
PREASSOCIATIVE  base: all * indeed *
POSTASSOCIATIVE base: * rule plus *
POSTASSOCIATIVE base: * cut *
PREASSOCIATIVE  base: * proves *
PREASSOCIATIVE
* proof of * reads *,
line * because * indeed * cut *,
because * indeed * qed,
line * premise * cut *,
line * side condition * cut *,
arbitrary * cut *,
locally define * as * cut *
POSTASSOCIATIVE base: * then *
PREASSOCIATIVE  base: * tab *
PREASSOCIATIVE  base: * row *

BODY

"File page.tex
\documentclass [fleqn]{article}
\setlength {\overfullrule }{1mm}
\input{lgwinclude}

\usepackage{latexsym}

%\setlength{\parindent}{0em}
%\setlength{\parskip}{1ex}

% The font of each Logiweb construct is under tight control except that
% strings are typeset in whatever font is in effect at the time of
% typesetting. This is done to enhance the readability of strings in the
% TeX source generated by Logiweb. The default font for typesetting
% strings is \rm:
\everymath{\rm}

\usepackage{makeidx}
\usepackage{page}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}
\newlength{\bracketwidth}
\settowidth{\bracketwidth}{$[{}$}
\newcommand{\back}{\protect\makebox[-1.0\bracketwidth]{}}

\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 130 490 730}}
\hypersetup{pdftitle=A Logiweb base page}
\hypersetup{colorlinks=true}
\bibliographystyle{plain}

% \tex{something} writes something to page.otx for later inclusion
\newwrite\outex
\newtoks\toktex
\immediate\openout\outex=page.otx
\newcommand{\tex}[1]{\toktex={\item #1}\immediate\write\outex{\the\toktex}}

% \test{something} writes something to page.tst for later inclusion
\newwrite\outest
\immediate\openout\outest=page.tst
\newcommand{\test}[1]{\toktex={\item #1}\immediate\write\outest{\the\toktex}}

% Concerning \catcode`\@=11 : See the TeXbook, Appendix B (page 344).
% \afterheading suppresses indentation once, c.f. latex.ltx.
% \display{something} displays something as a displayed equation except
% that linebreaking is possible and displaymath is not turned on by default.
% The first paragraph after \display{something} is unindented.
% Glue below formulas may be wrong. The definition of \display misses
% something like \addvspace{\belowdisplayskip}.
\catcode`\@=11
\def\afterheading{\@afterheading}
\catcode`\@=12
\newcommand{\display}[1]{\begin{list}{}{\setlength{\leftmargin}{\mathindent}}
\item #1\end{list}

\afterheading}
\newcommand{\statement}[1]{\begin{list}{}{\setlength{\leftmargin}{0mm}}
\item #1\end{list}

\afterheading}

\begin {document}
\title {Introduction to Logiweb}
\author {Klaus Grue}
\maketitle
\tableofcontents
"[ ragged right expansion ]"



\section{Introduction}

Disclaimer: This document is under construction.

Logiweb \cite{logiweb} is a system for distribution of mathematical definitions, lemmas, and proofs. More precisely, the Logiweb standard comprises a format, a semantics, and a protocol for storage, interpretation, and transmission of formal mathematics.

A ``clean'' implementation of Logiweb comprises a Logiweb server, a Logiweb client, and an authoring tool. The Logiweb standard governs the server, the client, and the backend of the authoring tool.

Logiweb allows a user to submit Logiweb pages that contain formal formal mathematics. To submit a page, the user must first produce the page using the authoring tool and then make the page available on the ordinary World Wide Web (WWW) under some Hyper Text Transport Protocal Uniform Resource Locator (http URL). Then the authoring tool must notify the nearest Logiweb server about the submission.

Each Logiweb page has a Logiweb reference which essentially is a global hash key computed on the basis of the contents of the page. Logiweb pages are addressed using Logiweb references but retrieved from WWW using their http URL. The main task of the mesh of Logiweb servers is to translate Logiweb references to http URLs.

A single Logiweb server cannot do the translation from Logiweb reference to http URL alone. Rather, the Logiweb servers form a mesh that cooperate on indexing all Logiweb pages in the world.



\subsection{Legal issues}

Once a Logiweb page is submitted to Logiweb it is understood that anybody is allowed to make verbatim copies of the page and resubmit them to Logiweb. Resubmitted copies have the same Logiweb reference as the original but a different http URL. For this reason, each Logiweb page may have many http URLs but only one Logiweb reference.

To Logiweb, all copies of a Logiweb page are equal, and the original (i.e.\ the first copy submitted to Logiweb) has no special priviledges. A Logiweb page continues to exist as long as there is at least one copy of it on Logiweb. Hence, a Logiweb page may continue to exist even if the original is deleted.

Copyright notices on Logiweb pages may restrict human readers in what they do with the pages, such as modifying them or exporting them to other media than Logiweb. But copyright notices cannot prevent verbatim copying inside Logiweb: verbatim copying is what Logiweb does to submitted pages. To avoid verbatim copying of your page, don't submit it to Logiweb.



\subsection{More legal issues}

The word ``Logiweb'' is a good one and, hence, it is used as a trademark and a registered trademark for many different things. But when used for a format, a semantics, and a protocol for exchange of mathematics via the internet, ``Logiweb'' is a trademark of the author of the present paper. The purpose is to force incompatible versions of Logiweb to pick other names. Furthermore, the blue ``Logiweb and stribes'' logo is a trademark of the author.



\subsection{References}

The reference of the present page is

\display{\tt\lgwCheckHex}

when expressed in \indexintro{mixed endian hexadecimal}. ``Mixed endian'' indicates that the references is written least significant byte first but most significant digit first. Or, stated otherwise, the bytes are written in network byte order but each byte is written with the most significant digit first as in dot-notation for ip-addresses. When written in mixed endian Kana, the reference of the present page reads

\display{\tt\lgwCheckKana}

In the Kana notation, ``n'', ``t'', ``s'', ``k'' represent 00, 01, 10, and 11, respectively. Also, ``a'', ``i'', ``u'', ``e'' represent 00, 01, 10, and 11, respectively. So ``11000100 11000000'' translates to ``kata kana'' and ``00 01 10 11 11 10 01 00'' translates to ``nise kuta''. The Kana format is useful if one has to pronounce a reference.



\subsection{Bibliographies}

Each Logiweb page contains a bibliography which is a list of references to other Logiweb pages. As an example the present page references a page named \href {\lgwBaseUrl}{base}.

As mentioned, the reference of a page depends on the contents of the page and one cannot change a page without affecting its reference. For that reason, an author of a Logiweb page can safely refer to another Logiweb page without fearing that that other page will change. Furthermore, if an author references a Logiweb page, then the author may copy and resubmit that page and in that way ensure that the referenced Logiweb page will not disappear from Logiweb.

The \href {\lgwBaseUrl}{base} page referenced by the present page contains loads of definitions of formal theories and many other things. The present page, which is under construction, states two small proofs that have been machine checked by Logiweb. Furthermore, the present page presents the same proofs in a style that will be supported in the near future.



\section{Logiweb sequent calculus}

\subsection{Unification}

\subsubsection{Parameter terms}

We shall refer to terms in which bound metavariables are replaced by cardinals as \index{term, parameter}\index{parameter term}\intro{parameter terms}. The function "[ bracket parameter term var t stack var s seed var n end parameter end bracket ]" converts an ordinary term "[ bracket var t end bracket ]" into a parameter term in which numbers are constructed from "[ bracket var n end bracket ]" using "[ bracket var b double var n end bracket ]" iteratively. When calling "[ bracket parameter term var t stack var s seed var n end parameter end bracket ]", "[ bracket var s end bracket ]" should be "[ bracket true end bracket ]".

%
\index{parameter term x stack y seed z end parameter "[ bracket parameter term var x stack var y seed var z end parameter end bracket ]"}%
%
\index{parm @\back "[ bracket parameter term var x stack var y seed var z end parameter end bracket ]" parameter term x stack y seed z end parameter}%
%
\tex{"[ math tex define parameter term var t stack var s seed var n end parameter as "
parm(#1.
,#2.
,#3.
)" end define end math ]"}%
%
\statement{"[ math value define parameter term var t stack var s seed var n end parameter as var n tagged guard newline

open if var t term root equal quote all var x indeed var y end quote then all var n indeed parameter term var t second stack parenthesis var t first pair var n end parenthesis pair var s seed true double var n end parameter else newline

let var m be lookup var t stack var s default true end lookup in newline

open if not var m then var m else var t root pair parameter term star var t tail stack var s seed var n end parameter end define end math ]"%
%
\footnote{"[ math pyk define parameter term var t stack var s seed var n end parameter as "parameter term * stack * seed * end parameter" end define end math ]"}}
%

%
\index{parameter term star x stack y seed z end parameter "[ bracket parameter term star var x stack var y seed var z end parameter end bracket ]"}%
%
\index{parm @\back "[ bracket parameter term star var x stack var y seed var z end parameter end bracket ]" parameter term star x stack y seed z end parameter}%
%
\tex{"[ math tex define parameter term star var t stack var s seed var n end parameter as "
parm^*(#1.
,#2.
,#3.
)" end define end math ]"}%
%
\statement{"[ math value define parameter term star var t stack var s seed var n end parameter as var s tagged guard var n tagged guard 

tagged if var t is atomic then true else parameter term var t head stack var s seed var n end parameter pair parameter term star var t tail stack var s seed var n end parameter end if end define end math ]"%
%
\footnote{"[ math pyk define parameter term star var t stack var s seed var n end parameter as "parameter term star * stack * seed * end parameter" end define end math ]"}}
%



\subsubsection{Substitutions}

We shall refer to an array of terms as a substitution. The following function instantiates a parameter term "[ bracket var t end bracket ]" using a substitution "[ bracket var s end bracket ]":

%
\index{instantiate x with y end instantiate "[ bracket instantiate var x with var y end instantiate end bracket ]"}%
%
\index{inst @\back "[ bracket instantiate var x with var y end instantiate end bracket ]" instantiate x with y end instantiate}%
%
\tex{"[ math tex define instantiate var t with var s end instantiate as "
inst(#1.
,#2.
)" end define end math ]"}%
%
\statement{"[ math value define instantiate var t with var s end instantiate as tagged if var t is cardinal then var s assoc var t end assoc else var t root pair instantiate star var t tail with var s end instantiate end if end define end math ]"%
%
\footnote{"[ math pyk define instantiate var t with var s end instantiate as "instantiate * with * end instantiate" end define end math ]"}}
%

%
\index{instantiate star x with y end instantiate "[ bracket instantiate star var x with var y end instantiate end bracket ]"}%
%
\index{inst @\back "[ bracket instantiate star var x with var y end instantiate end bracket ]" instantiate star x with y end instantiate}%
%
\tex{"[ math tex define instantiate star var t with var s end instantiate as "
inst^*(#1.
,#2.
)" end define end math ]"}%
%
\statement{"[ math value define instantiate star var t with var s end instantiate as var s tagged guard tagged if var t is atomic then true else instantiate var t head with var s end instantiate pair instantiate star var t tail with var s end instantiate end if end define end math ]"%
%
\footnote{"[ math pyk define instantiate star var t with var s end instantiate as "instantiate star * with * end instantiate" end define end math ]"}}
%

\test{"[ math test instantiate parameter term quote all var x indeed all var y indeed var x plus var y end quote stack true seed four end parameter with true set four to quote var u end quote end set set eight to quote var v end quote end set end instantiate term equal quote all var u indeed all var v indeed var u plus var v end quote end test end math ]"}



\subsubsection{Occurrence}

"[ bracket occur var t in var u end occur end bracket ]" is true if the parameter "[ bracket var t end bracket ]" occurs in the parameter term "[ bracket var u end bracket ]":

%
\index{occur x in y end occur "[ bracket occur var x in var y end occur end bracket ]"}%
%
\index{occur @\back "[ bracket occur var x in var y end occur end bracket ]" occur x in y end occur}%
%
\tex{"[ math tex define occur var t in var u end occur as "
occur(#1.
,#2.
)" end define end math ]"}%
%
\statement{"[ math value define occur var t in var u end occur as tagged if var u is cardinal then var t tagged equal var u else occur star var t in var u tail end occur end if end define end math ]"%
%
\footnote{"[ math pyk define occur var t in var u end occur as "occur * in * end occur" end define end math ]"}}
%

%
\index{occur star x in y end occur "[ bracket occur star var x in var y end occur end bracket ]"}%
%
\index{occur @\back "[ bracket occur star var x in var y end occur end bracket ]" occur star x in y end occur}%
%
\tex{"[ math tex define occur star var t in var u end occur as "
occur^*(#1.
,#2.
)" end define end math ]"}%
%
\statement{"[ math value define occur star var t in var u end occur as var t tagged guard tagged if var u is atomic then false else occur var t in var u head end occur macro or occur star var t in var u tail end occur end if end define end math ]"%
%
\footnote{"[ math pyk define occur star var t in var u end occur as "occur star * in * end occur" end define end math ]"}}
%

\test{math test occur eight in parameter term quote not all var x indeed var x end quote end occur end test end math}

\test{math false test occur nine in parameter term quote not all var x indeed var x end quote end occur end test end math}



\subsubsection{Unifications}

We shall refer to the result of applying a substitution to a parameter term as an \indexintro{instance} of the term. We shall refer to a common instance of two parameter terms as a \indexintro{unification} of the terms. As an example, "[ bracket meta a pair two end bracket ]" and "[ bracket one pair meta b end bracket ]" (where "[ bracket meta a end bracket ]" and "[ bracket meta b end bracket ]" denote numbers) have exactly one unification, namely "[ bracket one pair two end bracket ]". We shall say that two terms are \indexintro{compatible} if they have at least one unification and \indexintro{incompatible} otherwise.

A substitution which yields the same result when applied to two terms "[ bracket var u end bracket ]" and "[ bracket var v end bracket ]" is said to \indexintro{unify} the terms. As an example, the substitution which maps "[ bracket meta a end bracket ]" to "[ bracket one end bracket ]" and "[ bracket meta b end bracket ]" to "[ bracket two end bracket ]" unifies "[ bracket meta a pair two end bracket ]" and "[ bracket one pair meta b end bracket ]".

The \index{algorithm, unification}\indexintro{unification algorithm} presented in the following takes two terms as input and returns a unifying substitution if the terms are compatible. As an example, when applied to "[ bracket meta a pair two end bracket ]" and "[ bracket one pair meta b end bracket ]", the unification algorithm returns the substitution which maps "[ bracket meta a end bracket ]" to "[ bracket one end bracket ]" and "[ bracket meta b end bracket ]" to "[ bracket two end bracket ]".

There is more than one substitution which unifies "[ bracket meta a pair two end bracket ]" and "[ bracket one pair meta b end bracket ]". As an example the substitution that maps "[ bracket meta a end bracket ]" to "[ bracket one end bracket ]", "[ bracket meta b end bracket ]" to "[ bracket two end bracket ]", and "[ bracket meta c end bracket ]" to "[ bracket three end bracket ]" also unifies "[ bracket meta a pair two end bracket ]" and "[ bracket one pair meta b end bracket ]".



\subsubsection{Circularity test}

"[ bracket circular var t term var u substitution var s end circular end bracket ]" is true if adding the equation "[ bracket var t math equal var u end bracket ]" to the unification "[ bracket var s end bracket ]" creates a circularity.

%
\index{circular x term y substitution z end circular "[ bracket circular var x term var y substitution var z end circular end bracket ]"}%
%
\index{circular @\back "[ bracket circular var x term var y substitution var z end circular end bracket ]" circular x term y substitution z end circular}%
%
\tex{"[ math tex define circular var t term var u substitution var s end circular as "
circular(#1.
=#2.
,#3.
)" end define end math ]"}%
%
\statement{"[ math value define circular var t term var u substitution var s end circular as var s tagged guard tagged if var u is cardinal then var t tagged equal var u macro or occur var t in var s assoc var u end assoc end occur else circular star var t term var u tail substitution var s end circular end if end define end math ]"%
%
\footnote{"[ math pyk define circular var t term var u substitution var s end circular as "circular * term * substitution * end circular" end define end math ]"}}
%

%
\index{circular star x term y substitution z end circular "[ bracket circular star var x term var y substitution var z end circular end bracket ]"}%
%
\index{circular @\back "[ bracket circular star var x term var y substitution var z end circular end bracket ]" circular star x term y substitution z end circular}%
%
\tex{"[ math tex define circular star var t term var u substitution var s end circular as "
circular^*(#1.
=#2.
,#3.
)" end define end math ]"}%
%
\statement{"[ math value define circular star var t term var u substitution var s end circular as var t tagged guard var s tagged guard tagged if var u is atomic then false else circular var t term var u head substitution var s end circular macro or circular star var t term var u tail substitution var s end circular end if end define end math ]"%
%
\footnote{"[ math pyk define circular star var t term var u substitution var s end circular as "circular star * term * substitution * end circular" end define end math ]"}}
%



\subsubsection{Unification algorithm}

%
\index{unify x with y substitution z end unify "[ bracket unify var x with var y substitution var z end unify end bracket ]"}%
%
\index{unify @\back "[ bracket unify var x with var y substitution var z end unify end bracket ]" unify x with y substitution z end unify}%
%
\tex{"[ math tex define unify var t with var u substitution var s end unify as "
unify(#1.
=#2.
,#3.
)" end define end math ]"}%
%
\statement{"[ math value define unify var t with var u substitution var s end unify as var t tagged guard var u tagged guard newline

open if var s is cardinal then var s else newline

open if var t is cardinal then unify two var t with var u substitution var s end unify else newline

open if var u is cardinal then unify two var u with var t substitution var s end unify else newline

open if var t term root equal var u then unify star var t tail with var u tail substitution var s end unify else zero end define end math ]"%
%
\footnote{"[ math pyk define unify var t with var u substitution var s end unify as "unify * with * substitution * end unify" end define end math ]"}}
%

%
\index{unify star x with y substitution z end unify "[ bracket unify star var x with var y substitution var z end unify end bracket ]"}%
%
\index{unify @\back "[ bracket unify star var x with var y substitution var z end unify end bracket ]" unify star x with y substitution z end unify}%
%
\tex{"[ math tex define unify star var t with var u substitution var s end unify as "
unify^*(#1.
=#2.
,#3.
)" end define end math ]"}%
%
\statement{"[ math value define unify star var t with var u substitution var s end unify as var u tagged guard tagged if var t is atomic then var s else unify star var t tail with var u tail substitution unify var t head with var u head substitution var s end unify end unify end if end define end math ]"%
%
\footnote{"[ math pyk define unify star var t with var u substitution var s end unify as "unify star * with * substitution * end unify" end define end math ]"}}
%

%
\index{unify two x with y substitution z end unify "[ bracket unify two var x with var y substitution var z end unify end bracket ]"}%
%
\index{unify @\back "[ bracket unify two var x with var y substitution var z end unify end bracket ]" unify two x with y substitution z end unify}%
%
\tex{"[ math tex define unify two var t with var u substitution var s end unify as "
unify_2(#1.
=#2.
,#3.
)" end define end math ]"}%
%
\statement{"[ math value define unify two var t with var u substitution var s end unify as newline

open if var t tagged equal var u then var s else newline

let var t prime be var s assoc var t end assoc in newline

open if not var t prime then unify var t prime with var u substitution var s end unify else newline

open if circular var t term var u substitution var s end circular then zero else var s set var t to var u end set end define end math ]"%
%
\footnote{"[ math pyk define unify two var t with var u substitution var s end unify as "unify two * with * substitution * end unify" end define end math ]"}}
%

\test{"[ math test unify quote two end quote with quote two end quote substitution true end unify end test end math ]"}

\test{"[ math test unify quote two end quote with quote three end quote substitution true end unify tagged equal zero end test end math ]"}

\test{"[ math test unify quote two plus three end quote with quote two plus three end quote substitution true end unify end test end math ]"}

\test{"[ math test unify quote two plus three end quote with quote two plus four end quote substitution true end unify tagged equal zero end test end math ]"}

\test{"[ math test unify quote two end quote with three substitution true end unify assoc three end assoc term equal quote two end quote end test end math ]"}

\test{"[ math test unify three with quote two end quote substitution true end unify assoc three end assoc term equal quote two end quote end test end math ]"}

\test{"[ math test unify tuple quote var x plus var y end quote root comma one comma quote three end quote end tuple with quote two plus three end quote substitution true end unify assoc one end assoc term equal quote two end quote end test end math ]"}

\test{"[ math test unify tuple quote var x plus var y end quote root comma one comma quote three end quote end tuple with tuple quote var x plus var y end quote root comma quote two end quote comma two end tuple substitution true end unify assoc one end assoc term equal quote two end quote end test end math ]"}

\test{"[ math test unify parameter term quote meta a plus three end quote stack tuple quote meta a end quote pair one end tuple seed one end parameter with parameter term quote two plus meta b end quote stack tuple quote meta b end quote pair two end tuple seed one end parameter substitution true end unify assoc one end assoc term equal quote two end quote end test end math ]"}

\test{"[ math test unify parameter term quote meta a plus three end quote stack tuple quote meta a end quote pair one end tuple seed one end parameter with parameter term quote two plus meta b end quote stack tuple quote meta b end quote pair two end tuple seed one end parameter substitution true end unify assoc two end assoc term equal quote three end quote end test end math ]"}

\test{"[ math test instantiate parameter term quote meta a plus meta b end quote stack tuple quote meta a end quote pair one comma quote meta b end quote pair two end tuple seed one end parameter with unify parameter term quote meta a plus three end quote stack tuple quote meta a end quote pair one end tuple seed one end parameter with parameter term quote two plus meta b end quote stack tuple quote meta b end quote pair two end tuple seed one end parameter substitution true end unify end instantiate term equal quote two plus three end quote end test end math ]"}



\subsection{Proof generation}\label{section:ProofGeneration}

\subsubsection{Example lemmas}

As examples of sequent proofs, we prove two lemmas in the example theory "[ bracket example theory end bracket ]":

%
\index{reflexivity lemma "[ bracket reflexivity lemma end bracket ]"}%
%
\index{Reflexivity @\back "[ bracket reflexivity lemma end bracket ]" reflexivity lemma}%
%
\tex{"[ math tex define reflexivity lemma as "
Reflexivity" end define end math ]"}%
%
\statement{"[ math in theory example theory lemma reflexivity lemma says all meta a indeed meta a math equal meta a end lemma end math ]"%
%
\footnote{"[ math pyk define reflexivity lemma as "reflexivity lemma" end define end math ]"}}
%

\statement{"[ math proof of reflexivity lemma reads quote example theory infer all meta a indeed parenthesis macro newline

example scheme lemma init modus dereference modus at meta a at meta a cut macro newline

parenthesis example rule lemma init modus dereference modus at parenthesis meta a pair meta a end parenthesis head at meta a at meta a end parenthesis modus modus end parenthesis end quote end proof end math ]"}

%
\index{commutativity lemma "[ bracket commutativity lemma end bracket ]"}%
%
\index{Commutativity @\back "[ bracket commutativity lemma end bracket ]" commutativity lemma}%
%
\tex{"[ math tex define commutativity lemma as "
Commutativity" end define end math ]"}%
%
\statement{"[ math in theory example theory lemma commutativity lemma says all meta a indeed all meta b indeed meta a math equal meta b infer meta b math equal meta a end lemma end math ]"%
%
\footnote{"[ math pyk define commutativity lemma as "commutativity lemma" end define end math ]"}}
%

\statement{"[ math proof of commutativity lemma reads quote example theory infer all meta a indeed all meta b indeed meta a math equal meta b infer parenthesis macro newline

reflexivity lemma init modus dereference modus at meta a cut macro newline

parenthesis example rule lemma init modus dereference modus at meta a at meta b at meta a end parenthesis modus modus end parenthesis end quote end proof end math ]"}

As can be seen on the diagnose hook of the present page, the proofs above are correct according the the machine check made by the verifier.



\subsubsection{Medium level proofs}

In the following we define ``proof tactics'' and a ``proof expander'' which can translate medium level proofs like the one below to Logiweb sequent calculus proofs like the ones above. Actually, the proof below will translate to the proof of reflexivity above.

%
\index{reflexivity lemma one "[ bracket reflexivity lemma one end bracket ]"}%
%
\index{Reflexivity @\back "[ bracket reflexivity lemma one end bracket ]" reflexivity lemma one}%
%
\tex{"[ math tex define reflexivity lemma one as "
Reflexivity_1" end define end math ]"}%
%
\statement{"[ math in theory example theory lemma reflexivity lemma one says all meta a indeed meta a math equal meta a end lemma end math ]"%
%
\footnote{"[ math pyk define reflexivity lemma one as "reflexivity lemma one" end define end math ]"}}
%

\statement{"[ math

example theory proof of reflexivity lemma one reads

arbitrary meta a cut

line ell b because example scheme lemma indeed parenthesis meta a pair meta a end parenthesis head math equal meta a cut

because example rule lemma modus ponens ell b modus ponens ell b indeed meta a math equal meta a qed end math ]"}



\subsubsection{Proof tactics}

Counted in sequent operators, proofs typically comprise a small amount of original thought and a lot of trivial derivations. Frequently, trivial derivations can be generated by computer programs. Such programs are typically called \index{tactic, proof}\intro{tactics} or \index{proof tactic}\intro{proof tactics} \cite{Gordon79}.

To support proof tactics, we introduce a \indexintro{tactic aspect} for defining them and a  \indexintro{proof expander} for evaluating them. The proof  evaluates proof tactics and generates sequent proofs, which the proof evaluator may then evaluate to sequents.

The proof expander is itself a tactic since it generates proofs. The proof expander is a value defined tactic like the rule lemma tactic defined previously. But the proof expander is a particularly general tactic which brings life to tactics that are defined using the tactic aspect.

We make the "[ bracket the tactic aspect end bracket ]" aspect self-evaluating and use "[ bracket tactic end bracket ]" to denote it:

%
\index{tactic @\back "[ bracket the tactic aspect end bracket ]" the tactic aspect}%
%
\index{the tactic aspect "[ bracket the tactic aspect end bracket ]"}%
%
\tex{"[ math tex define the tactic aspect as "
{<}tactic{>}" end define end math ]"}%
%
\display{"[ math value define the tactic aspect as quote the tactic aspect end quote end define end math ]"%
%
\footnote{"[ math pyk define the tactic aspect as "the tactic aspect" end define end math ]"}}
%

%
\index{tactic "[ bracket tactic end bracket ]"}%
%
\tex{"[ math tex define tactic as "
tactic" end define end math ]"}%
%
\display{"[ math message define tactic as the tactic aspect end define end math ]"%
%
\footnote{"[ math pyk define tactic as "tactic" end define end math ]"}}
%

For convenience, we define a construct for making tactic definitions:

\index{tactic define x as y end define "[ math tactic define var x as var y end define end math ]"}%
%
\index{tactic: "[ math tactic define var x as var y end define end math ]"}%
%
\tex{"[ math tex define tactic define var x as var y end define as "
[#1/tex name/tex.
\stackrel {tactic}{=}#2.
]" end define end math ]"}%
%
\display{%
"[ math macro define tactic define var x as var y end define as define tactic of protect var x end protect as var y end define end define end math ]"%
%
\footnote{"[ math pyk define tactic define var x as var y end define as "tactic define * as * end define" end define end math ]"}}



\subsubsection{The proof expander}

The proof expander "[ bracket proof expand var t state var s cache var c end expand end bracket ]" proof expands the term "[ bracket var t end bracket ]" for the \indexintro{proof state} "[ bracket var s end bracket ]" and the cache "[ bracket var c end bracket ]" and returns the result as a semitagged map. The untagged version "[ bracket map untag proof expand var t state var s cache var c end expand end untag end bracket ]" is the expansion itself.

The proof expander "[ bracket proof expand var t state var s cache var c end expand end bracket ]" differs from the macro expander "[ bracket expand var t state var s cache var c end expand end bracket ]" in that it has no special treatment for page symbols and in that it uses the "[ bracket tactic end bracket ]" aspect instead of the "[ bracket macro end bracket ]" aspect.

When proofs are expanded, they are first macro expanded and then proof expanded. Macro expansion is done iteratively until the codex reaches a fixed point whereas proof expansion is done only once. Furthermore, the result of macro expansion is kept in the codex whereas the result of proof expansion is discarded as soon as a proof is checked. Hence, proof expansion is a momentary burden to the computers memory whereas macro expansion is chronic.

The definition of "[ bracket proof expand var t state var s cache var c end expand end bracket ]" is almost identical to that of "[ bracket expand var t state var s cache var c end expand end bracket ]". But it is easier to express since we can use macros like the `let' macro when defining proof expansion. For obvious reasons, macros cannot be used when defining the notion of macro expansion. The definition of "[ bracket proof expand var t state var s cache var c end expand end bracket ]" reads:

%
\index{p: "[ bracket proof expand var x state var y cache var z end expand end bracket ]" proof expand x state y cache z end expand}%
%
\tex{"[ math tex define proof expand var t state var s cache var c end expand as "
{\cal P}( #1.
, #2.
, #3.
)" end define end math ]"}%
%
\display{"[ math value define proof expand var t state var s cache var c end expand as var s tagged guard newline

let var d be aspect the tactic aspect term var t cache var c end aspect in newline

open if var d then var t head pair proof expand list var t tail state var s cache var c end expand else newline

normalizing untag eval var d third stack true cache var c end eval tagged apply var t tagged apply var s tagged apply var c end untag end define end math ]"%
%
\footnote{"[ math pyk define proof expand var t state var s cache var c end expand as "proof expand * state * cache * end expand" end define end math ]"}}
%

%
\index{p: "[ bracket proof expand list var x state var y cache var z end expand end bracket ]" proof expand list x state y cache z end expand}%
%
\tex{"[ math tex define proof expand list var t state var s cache var c end expand as "
{\cal P}^*( #1.
, #2.
, #3.
)" end define end math ]"}%
%
\display{"[ math value define proof expand list var t state var s cache var c end expand as var s tagged guard var c tagged guard tagged if var t then true else proof expand var t head state var s cache var c end expand pair proof expand list var t tail state var s cache var c end expand end if end define end math ]"%
%
\footnote{"[ math pyk define proof expand list var t state var s cache var c end expand as "proof expand list * state * cache * end expand" end define end math ]"}}
%



\subsubsection{The initial proof state}

Proof states have exactly the same format as macro states.

The \index{proof state, initial}\indexintro{initial proof state} "[ bracket proof state end bracket ]" is useful for passing as the second parameter to "[ bracket proof expand var t state var s cache var c end expand end bracket ]". "[ bracket proof state end bracket ]" is a pair whose head is the proof expander itself and whose tail is left blank. The definition of "[ bracket proof state end bracket ]" reads:

%
\index{p: "[ bracket proof state end bracket ]" proof state}%
%
\tex{"[ math tex define proof state as "
p_0" end define end math ]"}%
%
\display{"[ math define value of proof state as map tag lambda var t dot lambda var s dot lambda var c dot proof expand var t state var s cache var c end expand end tag pair true end define end math ]"%
%
\footnote{"[ math pyk define proof state as "proof state" end define end math ]"}}
%

The function "[ bracket state expand var t state var s cache var c end expand end bracket ]" defined previously macro expands the term "[ bracket var t end bracket ]" using the macro expander embedded in the macro state "[ bracket var s end bracket ]" using the cache "[ bracket var c end bracket ]". Since proof states have exactly the same syntax and semantics as macro states, we shall take the liberty to use "[ bracket state expand var t state var s cache var c end expand end bracket ]" for proof states also.



\subsubsection{The conclusion tactic}

The \index{tactic, conclusion}\indexintro{conclusion tactic} "[ bracket var x conclude var y end bracket ]" constructs a proof of "[ bracket var y end bracket ]" from the partial proof "[ bracket var x end bracket ]". The conclusion tactic does the following to the proof "[ bracket var x end bracket ]":

\begin{itemize}

\item Whenever "[ bracket var x end bracket ]" references a lemma "[ bracket var l end bracket ]", the conclusion tactic replaces "[ bracket var l end bracket ]" by "[ bracket var l init modus dereference modus end bracket ]".

\item Whenever a subproof "[ bracket var u end bracket ]" of "[ bracket var x end bracket ]" proves "[ bracket all var v indeed var w end bracket ]", the conclusion tactic replaces "[ bracket var u end bracket ]" by "[ bracket var u at var a end bracket ]" where the tactic uses unification to guess "[ bracket var a end bracket ]".

\item Whenever a subproof "[ bracket var u end bracket ]" of "[ bracket var x end bracket ]" proves "[ bracket var v endorse var w end bracket ]", the conclusion tactic replaces "[ bracket var u end bracket ]" by "[ bracket var u verify end bracket ]".

\end{itemize}

%
\index{\alpha x conclude y @\back "[ bracket var x conclude var y end bracket ]" x conclude y}%
%
\tex{"[ math tex define var x conclude var y as "#1.
\gg #2." end define end math ]"}%
%
\display{"[ math tactic define var x conclude var y as lambda var t dot lambda var s dot lambda var c dot conclude one var t cache var c end conclude end define end math ]"%
%
\footnote{"[ math pyk define var x conclude var y as "* conclude *" end define end math ]"}}
%

%
\index{conclude @\back "[ bracket conclude one var x cache var y end conclude end bracket ]" conclude one x cache y end conclude}%
%
\tex{"[ math tex define conclude one var t cache var c end conclude as "
conclude_1 ( #1.
, #2.
)" end define end math ]"}%
%
\display{"[ math value define conclude one var t cache var c end conclude as newline

let var r be conclude two var t first proves var t second cache var c end conclude in newline

open if var r is cardinal then error "Unification failed" term var t end error else var r end define end math ]"%
%
\footnote{"[ math pyk define conclude one var t cache var c end conclude as "conclude one * cache * end conclude" end define end math ]"}}
%

%
\index{conclude @\back "[ bracket conclude two var x proves var y cache var z end conclude end bracket ]" conclude two x proves y cache z end conclude}%
%
\tex{"[ math tex define conclude two var a proves var t cache var c end conclude as "
conclude_2 ( #1.
, #2.
, #3.
)" end define end math ]"}%
%
\display{"[ math value define conclude two var a proves var t cache var c end conclude as var t tagged guard newline

open if var a term root equal quote var x modus ponens var y end quote then conclude two var a first proves var a color var t modus ponens var a second end color cache var c end conclude else newline

open if var a term root equal quote var x modus probans var y end quote then conclude two var a first proves var a color var t modus probans var a second end color cache var c end conclude else newline

open if var a term root equal quote var x at var y end quote then conclude two var a first proves var a color var t at var a second end color cache var c end conclude else newline

open if aspect the proof aspect term var a cache var c end aspect then error "Lemma expected" term var a end error else newline

let var d be aspect the statement aspect term var a cache var c end aspect in newline

conclude three var a init modus dereference modus proves var t lemma parameter term var d third second stack true seed one end parameter substitution true end conclude end define end math ]"%
%
\footnote{"[ math pyk define conclude two var a proves var t cache var c end conclude as "conclude two * proves * cache * end conclude" end define end math ]"}}
%

%
\index{conclude @\back "[ bracket conclude three var x proves var y lemma var z substitution var a end conclude end bracket ]" conclude three x proves y lemma z substitution a end conclude}%
%
\tex{"[ math tex define conclude three var a proves var t lemma var l substitution var s end conclude as "
conclude_3 ( #1.
, #2.
, #3.
, #4.
)" end define end math ]"}%
%
\display{"[ math value define conclude three var a proves var t lemma var l substitution var s end conclude as var a tagged guard var t tagged guard var l tagged guard var s tagged guard newline

open if var l term root equal quote var x infer var y end quote then newline

var t term root equal quote var x modus ponens var y end quote select conclude three {var t color} var a modus {end color} proves var t first lemma var l second substitution unify var l first with var t second substitution var s end unify end conclude else conclude three {var a color} var a modus {end color} proves var t lemma var l second substitution var s end conclude end select else newline

open if var l term root equal quote var x endorse var y end quote then newline

var t term root equal quote var x modus probans var y end quote select conclude three {var t color} var a modus {end color} proves var t first lemma var l second substitution unify var l first with var t second substitution var s end unify end conclude else conclude three {var a color} var a modus {end color} proves var t lemma var l second substitution var s end conclude end select else newline

open if var l term root equal quote all var x indeed var y end quote then newline

var t term root equal quote var x at var y end quote select conclude three {var t color} var a at var t second {end color} proves var t first lemma var l second substitution unify var l first with var t second substitution var s end unify end conclude else conclude three {var a color} var a at var l first {end color} proves var t lemma var l second substitution var s end conclude end select else newline

let var s be unify var l with var t substitution var s end unify in newline

open if var s is cardinal then var s else newline

instantiate var a with var s end instantiate {var a} end define end math ]"%
%
\footnote{"[ math pyk define conclude three var a proves var t lemma var l substitution var s end conclude as "conclude three * proves * lemma * substitution * end conclude" end define end math ]"}}
%

Modus ponens:

%
\index{\alpha x modus ponens y @\back "[ bracket var x modus ponens var y end bracket ]" x modus ponens y}%
%
\tex{"[ math tex define var x modus ponens var y as "#1.
\rhd #2." end define end math ]"}%
%
\display{"[ math value define var x modus ponens var y as tuple quote var x modus ponens var y end quote root comma var x comma var y end tuple end define end math ]"%
%
\footnote{"[ math pyk define var x modus ponens var y as "* modus ponens *" end define end math ]"}}
%

Modus probans:

%
\index{\alpha x modus probans y @\back "[ bracket var x modus probans var y end bracket ]" x modus probans y}%
%
\tex{"[ math tex define var x modus probans var y as "#1.
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} #2." end define end math ]"}%
%
\display{"[ math value define var x modus probans var y as tuple quote var x modus probans var y end quote root comma var x comma var y end tuple end define end math ]"%
%
\footnote{"[ math pyk define var x modus probans var y as "* modus probans *" end define end math ]"}}
%



\subsubsection{Proof constructors}

Medium level proofs will be constructed from the constructs listed in the following. In the following the constructs are listed using their texname aspects. This is convenient when talking about the constructs. In the medium level proof above, the constructs are typeset using the tex aspect; the tex aspects include newline and tabulation commands which make proofs pleasing to read.

%
\index{\alpha x proof of y reads z @\back "[ bracket text var x proof of var y reads var z end text end bracket ]" x proof of y reads z}%
%
\index{proof: "[ bracket text var x proof of var y reads var z end text end bracket ]" x proof of y reads z}%
%
\tex{"[ math tex define var t proof of var s reads var p as "
\if\relax\csname lgwprooflinep\endcsname
\def\lgwprooflinep{x}
\newcount\lgwproofline
\fi
\begingroup
\def\insideproof{x}
\lgwproofline=0 #1.
\mathbf {\ proof\ of\ } #2.
\colon #3.
\gdef\lgwella{\relax}
\gdef\lgwellb{\relax}
\gdef\lgwellc{\relax}
\gdef\lgwelld{\relax}
\gdef\lgwelle{\relax}
\gdef\lgwellf{\relax}
\gdef\lgwellg{\relax}
\gdef\lgwellh{\relax}
\gdef\lgwelli{\relax}
\gdef\lgwellj{\relax}
\gdef\lgwellk{\relax}
\gdef\lgwelll{\relax}
\gdef\lgwellm{\relax}
\gdef\lgwelln{\relax}
\gdef\lgwello{\relax}
\gdef\lgwellp{\relax}
\gdef\lgwellq{\relax}
\gdef\lgwellr{\relax}
\gdef\lgwells{\relax}
\gdef\lgwellt{\relax}
\gdef\lgwellu{\relax}
\gdef\lgwellv{\relax}
\gdef\lgwellw{\relax}
\gdef\lgwellx{\relax}
\gdef\lgwelly{\relax}
\gdef\lgwellz{\relax}
\gdef\lgwellbiga{\relax}
\gdef\lgwellbigb{\relax}
\gdef\lgwellbigc{\relax}
\gdef\lgwellbigd{\relax}
\gdef\lgwellbige{\relax}
\gdef\lgwellbigf{\relax}
\gdef\lgwellbigg{\relax}
\gdef\lgwellbigh{\relax}
\gdef\lgwellbigi{\relax}
\gdef\lgwellbigj{\relax}
\gdef\lgwellbigk{\relax}
\gdef\lgwellbigl{\relax}
\gdef\lgwellbigm{\relax}
\gdef\lgwellbign{\relax}
\gdef\lgwellbigo{\relax}
\gdef\lgwellbigp{\relax}
\gdef\lgwellbigq{\relax}
\gdef\lgwellbigr{\relax}
\gdef\lgwellbigs{\relax}
\gdef\lgwellbigt{\relax}
\gdef\lgwellbigu{\relax}
\gdef\lgwellbigv{\relax}
\gdef\lgwellbigw{\relax}
\gdef\lgwellbigx{\relax}
\gdef\lgwellbigy{\relax}
\gdef\lgwellbigz{\relax}
\endgroup " end define end math ]"}%
%
\tex{"[ math tex name define var t proof of var s reads var p as "#1.
\mathbf{\ proof\ of\ } #2.
: #3." end define end math ]"}
%
\display{"[ math macro define var t proof of var s reads var p as proof of var s reads lambda var c dot lambda var x dot proof expand quote var t infer var p end quote state proof state cache var c end expand end proof end define end math ]"%
%
\footnote{"[ math pyk define var t proof of var l reads var p as "* proof of * reads *" end define end math ]"}}
%

%
\index{Line @\back "[ bracket text line var x because var y indeed var z cut var a end text end bracket ]" line x because y indeed z cut a}%
%
\index{line x because y indeed z cut a "[ bracket text line var x because var y indeed var z cut var a end text end bracket ]"}%
%
\tex{"[ math tex define line var l because var a indeed var i cut var p as "
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$#1.
$:}$#2.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#3.
$\hfill \makebox [0mm][l]{\quad ;}}#4." end define end math ]"}%
%
\tex{"[ math tex name define line var l because var a indeed var i cut var p as "
Line \, #1.
: #2.
\gg #3.
; #4." end define end math ]"}%
%
\display{"[ math macro define line var l because var a indeed var i cut var p as parenthesis var a conclude var i cut let var l abbreviate var i in var p end parenthesis end define end math ]"%
%
\footnote{"[ math pyk define line var l because var a indeed var i cut var p as "line * because * indeed * cut *" end define end math ]"}}
%

%
\index{Last line @\back "[ bracket text because var x indeed var y qed end text end bracket ]" because x indeed y qed}%
%
\index{because x indeed y qed "[ bracket text because var x indeed var y qed end text end bracket ]"}%
%
\tex{"[ math tex define because var a indeed var i qed as "
\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 \makebox[0mm]{$\Box$}}}" end define end math ]"}%
%
\tex{"[ math tex name define because var a indeed var i qed as "
Last\ line \, #1.
\gg #2." end define end math ]"}%
%
\display{"[ math macro define because var a indeed var i qed as parenthesis var a conclude var i end parenthesis end define end math ]"%
%
\footnote{"[ math pyk define because var a indeed var i qed as "because * indeed * qed" end define end math ]"}}
%

%
\index{premise @\back "[ bracket text line var x premise var y cut var z end text end bracket ]" line x premise y cut z}%
%
\index{line x premise y cut z "[ bracket text line var x premise var y cut var z end text end bracket ]"}%
%
\tex{"[ math tex define line var l premise var i cut var p as "
\newline \makebox [0.1\textwidth ][l]{$#1.
$:}\makebox [0.4\textwidth ][l]{$Premise{}\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$#2.
$\hfill \makebox [0mm][l]{\quad ;}}#3." end define end math ]"}%
%
\tex{"[ math tex name define line var l premise var i cut var p as "
Line \, #1.
: Premise \gg #2.
;#3." end define end math ]"}%
%
\display{"[ math macro define line var l premise var i cut var p as parenthesis var i infer let var l abbreviate var i in var p end parenthesis end define end math ]"%
%
\footnote{"[ math pyk define line var l premise var i cut var p as "line * premise * cut *" end define end math ]"}}
%

%
\index{side condition @\back "[ bracket text line var x side condition var y cut var z end text end bracket ]" line x side condition y cut z}%
%
\index{line x side condition y cut z "[ bracket text line var x side condition var y cut var z end text end bracket ]"}%
%
\tex{"[ math tex define line var l side condition var i cut var p as "
\newline \makebox [0.1\textwidth ][l]{$#1.
$:}\makebox [0.4\textwidth ][l]{
$\mbox{Side-condition}{}\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$#2.
$\hfill \makebox [0mm][l]{\quad ;}}#3." end define end math ]"}%
%
\tex{"[ math tex name define line var l side condition var i cut var p as "
Line \, #1.
: \mbox{Side-condition} \gg #2.
; #3." end define end math ]"}%
%
\display{"[ math macro define line var l side condition var i cut var p as parenthesis var i endorse let var l abbreviate var i in var p end parenthesis end define end math ]"%
%
\footnote{"[ math pyk define line var l side condition var i cut var p as "line * side condition * cut *" end define end math ]"}}
%

%
\index{arbitrary @\back "[ bracket text arbitrary var y cut var z end text end bracket ]" arbitrary x cut y}%
%
\index{arbitrary x cut y "[ bracket text arbitrary var x cut var y end text end bracket ]"}%
%
\tex{"[ math tex define arbitrary var i cut var p as "
\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 define end math ]"}%
%
\tex{"[ math tex name define arbitrary var i cut var p as "
Arbitrary \gg #1.
;#2." end define end math ]"}%
%
\display{"[ math macro define arbitrary var i cut var p as parenthesis all var i indeed var p end parenthesis end define end math ]"%
%
\footnote{"[ math pyk define arbitrary var i cut var p as "arbitrary * cut *" end define end math ]"}}
%

%
\index{local @\back "[ bracket text locally define var x as var y cut var z end text end bracket ]" locally define x as y cut z}%
%
\index{locally define x as y cut z "[ bracket text locally define var x as var y cut var z end text end bracket ]"}%
%
\tex{"[ math tex define locally define var a as var i cut var p as "
\newline\makebox[0.1\textwidth]{$
\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]{$Local{}\gg{}$}%
\quad%
\parbox[t]{0.4\textwidth}{$#1.
= #2.
$\hfill\makebox[0mm][l]{\quad ;}}#3." end define end math ]"}%
%
\tex{"[ math tex name define locally define var a as var i cut var p as "
Local \gg #1.
= #2.
; #3." end define end math ]"}%
%
\display{"[ math macro define locally define var a as var i cut var p as parenthesis let var a abbreviate var i in var p end parenthesis end define end math ]"%
%
\footnote{"[ math pyk define locally define var u as var v cut var p as "locally define * as * cut *" end define end math ]"}}
%



\appendix

\section{Chores}

The name of the page:

\display{"[ math pyk define check as "check" end define end math ]"}

\test{"[ math test true end test end math ]"}



\subsection{Line numbers}

The following definitions are experimental definitions of line numbers named ``ell a'', ``ell b'', etc.\ which expand into $[L_{01}]$, $[L_{02}]$, etc.\ in such a way that proof lines are numbered in succession. The ``ell dummy'' operator expands into different line numbers each time it is used and can be used for lines that are never referenced.

\begin{flushleft}
"[ math pyk define ell a as "ell a" end define end math ]"
"[ math pyk define ell b as "ell b" end define end math ]"
"[ math pyk define ell c as "ell c" end define end math ]"
"[ math pyk define ell d as "ell d" end define end math ]"
"[ math pyk define ell e as "ell e" end define end math ]"
"[ math pyk define ell f as "ell f" end define end math ]"
"[ math pyk define ell g as "ell g" end define end math ]"
"[ math pyk define ell h as "ell h" end define end math ]"
"[ math pyk define ell i as "ell i" end define end math ]"
"[ math pyk define ell j as "ell j" end define end math ]"
"[ math pyk define ell k as "ell k" end define end math ]"
"[ math pyk define ell l as "ell l" end define end math ]"
"[ math pyk define ell m as "ell m" end define end math ]"
"[ math pyk define ell n as "ell n" end define end math ]"
"[ math pyk define ell o as "ell o" end define end math ]"
"[ math pyk define ell p as "ell p" end define end math ]"
"[ math pyk define ell q as "ell q" end define end math ]"
"[ math pyk define ell r as "ell r" end define end math ]"
"[ math pyk define ell s as "ell s" end define end math ]"
"[ math pyk define ell t as "ell t" end define end math ]"
"[ math pyk define ell u as "ell u" end define end math ]"
"[ math pyk define ell v as "ell v" end define end math ]"
"[ math pyk define ell w as "ell w" end define end math ]"
"[ math pyk define ell x as "ell x" end define end math ]"
"[ math pyk define ell y as "ell y" end define end math ]"
"[ math pyk define ell z as "ell z" end define end math ]"
"[ math pyk define ell big a as "ell big a" end define end math ]"
"[ math pyk define ell big b as "ell big b" end define end math ]"
"[ math pyk define ell big c as "ell big c" end define end math ]"
"[ math pyk define ell big d as "ell big d" end define end math ]"
"[ math pyk define ell big e as "ell big e" end define end math ]"
"[ math pyk define ell big f as "ell big f" end define end math ]"
"[ math pyk define ell big g as "ell big g" end define end math ]"
"[ math pyk define ell big h as "ell big h" end define end math ]"
"[ math pyk define ell big i as "ell big i" end define end math ]"
"[ math pyk define ell big j as "ell big j" end define end math ]"
"[ math pyk define ell big k as "ell big k" end define end math ]"
"[ math pyk define ell big l as "ell big l" end define end math ]"
"[ math pyk define ell big m as "ell big m" end define end math ]"
"[ math pyk define ell big n as "ell big n" end define end math ]"
"[ math pyk define ell big o as "ell big o" end define end math ]"
"[ math pyk define ell big p as "ell big p" end define end math ]"
"[ math pyk define ell big q as "ell big q" end define end math ]"
"[ math pyk define ell big r as "ell big r" end define end math ]"
"[ math pyk define ell big s as "ell big s" end define end math ]"
"[ math pyk define ell big t as "ell big t" end define end math ]"
"[ math pyk define ell big u as "ell big u" end define end math ]"
"[ math pyk define ell big v as "ell big v" end define end math ]"
"[ math pyk define ell big w as "ell big w" end define end math ]"
"[ math pyk define ell big x as "ell big x" end define end math ]"
"[ math pyk define ell big y as "ell big y" end define end math ]"
"[ math pyk define ell big z as "ell big z" end define end math ]"
"[ math pyk define ell dummy as "ell dummy" end define end math ]"

"[ math tex name define ell a as "L_a" end define end math ]"
"[ math tex name define ell b as "L_b" end define end math ]"
"[ math tex name define ell c as "L_c" end define end math ]"
"[ math tex name define ell d as "L_d" end define end math ]"
"[ math tex name define ell e as "L_e" end define end math ]"
"[ math tex name define ell f as "L_f" end define end math ]"
"[ math tex name define ell g as "L_g" end define end math ]"
"[ math tex name define ell h as "L_h" end define end math ]"
"[ math tex name define ell i as "L_i" end define end math ]"
"[ math tex name define ell j as "L_j" end define end math ]"
"[ math tex name define ell k as "L_k" end define end math ]"
"[ math tex name define ell l as "L_l" end define end math ]"
"[ math tex name define ell m as "L_m" end define end math ]"
"[ math tex name define ell n as "L_n" end define end math ]"
"[ math tex name define ell o as "L_o" end define end math ]"
"[ math tex name define ell p as "L_p" end define end math ]"
"[ math tex name define ell q as "L_q" end define end math ]"
"[ math tex name define ell r as "L_r" end define end math ]"
"[ math tex name define ell s as "L_s" end define end math ]"
"[ math tex name define ell t as "L_t" end define end math ]"
"[ math tex name define ell u as "L_u" end define end math ]"
"[ math tex name define ell v as "L_v" end define end math ]"
"[ math tex name define ell w as "L_w" end define end math ]"
"[ math tex name define ell x as "L_x" end define end math ]"
"[ math tex name define ell y as "L_y" end define end math ]"
"[ math tex name define ell z as "L_z" end define end math ]"
"[ math tex name define ell big a as "L_A" end define end math ]"
"[ math tex name define ell big b as "L_B" end define end math ]"
"[ math tex name define ell big c as "L_C" end define end math ]"
"[ math tex name define ell big d as "L_D" end define end math ]"
"[ math tex name define ell big e as "L_E" end define end math ]"
"[ math tex name define ell big f as "L_F" end define end math ]"
"[ math tex name define ell big g as "L_G" end define end math ]"
"[ math tex name define ell big h as "L_H" end define end math ]"
"[ math tex name define ell big i as "L_I" end define end math ]"
"[ math tex name define ell big j as "L_J" end define end math ]"
"[ math tex name define ell big k as "L_K" end define end math ]"
"[ math tex name define ell big l as "L_L" end define end math ]"
"[ math tex name define ell big m as "L_M" end define end math ]"
"[ math tex name define ell big n as "L_N" end define end math ]"
"[ math tex name define ell big o as "L_O" end define end math ]"
"[ math tex name define ell big p as "L_P" end define end math ]"
"[ math tex name define ell big q as "L_Q" end define end math ]"
"[ math tex name define ell big r as "L_R" end define end math ]"
"[ math tex name define ell big s as "L_S" end define end math ]"
"[ math tex name define ell big t as "L_T" end define end math ]"
"[ math tex name define ell big u as "L_U" end define end math ]"
"[ math tex name define ell big v as "L_V" end define end math ]"
"[ math tex name define ell big w as "L_W" end define end math ]"
"[ math tex name define ell big x as "L_X" end define end math ]"
"[ math tex name define ell big y as "L_Y" end define end math ]"
"[ math tex name define ell big z as "L_Z" end define end math ]"
"[ math tex name define ell dummy as "L_?" end define end math ]"
\end{flushleft}

"[ math tex define ell a as "
\if \relax \csname lgwprooflinep\endcsname L_a \else
\if \relax \csname lgwella\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwella {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwella \fi " end define end math ]"

"[ math tex define ell b as "
\if \relax \csname lgwprooflinep\endcsname L_b \else
\if \relax \csname lgwellb\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellb {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellb \fi " end define end math ]"

"[ math tex define ell c as "
\if \relax \csname lgwprooflinep\endcsname L_c \else
\if \relax \csname lgwellc\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellc {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellc \fi " end define end math ]"

"[ math tex define ell d as "
\if \relax \csname lgwprooflinep\endcsname L_d \else
\if \relax \csname lgwelld\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwelld {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwelld \fi " end define end math ]"

"[ math tex define ell e as "
\if \relax \csname lgwprooflinep\endcsname L_e \else
\if \relax \csname lgwelle\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwelle {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwelle \fi " end define end math ]"

"[ math tex define ell f as "
\if \relax \csname lgwprooflinep\endcsname L_f \else
\if \relax \csname lgwellf\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellf {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellf \fi " end define end math ]"

"[ math tex define ell g as "
\if \relax \csname lgwprooflinep\endcsname L_g \else
\if \relax \csname lgwellg\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellg {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellg \fi " end define end math ]"

"[ math tex define ell h as "
\if \relax \csname lgwprooflinep\endcsname L_h \else
\if \relax \csname lgwellh\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellh {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellh \fi " end define end math ]"

"[ math tex define ell i as "
\if \relax \csname lgwprooflinep\endcsname L_i \else
\if \relax \csname lgwelli\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwelli {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwelli \fi " end define end math ]"

"[ math tex define ell j as "
\if \relax \csname lgwprooflinep\endcsname L_j \else
\if \relax \csname lgwellj\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellj {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellj \fi " end define end math ]"

"[ math tex define ell k as "
\if \relax \csname lgwprooflinep\endcsname L_k \else
\if \relax \csname lgwellk\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellk {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellk \fi " end define end math ]"

"[ math tex define ell l as "
\if \relax \csname lgwprooflinep\endcsname L_l \else
\if \relax \csname lgwelll\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwelll {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwelll \fi " end define end math ]"

"[ math tex define ell m as "
\if \relax \csname lgwprooflinep\endcsname L_m \else
\if \relax \csname lgwellm\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellm {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellm \fi " end define end math ]"

"[ math tex define ell n as "
\if \relax \csname lgwprooflinep\endcsname L_n \else
\if \relax \csname lgwelln\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwelln {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwelln \fi " end define end math ]"

"[ math tex define ell o as "
\if \relax \csname lgwprooflinep\endcsname L_o \else
\if \relax \csname lgwello\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwello \fi " end define end math ]"

"[ math tex define ell p as "
\if \relax \csname lgwprooflinep\endcsname L_p \else
\if \relax \csname lgwellp\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellp {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellp \fi " end define end math ]"

"[ math tex define ell q as "
\if \relax \csname lgwprooflinep\endcsname L_q \else
\if \relax \csname lgwellq\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellq {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellq \fi " end define end math ]"

"[ math tex define ell r as "
\if \relax \csname lgwprooflinep\endcsname L_r \else
\if \relax \csname lgwellr\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellr {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellr \fi " end define end math ]"

"[ math tex define ell s as "
\if \relax \csname lgwprooflinep\endcsname L_s \else
\if \relax \csname lgwells\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwells {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwells \fi " end define end math ]"

"[ math tex define ell t as "
\if \relax \csname lgwprooflinep\endcsname L_t \else
\if \relax \csname lgwellt\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellt {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellt \fi " end define end math ]"

"[ math tex define ell u as "
\if \relax \csname lgwprooflinep\endcsname L_u \else
\if \relax \csname lgwellu\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellu {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellu \fi " end define end math ]"

"[ math tex define ell v as "
\if \relax \csname lgwprooflinep\endcsname L_v \else
\if \relax \csname lgwellv\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellv {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellv \fi " end define end math ]"

"[ math tex define ell w as "
\if \relax \csname lgwprooflinep\endcsname L_w \else
\if \relax \csname lgwellw\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellw {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellw \fi " end define end math ]"

"[ math tex define ell x as "
\if \relax \csname lgwprooflinep\endcsname L_x \else
\if \relax \csname lgwellx\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellx {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellx \fi " end define end math ]"

"[ math tex define ell y as "
\if \relax \csname lgwprooflinep\endcsname L_y \else
\if \relax \csname lgwelly\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwelly {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwelly \fi " end define end math ]"

"[ math tex define ell z as "
\if \relax \csname lgwprooflinep\endcsname L_z \else
\if \relax \csname lgwellz\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellz {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellz \fi " end define end math ]"

"[ math tex define ell big a as "
\if \relax \csname lgwprooflinep\endcsname L_A \else
\if \relax \csname lgwellbiga\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbiga {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbiga \fi " end define end math ]"

"[ math tex define ell big b as "
\if \relax \csname lgwprooflinep\endcsname L_B \else
\if \relax \csname lgwellbigb\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigb {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigb \fi " end define end math ]"

"[ math tex define ell big c as "
\if \relax \csname lgwprooflinep\endcsname L_C \else
\if \relax \csname lgwellbigc\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigc {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigc \fi " end define end math ]"

"[ math tex define ell big d as "
\if \relax \csname lgwprooflinep\endcsname L_D \else
\if \relax \csname lgwellbigd\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigd {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigd \fi " end define end math ]"

"[ math tex define ell big e as "
\if \relax \csname lgwprooflinep\endcsname L_E \else
\if \relax \csname lgwellbige\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbige {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbige \fi " end define end math ]"

"[ math tex define ell big f as "
\if \relax \csname lgwprooflinep\endcsname L_F \else
\if \relax \csname lgwellbigf\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigf {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigf \fi " end define end math ]"

"[ math tex define ell big g as "
\if \relax \csname lgwprooflinep\endcsname L_G \else
\if \relax \csname lgwellbigg\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigg {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigg \fi " end define end math ]"

"[ math tex define ell big h as "
\if \relax \csname lgwprooflinep\endcsname L_H \else
\if \relax \csname lgwellbigh\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigh {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigh \fi " end define end math ]"

"[ math tex define ell big i as "
\if \relax \csname lgwprooflinep\endcsname L_I \else
\if \relax \csname lgwellbigi\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigi {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigi \fi " end define end math ]"

"[ math tex define ell big j as "
\if \relax \csname lgwprooflinep\endcsname L_J \else
\if \relax \csname lgwellbigj\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigj {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigj \fi " end define end math ]"

"[ math tex define ell big k as "
\if \relax \csname lgwprooflinep\endcsname L_K \else
\if \relax \csname lgwellbigk\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigk {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigk \fi " end define end math ]"

"[ math tex define ell big l as "
\if \relax \csname lgwprooflinep\endcsname L_L \else
\if \relax \csname lgwellbigl\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigl {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigl \fi " end define end math ]"

"[ math tex define ell big m as "
\if \relax \csname lgwprooflinep\endcsname L_M \else
\if \relax \csname lgwellbigm\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigm {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigm \fi " end define end math ]"

"[ math tex define ell big n as "
\if \relax \csname lgwprooflinep\endcsname L_N \else
\if \relax \csname lgwellbign\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbign {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbign \fi " end define end math ]"

"[ math tex define ell big o as "
\if \relax \csname lgwprooflinep\endcsname L_O \else
\if \relax \csname lgwellbigo\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigo {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigo \fi " end define end math ]"

"[ math tex define ell big p as "
\if \relax \csname lgwprooflinep\endcsname L_P \else
\if \relax \csname lgwellbigp\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigp {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigp \fi " end define end math ]"

"[ math tex define ell big q as "
\if \relax \csname lgwprooflinep\endcsname L_Q \else
\if \relax \csname lgwellbigq\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigq {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigq \fi " end define end math ]"

"[ math tex define ell big r as "
\if \relax \csname lgwprooflinep\endcsname L_R \else
\if \relax \csname lgwellbigr\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigr {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigr \fi " end define end math ]"

"[ math tex define ell big s as "
\if \relax \csname lgwprooflinep\endcsname L_S \else
\if \relax \csname lgwellbigs\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigs {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigs \fi " end define end math ]"

"[ math tex define ell big t as "
\if \relax \csname lgwprooflinep\endcsname L_T \else
\if \relax \csname lgwellbigt\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigt {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigt \fi " end define end math ]"

"[ math tex define ell big u as "
\if \relax \csname lgwprooflinep\endcsname L_U \else
\if \relax \csname lgwellbigu\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigu {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigu \fi " end define end math ]"

"[ math tex define ell big v as "
\if \relax \csname lgwprooflinep\endcsname L_V \else
\if \relax \csname lgwellbigv\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigv {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigv \fi " end define end math ]"

"[ math tex define ell big w as "
\if \relax \csname lgwprooflinep\endcsname L_W \else
\if \relax \csname lgwellbigw\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigw {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigw \fi " end define end math ]"

"[ math tex define ell big x as "
\if \relax \csname lgwprooflinep\endcsname L_X \else
\if \relax \csname lgwellbigx\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigx {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigx \fi " end define end math ]"

"[ math tex define ell big y as "
\if \relax \csname lgwprooflinep\endcsname L_Y \else
\if \relax \csname lgwellbigy\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigy {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigy \fi " end define end math ]"

"[ math tex define ell big z as "
\if \relax \csname lgwprooflinep\endcsname L_Z \else
\if \relax \csname lgwellbigz\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellbigz {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellbigz \fi " end define end math ]"

"[ math tex define ell dummy as "
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi " end define end math ]"



\section{\TeX\ definitions}

\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\immediate\closeout\outex
\input{./page.otx}
\end{list}



\section{Test}

Test cases are listed here. To avoid \TeX\ errors about missing items, a trivial test has been included.

\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\immediate\closeout\outest
\input{./page.tst}
\end{list}



\section{Priority table}\label{section:PriorityTable}


"[ flush left math priority table Priority end table end math end left ]"



\section{Index}

\newcommand\myidxitem{\par\noindent}

\renewenvironment{theindex}{\let\item\myidxitem}{}

\printindex



\section{Bibliography}

\bibliography{./page}

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

@article      {berline97,
  author    = {C. Berline and K. Grue},
  title     = {A $\kappa$-denotational semantics for {M}ap {T}heory
               in {ZFC+SI}},
  journal   = TCS,
  year      = {1997},
  volume    = {179},
  number    = {1--2},
  pages     = {137--202},
  month     = {jun}}

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

@Article      {godel,
  author    = {K. G{\"!o}del},
  title     = {{\"!U}ber for\-mal un\-ent\-scheid\-ba\-re
               \mbox{S\"!at}\-ze der \mbox{Prin}\-ci\-pia 
               \mbox{Mathe}\-ma\-ti\-ca und ver\-wand\-ter
               \mbox{Sys}\-teme \mbox{I}},
  journal   = {Mo\-nats\-hef\-te f{\"!u}r Mathe\-ma\-tik und Phy\-sik},
  year      = {19\-31},
  volume    = {12},
  number    = {\mbox{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}}

@inproceedings{Logiweb,
  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}}

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

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

End of file
File page.sty
% thebibliography environment from
% /usr/share/texmf/tex/latex/base/book.cls
% with \chapter removed
\renewenvironment{thebibliography}[1]
     {\list{\@biblabel{\@arabic\c@enumiv}}%
           {\settowidth\labelwidth{\@biblabel{#1}}%
            \leftmargin\labelwidth
            \advance\leftmargin\labelsep
            \@openbib@code
            \usecounter{enumiv}%
            \let\p@enumiv\@empty
            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
      \sloppy
      \clubpenalty4000
      \@clubpenalty \clubpenalty
      \widowpenalty4000%
      \sfcode`\.\@m}
     {\def\@noitemerr
       {\@latex@warning{Empty `thebibliography' environment}}%
      \endlist}
End of file
latex page
makeindex page
bibtex page
latex page
makeindex page
latex page"