"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
"
begin ragged right
end "
\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 "
begin bracket parameter term var t stack var s seed var n end parameter end bracket
end " converts an ordinary term "
begin bracket var t end bracket
end " into a parameter term in which numbers are constructed from "
begin bracket var n end bracket
end " using "
begin bracket var b double var n end bracket
end " iteratively. When calling "
begin bracket parameter term var t stack var s seed var n end parameter end bracket
end ", "
begin bracket var s end bracket
end " should be "
begin bracket true end bracket
end ".
%
\index{parameter term x stack y seed z end parameter "
begin bracket parameter term var x stack var y seed var z end parameter end bracket
end "}%
%
\index{parm @\back "
begin bracket parameter term var x stack var y seed var z end parameter end bracket
end " parameter term x stack y seed z end parameter}%
%
\tex{"
begin math define tex of parameter term var t stack var s seed var n end parameter as text "
parm(#1.
,#2.
,#3.
)" end text end define end math
end "}%
%
\statement{"
begin math define value of parameter term var t stack var s seed var n end parameter as var n tagged guard newline tagged 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 var t first pair var n pair var s seed true double var n end parameter else newline let one lambda var m dot newline tagged 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 if apply lookup var t stack var s default true end lookup end let end if end define end math
end "%
%
\footnote{"
begin math define pyk of parameter term var t stack var s seed var n end parameter as text "parameter term * stack * seed * end parameter" end text end define end math
end "}}
%
%
\index{parameter term star x stack y seed z end parameter "
begin bracket parameter term star var x stack var y seed var z end parameter end bracket
end "}%
%
\index{parm @\back "
begin bracket parameter term star var x stack var y seed var z end parameter end bracket
end " parameter term star x stack y seed z end parameter}%
%
\tex{"
begin math define tex of parameter term star var t stack var s seed var n end parameter as text "
parm^*(#1.
,#2.
,#3.
)" end text end define end math
end "}%
%
\statement{"
begin math define value of 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
end "%
%
\footnote{"
begin math define pyk of parameter term star var t stack var s seed var n end parameter as text "parameter term star * stack * seed * end parameter" end text end define end math
end "}}
%
\subsubsection{Substitutions}
We shall refer to an array of terms as a substitution. The following function instantiates a parameter term "
begin bracket var t end bracket
end " using a substitution "
begin bracket var s end bracket
end ":
%
\index{instantiate x with y end instantiate "
begin bracket instantiate var x with var y end instantiate end bracket
end "}%
%
\index{inst @\back "
begin bracket instantiate var x with var y end instantiate end bracket
end " instantiate x with y end instantiate}%
%
\tex{"
begin math define tex of instantiate var t with var s end instantiate as text "
inst(#1.
,#2.
)" end text end define end math
end "}%
%
\statement{"
begin math define value of 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
end "%
%
\footnote{"
begin math define pyk of instantiate var t with var s end instantiate as text "instantiate * with * end instantiate" end text end define end math
end "}}
%
%
\index{instantiate star x with y end instantiate "
begin bracket instantiate star var x with var y end instantiate end bracket
end "}%
%
\index{inst @\back "
begin bracket instantiate star var x with var y end instantiate end bracket
end " instantiate star x with y end instantiate}%
%
\tex{"
begin math define tex of instantiate star var t with var s end instantiate as text "
inst^*(#1.
,#2.
)" end text end define end math
end "}%
%
\statement{"
begin math define value of 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
end "%
%
\footnote{"
begin math define pyk of instantiate star var t with var s end instantiate as text "instantiate star * with * end instantiate" end text end define end math
end "}}
%
\test{"
begin 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
end "}
\subsubsection{Occurrence}
"
begin bracket occur var t in var u end occur end bracket
end " is true if the parameter "
begin bracket var t end bracket
end " occurs in the parameter term "
begin bracket var u end bracket
end ":
%
\index{occur x in y end occur "
begin bracket occur var x in var y end occur end bracket
end "}%
%
\index{occur @\back "
begin bracket occur var x in var y end occur end bracket
end " occur x in y end occur}%
%
\tex{"
begin math define tex of occur var t in var u end occur as text "
occur(#1.
,#2.
)" end text end define end math
end "}%
%
\statement{"
begin math define value of 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
end "%
%
\footnote{"
begin math define pyk of occur var t in var u end occur as text "occur * in * end occur" end text end define end math
end "}}
%
%
\index{occur star x in y end occur "
begin bracket occur star var x in var y end occur end bracket
end "}%
%
\index{occur @\back "
begin bracket occur star var x in var y end occur end bracket
end " occur star x in y end occur}%
%
\tex{"
begin math define tex of occur star var t in var u end occur as text "
occur^*(#1.
,#2.
)" end text end define end math
end "}%
%
\statement{"
begin math define value of occur star var t in var u end occur as var t tagged guard tagged if var u is atomic then false else tagged if occur var t in var u head end occur then true else occur star var t in var u tail end occur end if end if end define end math
end "%
%
\footnote{"
begin math define pyk of occur star var t in var u end occur as text "occur star * in * end occur" end text end define end math
end "}}
%
\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, "
begin bracket metavar var a end metavar pair two end bracket
end " and "
begin bracket one pair metavar var b end metavar end bracket
end " (where "
begin bracket metavar var a end metavar end bracket
end " and "
begin bracket metavar var b end metavar end bracket
end " denote numbers) have exactly one unification, namely "
begin bracket one pair two end bracket
end ". 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 "
begin bracket var u end bracket
end " and "
begin bracket var v end bracket
end " is said to \indexintro{unify} the terms. As an example, the substitution which maps "
begin bracket metavar var a end metavar end bracket
end " to "
begin bracket one end bracket
end " and "
begin bracket metavar var b end metavar end bracket
end " to "
begin bracket two end bracket
end " unifies "
begin bracket metavar var a end metavar pair two end bracket
end " and "
begin bracket one pair metavar var b end metavar end bracket
end ".
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 "
begin bracket metavar var a end metavar pair two end bracket
end " and "
begin bracket one pair metavar var b end metavar end bracket
end ", the unification algorithm returns the substitution which maps "
begin bracket metavar var a end metavar end bracket
end " to "
begin bracket one end bracket
end " and "
begin bracket metavar var b end metavar end bracket
end " to "
begin bracket two end bracket
end ".
There is more than one substitution which unifies "
begin bracket metavar var a end metavar pair two end bracket
end " and "
begin bracket one pair metavar var b end metavar end bracket
end ". As an example the substitution that maps "
begin bracket metavar var a end metavar end bracket
end " to "
begin bracket one end bracket
end ", "
begin bracket metavar var b end metavar end bracket
end " to "
begin bracket two end bracket
end ", and "
begin bracket metavar var c end metavar end bracket
end " to "
begin bracket three end bracket
end " also unifies "
begin bracket metavar var a end metavar pair two end bracket
end " and "
begin bracket one pair metavar var b end metavar end bracket
end ".
\subsubsection{Circularity test}
"
begin bracket circular var t term var u substitution var s end circular end bracket
end " is true if adding the equation "
begin bracket var t math equal var u end bracket
end " to the unification "
begin bracket var s end bracket
end " creates a circularity.
%
\index{circular x term y substitution z end circular "
begin bracket circular var x term var y substitution var z end circular end bracket
end "}%
%
\index{circular @\back "
begin bracket circular var x term var y substitution var z end circular end bracket
end " circular x term y substitution z end circular}%
%
\tex{"
begin math define tex of circular var t term var u substitution var s end circular as text "
circular(#1.
=#2.
,#3.
)" end text end define end math
end "}%
%
\statement{"
begin math define value of circular var t term var u substitution var s end circular as var s tagged guard tagged if var u is cardinal then tagged if var t tagged equal var u then true else occur var t in var s assoc var u end assoc end occur end if else circular star var t term var u tail substitution var s end circular end if end define end math
end "%
%
\footnote{"
begin math define pyk of circular var t term var u substitution var s end circular as text "circular * term * substitution * end circular" end text end define end math
end "}}
%
%
\index{circular star x term y substitution z end circular "
begin bracket circular star var x term var y substitution var z end circular end bracket
end "}%
%
\index{circular @\back "
begin bracket circular star var x term var y substitution var z end circular end bracket
end " circular star x term y substitution z end circular}%
%
\tex{"
begin math define tex of circular star var t term var u substitution var s end circular as text "
circular^*(#1.
=#2.
,#3.
)" end text end define end math
end "}%
%
\statement{"
begin math define value of 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 tagged if circular var t term var u head substitution var s end circular then true else circular star var t term var u tail substitution var s end circular end if end if end define end math
end "%
%
\footnote{"
begin math define pyk of circular star var t term var u substitution var s end circular as text "circular star * term * substitution * end circular" end text end define end math
end "}}
%
\subsubsection{Unification algorithm}
%
\index{unify x with y substitution z end unify "
begin bracket unify var x with var y substitution var z end unify end bracket
end "}%
%
\index{unify @\back "
begin bracket unify var x with var y substitution var z end unify end bracket
end " unify x with y substitution z end unify}%
%
\tex{"
begin math define tex of unify var t with var u substitution var s end unify as text "
unify(#1.
=#2.
,#3.
)" end text end define end math
end "}%
%
\statement{"
begin math define value of unify var t with var u substitution var s end unify as var t tagged guard var u tagged guard newline tagged if var s is cardinal then var s else newline tagged if var t is cardinal then unify two var t with var u substitution var s end unify else newline tagged if var u is cardinal then unify two var u with var t substitution var s end unify else newline tagged 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 if end if end if end if end define end math
end "%
%
\footnote{"
begin math define pyk of unify var t with var u substitution var s end unify as text "unify * with * substitution * end unify" end text end define end math
end "}}
%
%
\index{unify star x with y substitution z end unify "
begin bracket unify star var x with var y substitution var z end unify end bracket
end "}%
%
\index{unify @\back "
begin bracket unify star var x with var y substitution var z end unify end bracket
end " unify star x with y substitution z end unify}%
%
\tex{"
begin math define tex of unify star var t with var u substitution var s end unify as text "
unify^*(#1.
=#2.
,#3.
)" end text end define end math
end "}%
%
\statement{"
begin math define value of 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
end "%
%
\footnote{"
begin math define pyk of unify star var t with var u substitution var s end unify as text "unify star * with * substitution * end unify" end text end define end math
end "}}
%
%
\index{unify two x with y substitution z end unify "
begin bracket unify two var x with var y substitution var z end unify end bracket
end "}%
%
\index{unify @\back "
begin bracket unify two var x with var y substitution var z end unify end bracket
end " unify two x with y substitution z end unify}%
%
\tex{"
begin math define tex of unify two var t with var u substitution var s end unify as text "
unify_2(#1.
=#2.
,#3.
)" end text end define end math
end "}%
%
\statement{"
begin math define value of unify two var t with var u substitution var s end unify as newline tagged if var t tagged equal var u then var s else newline let one lambda var t prime dot newline tagged if not var t prime then unify var t prime with var u substitution var s end unify else newline tagged 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 if end if apply var s assoc var t end assoc end let end if end define end math
end "%
%
\footnote{"
begin math define pyk of unify two var t with var u substitution var s end unify as text "unify two * with * substitution * end unify" end text end define end math
end "}}
%
\test{"
begin math test unify quote two end quote with quote two end quote substitution true end unify end test end math
end "}
\test{"
begin math test unify quote two end quote with quote three end quote substitution true end unify tagged equal zero end test end math
end "}
\test{"
begin math test unify quote two plus three end quote with quote two plus three end quote substitution true end unify end test end math
end "}
\test{"
begin 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
end "}
\test{"
begin 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
end "}
\test{"
begin 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
end "}
\test{"
begin math test unify quote var x plus var y end quote root pair one pair quote three end quote pair true 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
end "}
\test{"
begin math test unify quote var x plus var y end quote root pair one pair quote three end quote pair true with quote var x plus var y end quote root pair quote two end quote pair two pair true substitution true end unify assoc one end assoc term equal quote two end quote end test end math
end "}
\test{"
begin math test unify parameter term quote metavar var a end metavar plus three end quote stack quote metavar var a end metavar end quote pair one pair true seed one end parameter with parameter term quote two plus metavar var b end metavar end quote stack quote metavar var b end metavar end quote pair two pair true seed one end parameter substitution true end unify assoc one end assoc term equal quote two end quote end test end math
end "}
\test{"
begin math test unify parameter term quote metavar var a end metavar plus three end quote stack quote metavar var a end metavar end quote pair one pair true seed one end parameter with parameter term quote two plus metavar var b end metavar end quote stack quote metavar var b end metavar end quote pair two pair true seed one end parameter substitution true end unify assoc two end assoc term equal quote three end quote end test end math
end "}
\test{"
begin math test instantiate parameter term quote metavar var a end metavar plus metavar var b end metavar end quote stack quote metavar var a end metavar end quote pair one pair quote metavar var b end metavar end quote pair two pair true seed one end parameter with unify parameter term quote metavar var a end metavar plus three end quote stack quote metavar var a end metavar end quote pair one pair true seed one end parameter with parameter term quote two plus metavar var b end metavar end quote stack quote metavar var b end metavar end quote pair two pair true seed one end parameter substitution true end unify end instantiate term equal quote two plus three end quote end test end math
end "}
\subsection{Proof generation}\label{section:ProofGeneration}
\subsubsection{Example lemmas}
As examples of sequent proofs, we prove two lemmas in the example theory "
begin bracket example theory end bracket
end ":
%
\index{reflexivity lemma "
begin bracket reflexivity lemma end bracket
end "}%
%
\index{Reflexivity @\back "
begin bracket reflexivity lemma end bracket
end " reflexivity lemma}%
%
\tex{"
begin math define tex of reflexivity lemma as text "
Reflexivity" end text end define end math
end "}%
%
\statement{"
begin math define statement of reflexivity lemma as example theory infer all metavar var a end metavar indeed metavar var a end metavar math equal metavar var a end metavar end define end math
end "%
%
\footnote{"
begin math define pyk of reflexivity lemma as text "reflexivity lemma" end text end define end math
end "}}
%
\statement{"
begin math define proof of reflexivity lemma as quote example theory infer all metavar var a end metavar indeed example scheme lemma init modus dereference modus at metavar var a end metavar at metavar var a end metavar cut example rule lemma init modus dereference modus at metavar var a end metavar pair metavar var a end metavar head at metavar var a end metavar at metavar var a end metavar modus modus end quote end define end math
end "}
%
\index{commutativity lemma "
begin bracket commutativity lemma end bracket
end "}%
%
\index{Commutativity @\back "
begin bracket commutativity lemma end bracket
end " commutativity lemma}%
%
\tex{"
begin math define tex of commutativity lemma as text "
Commutativity" end text end define end math
end "}%
%
\statement{"
begin math define statement of commutativity lemma as example theory infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar math equal metavar var b end metavar infer metavar var b end metavar math equal metavar var a end metavar end define end math
end "%
%
\footnote{"
begin math define pyk of commutativity lemma as text "commutativity lemma" end text end define end math
end "}}
%
\statement{"
begin math define proof of commutativity lemma as quote example theory infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar math equal metavar var b end metavar infer reflexivity lemma init modus dereference modus at metavar var a end metavar cut example rule lemma init modus dereference modus at metavar var a end metavar at metavar var b end metavar at metavar var a end metavar modus modus end quote end define end math
end "}
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 "
begin bracket reflexivity lemma one end bracket
end "}%
%
\index{Reflexivity @\back "
begin bracket reflexivity lemma one end bracket
end " reflexivity lemma one}%
%
\tex{"
begin math define tex of reflexivity lemma one as text "
Reflexivity_1" end text end define end math
end "}%
%
\statement{"
begin math define statement of reflexivity lemma one as example theory infer all metavar var a end metavar indeed metavar var a end metavar math equal metavar var a end metavar end define end math
end "%
%
\footnote{"
begin math define pyk of reflexivity lemma one as text "reflexivity lemma one" end text end define end math
end "}}
%
\statement{"
begin math define proof of reflexivity lemma one as lambda var c dot lambda var x dot proof expand quote example theory infer all metavar var a end metavar indeed example scheme lemma conclude metavar var a end metavar pair metavar var a end metavar head math equal metavar var a end metavar cut example rule lemma modus ponens metavar var a end metavar pair metavar var a end metavar head math equal metavar var a end metavar modus ponens metavar var a end metavar pair metavar var a end metavar head math equal metavar var a end metavar conclude metavar var a end metavar math equal metavar var a end metavar end quote state proof state cache var c end expand end define end math
end "}
\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 "
begin bracket the tactic aspect end bracket
end " aspect self-evaluating and use "
begin bracket tactic end bracket
end " to denote it:
%
\index{tactic @\back "
begin bracket the tactic aspect end bracket
end " the tactic aspect}%
%
\index{the tactic aspect "
begin bracket the tactic aspect end bracket
end "}%
%
\tex{"
begin math define tex of the tactic aspect as text "
{<}tactic{>}" end text end define end math
end "}%
%
\display{"
begin math define value of the tactic aspect as quote the tactic aspect end quote end define end math
end "%
%
\footnote{"
begin math define pyk of the tactic aspect as text "the tactic aspect" end text end define end math
end "}}
%
%
\index{tactic "
begin bracket tactic end bracket
end "}%
%
\tex{"
begin math define tex of tactic as text "
tactic" end text end define end math
end "}%
%
\display{"
begin math define message of tactic as the tactic aspect end define end math
end "%
%
\footnote{"
begin math define pyk of tactic as text "tactic" end text end define end math
end "}}
%
For convenience, we define a construct for making tactic definitions:
\index{tactic define x as y end define "
begin math define tactic of var x as var y end define end math
end "}%
%
\index{tactic: "
begin math define tactic of var x as var y end define end math
end "}%
%
\tex{"
begin math define tex of tactic define var x as var y end define as text "
[#1/tex name/tex.
\stackrel {tactic}{=}#2.
]" end text end define end math
end "}%
%
\display{%
"
begin math define macro of tactic 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 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 quote end define end define end math
end "%
%
\footnote{"
begin math define pyk of tactic define var x as var y end define as text "tactic define * as * end define" end text end define end math
end "}}
\subsubsection{The proof expander}
The proof expander "
begin bracket proof expand var t state var s cache var c end expand end bracket
end " proof expands the term "
begin bracket var t end bracket
end " for the \indexintro{proof state} "
begin bracket var s end bracket
end " and the cache "
begin bracket var c end bracket
end " and returns the result as a semitagged map. The untagged version "
begin bracket map untag proof expand var t state var s cache var c end expand end untag end bracket
end " is the expansion itself.
The proof expander "
begin bracket proof expand var t state var s cache var c end expand end bracket
end " differs from the macro expander "
begin bracket expand var t state var s cache var c end expand end bracket
end " in that it has no special treatment for page symbols and in that it uses the "
begin bracket tactic end bracket
end " aspect instead of the "
begin bracket macro end bracket
end " 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 "
begin bracket proof expand var t state var s cache var c end expand end bracket
end " is almost identical to that of "
begin bracket expand var t state var s cache var c end expand end bracket
end ". 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 "
begin bracket proof expand var t state var s cache var c end expand end bracket
end " reads:
%
\index{p: "
begin bracket proof expand var x state var y cache var z end expand end bracket
end " proof expand x state y cache z end expand}%
%
\tex{"
begin math define tex of proof expand var t state var s cache var c end expand as text "
{\cal P}( #1.
, #2.
, #3.
)" end text end define end math
end "}%
%
\display{"
begin math define value of proof expand var t state var s cache var c end expand as var s tagged guard newline let one lambda var d dot newline tagged 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 if apply aspect the tactic aspect term var t cache var c end aspect end let end define end math
end "%
%
\footnote{"
begin math define pyk of proof expand var t state var s cache var c end expand as text "proof expand * state * cache * end expand" end text end define end math
end "}}
%
%
\index{p: "
begin bracket proof expand list var x state var y cache var z end expand end bracket
end " proof expand list x state y cache z end expand}%
%
\tex{"
begin math define tex of proof expand list var t state var s cache var c end expand as text "
{\cal P}^*( #1.
, #2.
, #3.
)" end text end define end math
end "}%
%
\display{"
begin math define value of 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
end "%
%
\footnote{"
begin math define pyk of proof expand list var t state var s cache var c end expand as text "proof expand list * state * cache * end expand" end text end define end math
end "}}
%
\subsubsection{The initial proof state}
Proof states have exactly the same format as macro states.
The \index{proof state, initial}\indexintro{initial proof state} "
begin bracket proof state end bracket
end " is useful for passing as the second parameter to "
begin bracket proof expand var t state var s cache var c end expand end bracket
end ". "
begin bracket proof state end bracket
end " is a pair whose head is the proof expander itself and whose tail is left blank. The definition of "
begin bracket proof state end bracket
end " reads:
%
\index{p: "
begin bracket proof state end bracket
end " proof state}%
%
\tex{"
begin math define tex of proof state as text "
p_0" end text end define end math
end "}%
%
\display{"
begin 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
end "%
%
\footnote{"
begin math define pyk of proof state as text "proof state" end text end define end math
end "}}
%
The function "
begin bracket state expand var t state var s cache var c end expand end bracket
end " defined previously macro expands the term "
begin bracket var t end bracket
end " using the macro expander embedded in the macro state "
begin bracket var s end bracket
end " using the cache "
begin bracket var c end bracket
end ". Since proof states have exactly the same syntax and semantics as macro states, we shall take the liberty to use "
begin bracket state expand var t state var s cache var c end expand end bracket
end " for proof states also.
\subsubsection{The conclusion tactic}
The \index{tactic, conclusion}\indexintro{conclusion tactic} "
begin bracket var x conclude var y end bracket
end " constructs a proof of "
begin bracket var y end bracket
end " from the partial proof "
begin bracket var x end bracket
end ". The conclusion tactic does the following to the proof "
begin bracket var x end bracket
end ":
\begin{itemize}
\item Whenever "
begin bracket var x end bracket
end " references a lemma "
begin bracket var l end bracket
end ", the conclusion tactic replaces "
begin bracket var l end bracket
end " by "
begin bracket var l init modus dereference modus end bracket
end ".
\item Whenever a subproof "
begin bracket var u end bracket
end " of "
begin bracket var x end bracket
end " proves "
begin bracket all var v indeed var w end bracket
end ", the conclusion tactic replaces "
begin bracket var u end bracket
end " by "
begin bracket var u at var a end bracket
end " where the tactic uses unification to guess "
begin bracket var a end bracket
end ".
\item Whenever a subproof "
begin bracket var u end bracket
end " of "
begin bracket var x end bracket
end " proves "
begin bracket var v endorse var w end bracket
end ", the conclusion tactic replaces "
begin bracket var u end bracket
end " by "
begin bracket var u verify end bracket
end ".
\end{itemize}
%
\index{\alpha x conclude y @\back "
begin bracket var x conclude var y end bracket
end " x conclude y}%
%
\tex{"
begin math define tex of var x conclude var y as text "#1.
\gg #2." end text end define end math
end "}%
%
\display{"
begin math define tactic of 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
end "%
%
\footnote{"
begin math define pyk of var x conclude var y as text "* conclude *" end text end define end math
end "}}
%
%
\index{conclude @\back "
begin bracket conclude one var x cache var y end conclude end bracket
end " conclude one x cache y end conclude}%
%
\tex{"
begin math define tex of conclude one var t cache var c end conclude as text "
conclude_1 ( #1.
, #2.
)" end text end define end math
end "}%
%
\display{"
begin math define value of conclude one var t cache var c end conclude as newline let one lambda var r dot newline tagged if var r is cardinal then error two quote "Unification failed" end quote term var t end error else var r end if apply conclude two var t first proves var t second cache var c end conclude end let end define end math
end "%
%
\footnote{"
begin math define pyk of conclude one var t cache var c end conclude as text "conclude one * cache * end conclude" end text end define end math
end "}}
%
%
\index{conclude @\back "
begin bracket conclude two var x proves var y cache var z end conclude end bracket
end " conclude two x proves y cache z end conclude}%
%
\tex{"
begin math define tex of conclude two var a proves var t cache var c end conclude as text "
conclude_2 ( #1.
, #2.
, #3.
)" end text end define end math
end "}%
%
\display{"
begin math define value of conclude two var a proves var t cache var c end conclude as var t tagged guard newline tagged 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 tagged 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 tagged 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 tagged if aspect the proof aspect term var a cache var c end aspect then error two quote "Lemma expected" end quote term var a end error else newline let one lambda var d dot 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 apply aspect the statement aspect term var a cache var c end aspect end let end if end if end if end if end define end math
end "%
%
\footnote{"
begin math define pyk of conclude two var a proves var t cache var c end conclude as text "conclude two * proves * cache * end conclude" end text end define end math
end "}}
%
%
\index{conclude @\back "
begin bracket conclude three var x proves var y lemma var z substitution var a end conclude end bracket
end " conclude three x proves y lemma z substitution a end conclude}%
%
\tex{"
begin math define tex of conclude three var a proves var t lemma var l substitution var s end conclude as text "
conclude_3 ( #1.
, #2.
, #3.
, #4.
)" end text end define end math
end "}%
%
\display{"
begin math define value of 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 tagged 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 a modus 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 modus proves var t lemma var l second substitution var s end conclude end select else newline tagged 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 a modus 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 modus proves var t lemma var l second substitution var s end conclude end select else newline tagged 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 a at var t second 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 at var l first proves var t lemma var l second substitution var s end conclude end select else newline let one lambda var s dot newline tagged if var s is cardinal then var s else newline instantiate var a with var s end instantiate end if apply unify var l with var t substitution var s end unify end let end if end if end if end define end math
end "%
%
\footnote{"
begin math define pyk of conclude three var a proves var t lemma var l substitution var s end conclude as text "conclude three * proves * lemma * substitution * end conclude" end text end define end math
end "}}
%
Modus ponens:
%
\index{\alpha x modus ponens y @\back "
begin bracket var x modus ponens var y end bracket
end " x modus ponens y}%
%
\tex{"
begin math define tex of var x modus ponens var y as text "#1.
\rhd #2." end text end define end math
end "}%
%
\display{"
begin math define value of var x modus ponens var y as quote var x modus ponens var y end quote root pair var x pair var y pair true end define end math
end "%
%
\footnote{"
begin math define pyk of var x modus ponens var y as text "* modus ponens *" end text end define end math
end "}}
%
Modus probans:
%
\index{\alpha x modus probans y @\back "
begin bracket var x modus probans var y end bracket
end " x modus probans y}%
%
\tex{"
begin math define tex of var x modus probans var y as text "#1.
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} #2." end text end define end math
end "}%
%
\display{"
begin math define value of var x modus probans var y as quote var x modus probans var y end quote root pair var x pair var y pair true end define end math
end "%
%
\footnote{"
begin math define pyk of var x modus probans var y as text "* modus probans *" end text end define end math
end "}}
%
\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 "
begin bracket text define proof of var y as lambda var c dot lambda var x dot proof expand quote var x infer var z end quote state proof state cache var c end expand end define end text end bracket
end " x proof of y reads z}%
%
\index{proof: "
begin bracket text define proof of var y as lambda var c dot lambda var x dot proof expand quote var x infer var z end quote state proof state cache var c end expand end define end text end bracket
end " x proof of y reads z}%
%
\tex{"
begin math define tex of var t proof of var s reads var p as text "
\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 text end define end math
end "}%
%
\tex{"
begin math define tex name of var t proof of var s reads var p as text "#1.
\mathbf{\ proof\ of\ } #2.
: #3." end text end define end math
end "}
%
\display{"
begin math define macro of var t proof of var s reads 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 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 quote end define end define end math
end "%
%
\footnote{"
begin math define pyk of var t proof of var l reads var p as text "* proof of * reads *" end text end define end math
end "}}
%
%
\index{Line @\back "
begin bracket text var y conclude var z cut var a end text end bracket
end " line x because y indeed z cut a}%
%
\index{line x because y indeed z cut a "
begin bracket text var y conclude var z cut var a end text end bracket
end "}%
%
\tex{"
begin math define tex of line var l because var a indeed var i cut 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]{$#1.
$:}$#2.
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$#3.
$\hfill \makebox [0mm][l]{\quad ;}}#4." end text end define end math
end "}%
%
\tex{"
begin math define tex name of line var l because var a indeed var i cut var p as text "
Line \, #1.
: #2.
\gg #3.
; #4." end text end define end math
end "}%
%
\display{"
begin math define macro of line var l because var a indeed var i cut 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 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 quote end define end define end math
end "%
%
\footnote{"
begin math define pyk of line var l because var a indeed var i cut var p as text "line * because * indeed * cut *" end text end define end math
end "}}
%
%
\index{Last line @\back "
begin bracket text var x conclude var y end text end bracket
end " because x indeed y qed}%
%
\index{because x indeed y qed "
begin bracket text var x conclude var y end text end bracket
end "}%
%
\tex{"
begin math define tex of because var a indeed var i qed 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 \makebox[0mm]{$\Box$}}}" end text end define end math
end "}%
%
\tex{"
begin math define tex name of because var a indeed var i qed as text "
Last\ line \, #1.
\gg #2." end text end define end math
end "}%
%
\display{"
begin math define macro of because var a indeed var i qed 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 qed as parenthesis var a conclude var i end parenthesis end define end quote end define end define end math
end "%
%
\footnote{"
begin math define pyk of because var a indeed var i qed as text "because * indeed * qed" end text end define end math
end "}}
%
%
\index{premise @\back "
begin bracket text var y infer var z end text end bracket
end " line x premise y cut z}%
%
\index{line x premise y cut z "
begin bracket text var y infer var z end text end bracket
end "}%
%
\tex{"
begin math define tex of line var l premise var i cut var p as text "
\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 text end define end math
end "}%
%
\tex{"
begin math define tex name of line var l premise var i cut var p as text "
Line \, #1.
: Premise \gg #2.
;#3." end text end define end math
end "}%
%
\display{"
begin math define macro of line var l premise var i cut 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 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 quote end define end define end math
end "%
%
\footnote{"
begin math define pyk of line var l premise var i cut var p as text "line * premise * cut *" end text end define end math
end "}}
%
%
\index{side condition @\back "
begin bracket text var y endorse var z end text end bracket
end " line x side condition y cut z}%
%
\index{line x side condition y cut z "
begin bracket text var y endorse var z end text end bracket
end "}%
%
\tex{"
begin math define tex of line var l side condition var i cut var p as text "
\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 text end define end math
end "}%
%
\tex{"
begin math define tex name of line var l side condition var i cut var p as text "
Line \, #1.
: \mbox{Side-condition} \gg #2.
; #3." end text end define end math
end "}%
%
\display{"
begin math define macro of line var l side condition var i cut 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 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 quote end define end define end math
end "%
%
\footnote{"
begin math define pyk of line var l side condition var i cut var p as text "line * side condition * cut *" end text end define end math
end "}}
%
%
\index{arbitrary @\back "
begin bracket text all var y indeed var z end text end bracket
end " arbitrary x cut y}%
%
\index{arbitrary x cut y "
begin bracket text all var x indeed var y end text end bracket
end "}%
%
\tex{"
begin math define tex of arbitrary var i cut 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 "}%
%
\tex{"
begin math define tex name of arbitrary var i cut var p as text "
Arbitrary \gg #1.
;#2." end text end define end math
end "}%
%
\display{"
begin math define macro of arbitrary var i cut 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 arbitrary var i cut var p as parenthesis all var i indeed var p end parenthesis end define end quote end define end define end math
end "%
%
\footnote{"
begin math define pyk of arbitrary var i cut var p as text "arbitrary * cut *" end text end define end math
end "}}
%
%
\index{local @\back "
begin bracket text var z end text end bracket
end " locally define x as y cut z}%
%
\index{locally define x as y cut z "
begin bracket text var z end text end bracket
end "}%
%
\tex{"
begin math define tex of locally define var a as var i cut var p as text "
\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 text end define end math
end "}%
%
\tex{"
begin math define tex name of locally define var a as var i cut var p as text "
Local \gg #1.
= #2.
; #3." end text end define end math
end "}%
%
\display{"
begin math define macro of locally define var a as var i cut 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 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 quote end define end define end math
end "%
%
\footnote{"
begin math define pyk of locally define var u as var v cut var p as text "locally define * as * cut *" end text end define end math
end "}}
%
\appendix
\section{Chores}
The name of the page:
\display{"
begin math define pyk of check as text "check" end text end define end math
end "}
\test{"
begin math test true end test end math
end "}
\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}
"
begin math define pyk of ell a as text "ell a" end text end define end math
end "
"
begin math define pyk of ell b as text "ell b" end text end define end math
end "
"
begin math define pyk of ell c as text "ell c" end text end define end math
end "
"
begin math define pyk of ell d as text "ell d" end text end define end math
end "
"
begin math define pyk of ell e as text "ell e" end text end define end math
end "
"
begin math define pyk of ell f as text "ell f" end text end define end math
end "
"
begin math define pyk of ell g as text "ell g" end text end define end math
end "
"
begin math define pyk of ell h as text "ell h" end text end define end math
end "
"
begin math define pyk of ell i as text "ell i" end text end define end math
end "
"
begin math define pyk of ell j as text "ell j" end text end define end math
end "
"
begin math define pyk of ell k as text "ell k" end text end define end math
end "
"
begin math define pyk of ell l as text "ell l" end text end define end math
end "
"
begin math define pyk of ell m as text "ell m" end text end define end math
end "
"
begin math define pyk of ell n as text "ell n" end text end define end math
end "
"
begin math define pyk of ell o as text "ell o" end text end define end math
end "
"
begin math define pyk of ell p as text "ell p" end text end define end math
end "
"
begin math define pyk of ell q as text "ell q" end text end define end math
end "
"
begin math define pyk of ell r as text "ell r" end text end define end math
end "
"
begin math define pyk of ell s as text "ell s" end text end define end math
end "
"
begin math define pyk of ell t as text "ell t" end text end define end math
end "
"
begin math define pyk of ell u as text "ell u" end text end define end math
end "
"
begin math define pyk of ell v as text "ell v" end text end define end math
end "
"
begin math define pyk of ell w as text "ell w" end text end define end math
end "
"
begin math define pyk of ell x as text "ell x" end text end define end math
end "
"
begin math define pyk of ell y as text "ell y" end text end define end math
end "
"
begin math define pyk of ell z as text "ell z" end text end define end math
end "
"
begin math define pyk of ell big a as text "ell big a" end text end define end math
end "
"
begin math define pyk of ell big b as text "ell big b" end text end define end math
end "
"
begin math define pyk of ell big c as text "ell big c" end text end define end math
end "
"
begin math define pyk of ell big d as text "ell big d" end text end define end math
end "
"
begin math define pyk of ell big e as text "ell big e" end text end define end math
end "
"
begin math define pyk of ell big f as text "ell big f" end text end define end math
end "
"
begin math define pyk of ell big g as text "ell big g" end text end define end math
end "
"
begin math define pyk of ell big h as text "ell big h" end text end define end math
end "
"
begin math define pyk of ell big i as text "ell big i" end text end define end math
end "
"
begin math define pyk of ell big j as text "ell big j" end text end define end math
end "
"
begin math define pyk of ell big k as text "ell big k" end text end define end math
end "
"
begin math define pyk of ell big l as text "ell big l" end text end define end math
end "
"
begin math define pyk of ell big m as text "ell big m" end text end define end math
end "
"
begin math define pyk of ell big n as text "ell big n" end text end define end math
end "
"
begin math define pyk of ell big o as text "ell big o" end text end define end math
end "
"
begin math define pyk of ell big p as text "ell big p" end text end define end math
end "
"
begin math define pyk of ell big q as text "ell big q" end text end define end math
end "
"
begin math define pyk of ell big r as text "ell big r" end text end define end math
end "
"
begin math define pyk of ell big s as text "ell big s" end text end define end math
end "
"
begin math define pyk of ell big t as text "ell big t" end text end define end math
end "
"
begin math define pyk of ell big u as text "ell big u" end text end define end math
end "
"
begin math define pyk of ell big v as text "ell big v" end text end define end math
end "
"
begin math define pyk of ell big w as text "ell big w" end text end define end math
end "
"
begin math define pyk of ell big x as text "ell big x" end text end define end math
end "
"
begin math define pyk of ell big y as text "ell big y" end text end define end math
end "
"
begin math define pyk of ell big z as text "ell big z" end text end define end math
end "
"
begin math define pyk of ell dummy as text "ell dummy" end text end define end math
end "
"
begin math define tex name of ell a as text "L_a" end text end define end math
end "
"
begin math define tex name of ell b as text "L_b" end text end define end math
end "
"
begin math define tex name of ell c as text "L_c" end text end define end math
end "
"
begin math define tex name of ell d as text "L_d" end text end define end math
end "
"
begin math define tex name of ell e as text "L_e" end text end define end math
end "
"
begin math define tex name of ell f as text "L_f" end text end define end math
end "
"
begin math define tex name of ell g as text "L_g" end text end define end math
end "
"
begin math define tex name of ell h as text "L_h" end text end define end math
end "
"
begin math define tex name of ell i as text "L_i" end text end define end math
end "
"
begin math define tex name of ell j as text "L_j" end text end define end math
end "
"
begin math define tex name of ell k as text "L_k" end text end define end math
end "
"
begin math define tex name of ell l as text "L_l" end text end define end math
end "
"
begin math define tex name of ell m as text "L_m" end text end define end math
end "
"
begin math define tex name of ell n as text "L_n" end text end define end math
end "
"
begin math define tex name of ell o as text "L_o" end text end define end math
end "
"
begin math define tex name of ell p as text "L_p" end text end define end math
end "
"
begin math define tex name of ell q as text "L_q" end text end define end math
end "
"
begin math define tex name of ell r as text "L_r" end text end define end math
end "
"
begin math define tex name of ell s as text "L_s" end text end define end math
end "
"
begin math define tex name of ell t as text "L_t" end text end define end math
end "
"
begin math define tex name of ell u as text "L_u" end text end define end math
end "
"
begin math define tex name of ell v as text "L_v" end text end define end math
end "
"
begin math define tex name of ell w as text "L_w" end text end define end math
end "
"
begin math define tex name of ell x as text "L_x" end text end define end math
end "
"
begin math define tex name of ell y as text "L_y" end text end define end math
end "
"
begin math define tex name of ell z as text "L_z" end text end define end math
end "
"
begin math define tex name of ell big a as text "L_A" end text end define end math
end "
"
begin math define tex name of ell big b as text "L_B" end text end define end math
end "
"
begin math define tex name of ell big c as text "L_C" end text end define end math
end "
"
begin math define tex name of ell big d as text "L_D" end text end define end math
end "
"
begin math define tex name of ell big e as text "L_E" end text end define end math
end "
"
begin math define tex name of ell big f as text "L_F" end text end define end math
end "
"
begin math define tex name of ell big g as text "L_G" end text end define end math
end "
"
begin math define tex name of ell big h as text "L_H" end text end define end math
end "
"
begin math define tex name of ell big i as text "L_I" end text end define end math
end "
"
begin math define tex name of ell big j as text "L_J" end text end define end math
end "
"
begin math define tex name of ell big k as text "L_K" end text end define end math
end "
"
begin math define tex name of ell big l as text "L_L" end text end define end math
end "
"
begin math define tex name of ell big m as text "L_M" end text end define end math
end "
"
begin math define tex name of ell big n as text "L_N" end text end define end math
end "
"
begin math define tex name of ell big o as text "L_O" end text end define end math
end "
"
begin math define tex name of ell big p as text "L_P" end text end define end math
end "
"
begin math define tex name of ell big q as text "L_Q" end text end define end math
end "
"
begin math define tex name of ell big r as text "L_R" end text end define end math
end "
"
begin math define tex name of ell big s as text "L_S" end text end define end math
end "
"
begin math define tex name of ell big t as text "L_T" end text end define end math
end "
"
begin math define tex name of ell big u as text "L_U" end text end define end math
end "
"
begin math define tex name of ell big v as text "L_V" end text end define end math
end "
"
begin math define tex name of ell big w as text "L_W" end text end define end math
end "
"
begin math define tex name of ell big x as text "L_X" end text end define end math
end "
"
begin math define tex name of ell big y as text "L_Y" end text end define end math
end "
"
begin math define tex name of ell big z as text "L_Z" end text end define end math
end "
"
begin math define tex name of ell dummy as text "L_?" end text end define end math
end "
\end{flushleft}
"
begin math define tex of ell a as text "
\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 text end define end math
end "
"
begin math define tex of ell b as text "
\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 text end define end math
end "
"
begin math define tex of ell c as text "
\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 text end define end math
end "
"
begin math define tex of ell d as text "
\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 text end define end math
end "
"
begin math define tex of ell e as text "
\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 text end define end math
end "
"
begin math define tex of ell f as text "
\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 text end define end math
end "
"
begin math define tex of ell g as text "
\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 text end define end math
end "
"
begin math define tex of ell h as text "
\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 text end define end math
end "
"
begin math define tex of ell i as text "
\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 text end define end math
end "
"
begin math define tex of ell j as text "
\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 text end define end math
end "
"
begin math define tex of ell k as text "
\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 text end define end math
end "
"
begin math define tex of ell l as text "
\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 text end define end math
end "
"
begin math define tex of ell m as text "
\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 text end define end math
end "
"
begin math define tex of ell n as text "
\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 text end define end math
end "
"
begin math define tex of ell o as text "
\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 text end define end math
end "
"
begin math define tex of ell p as text "
\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 text end define end math
end "
"
begin math define tex of ell q as text "
\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 text end define end math
end "
"
begin math define tex of ell r as text "
\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 text end define end math
end "
"
begin math define tex of ell s as text "
\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 text end define end math
end "
"
begin math define tex of ell t as text "
\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 text end define end math
end "
"
begin math define tex of ell u as text "
\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 text end define end math
end "
"
begin math define tex of ell v as text "
\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 text end define end math
end "
"
begin math define tex of ell w as text "
\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 text end define end math
end "
"
begin math define tex of ell x as text "
\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 text end define end math
end "
"
begin math define tex of ell y as text "
\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 text end define end math
end "
"
begin math define tex of ell z as text "
\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 text end define end math
end "
"
begin math define tex of ell big a as text "
\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 text end define end math
end "
"
begin math define tex of ell big b as text "
\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 text end define end math
end "
"
begin math define tex of ell big c as text "
\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 text end define end math
end "
"
begin math define tex of ell big d as text "
\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 text end define end math
end "
"
begin math define tex of ell big e as text "
\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 text end define end math
end "
"
begin math define tex of ell big f as text "
\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 text end define end math
end "
"
begin math define tex of ell big g as text "
\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 text end define end math
end "
"
begin math define tex of ell big h as text "
\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 text end define end math
end "
"
begin math define tex of ell big i as text "
\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 text end define end math
end "
"
begin math define tex of ell big j as text "
\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 text end define end math
end "
"
begin math define tex of ell big k as text "
\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 text end define end math
end "
"
begin math define tex of ell big l as text "
\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 text end define end math
end "
"
begin math define tex of ell big m as text "
\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 text end define end math
end "
"
begin math define tex of ell big n as text "
\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 text end define end math
end "
"
begin math define tex of ell big o as text "
\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 text end define end math
end "
"
begin math define tex of ell big p as text "
\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 text end define end math
end "
"
begin math define tex of ell big q as text "
\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 text end define end math
end "
"
begin math define tex of ell big r as text "
\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 text end define end math
end "
"
begin math define tex of ell big s as text "
\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 text end define end math
end "
"
begin math define tex of ell big t as text "
\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 text end define end math
end "
"
begin math define tex of ell big u as text "
\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 text end define end math
end "
"
begin math define tex of ell big v as text "
\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 text end define end math
end "
"
begin math define tex of ell big w as text "
\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 text end define end math
end "
"
begin math define tex of ell big x as text "
\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 text end define end math
end "
"
begin math define tex of ell big y as text "
\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 text end define end math
end "
"
begin math define tex of ell big z as text "
\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 text end define end math
end "
"
begin math define tex of ell dummy as text "
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi " end text end define end math
end "
\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}
"
begin flush left math define priority of check as preassociative priority check equal priority base equal priority bracket x end bracket equal priority big bracket x end bracket equal priority math x end math equal priority flush left x end left equal priority var x equal priority var y equal priority var z equal priority proclaim x as x end proclaim equal priority define x of x as x end define equal priority pyk equal priority tex equal priority tex name equal priority priority equal priority x equal priority true equal priority if x then x else x end if equal priority introduce x of x as x end introduce equal priority value equal priority claim equal priority bottom equal priority function f of x end function equal priority identity x end identity equal priority false equal priority untagged zero equal priority untagged one equal priority untagged two equal priority untagged three equal priority untagged four equal priority untagged five equal priority untagged six equal priority untagged seven equal priority untagged eight equal priority untagged nine equal priority zero equal priority one equal priority two equal priority three equal priority four equal priority five equal priority six equal priority seven equal priority eight equal priority nine equal priority var a equal priority var b equal priority var c equal priority var d equal priority var e equal priority var f equal priority var g equal priority var h equal priority var i equal priority var j equal priority var k equal priority var l equal priority var m equal priority var n equal priority var o equal priority var p equal priority var q equal priority var r equal priority var s equal priority var t equal priority var u equal priority var v equal priority var w equal priority tagged parenthesis x end tagged equal priority tagged if x then x else x end if equal priority array x is x end array equal priority left equal priority center equal priority right equal priority empty equal priority substitute x set x to x end substitute equal priority map tag x end tag equal priority raw map untag x end untag equal priority map untag x end untag equal priority normalizing untag x end untag equal priority apply x to x end apply equal priority apply one x to x end apply equal priority identifier x end identifier equal priority identifier one x plus id x end identifier equal priority array plus x and x end plus equal priority array remove x array x level x end remove equal priority array put x value x array x level x end put equal priority array add x value x index x value x level x end add equal priority bit x of x end bit equal priority bit one x of x end bit equal priority example rack equal priority vector hook equal priority bibliography hook equal priority dictionary hook equal priority body hook equal priority codex hook equal priority expansion hook equal priority code hook equal priority cache hook equal priority diagnose hook equal priority pyk aspect equal priority tex aspect equal priority texname aspect equal priority value aspect equal priority message aspect equal priority macro aspect equal priority definition aspect equal priority unpack aspect equal priority claim aspect equal priority priority aspect equal priority lambda identifier equal priority apply identifier equal priority true identifier equal priority if identifier equal priority quote identifier equal priority proclaim identifier equal priority define identifier equal priority introduce identifier equal priority hide identifier equal priority pre identifier equal priority post identifier equal priority eval x stack x cache x end eval equal priority eval two x ref x id x stack x cache x end eval equal priority eval three x function x stack x cache x end eval equal priority eval four x arguments x stack x cache x end eval equal priority lookup x stack x default x end lookup equal priority abstract x term x stack x cache x end abstract equal priority quote x end quote equal priority expand x state x cache x end expand equal priority expand two x definition x state x cache x end expand equal priority expand list x state x cache x end expand equal priority macro equal priority macro state equal priority zip x with x end zip equal priority assoc one x address x index x end assoc equal priority protect x end protect equal priority self equal priority macro define x as x end define equal priority value define x as x end define equal priority intro define x as x end define equal priority pyk define x as x end define equal priority tex define x as x end define equal priority tex name define x as x end define equal priority priority table x end table equal priority macro define one equal priority macro define two x end define equal priority macro define three x end define equal priority macro define four x state x cache x definition x end define equal priority state expand x state x cache x end expand equal priority quote expand x term x stack x end expand equal priority quote expand two x term x stack x end expand equal priority quote expand three x term x stack x value x end expand equal priority quote expand star x term x stack x end expand equal priority parenthesis x end parenthesis equal priority 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 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 color x term x end color equal priority color star x term x end color equal priority vars x end vars equal priority vars star x end vars equal priority instantiate x color x term x end instantiate equal priority instantiate star x color x term x end instantiate equal priority unify x term x with x term x plus x end unify equal priority unify star x term x with x term x plus x end unify equal priority unify one x term x with x term x plus x end unify equal priority unify two x plus x end unify equal priority unify three x vars x plus x end unify 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 end occur equal priority occur star x in x end occur equal priority circular x term x substitution x end circular equal priority circular star x term x substitution x end circular 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 reflexivity lemma equal priority reflexivity lemma one equal priority commutativity lemma 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 end priority greater than preassociative priority x sub x end sub 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 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 end priority greater than preassociative 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 end priority greater than preassociative priority x apply x equal priority x tagged apply x end priority greater than preassociative 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 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 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 postassociative priority x macro imply x end priority greater than postassociative priority x guard 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 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 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 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 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 cut x equal priority because x indeed x qed equal priority line x premise x cut x equal priority line x side condition x cut x equal priority arbitrary x cut x equal priority locally define x as x cut 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 end priority greater than preassociative priority x row
x end priority greater than unicode end of text end define end math end left
end "
\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"
The pyk compiler, version 0.grue.20050502+ by Klaus Grue,