Logiweb(TM)

Logiweb body of check in pyk

Up Help

text "page.html" : "<head>
<title>
A Logiweb proof checker
</title>
</head>

<body>
<h2>
A Logiweb proof checker
</h2>

<p>
<a href='../index.html'>Up</a>
</p>

<p>

Contents:
<a href='page.pdf'>Main text</a>
<a href='chores.pdf'>Chores</a>
</p>

<p><address>Klaus Grue</address></p>
</body>
" end text ,, text "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}}

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

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

@techreport{chores,
author = {K. Grue},
year = {2006},
title = {A Logiweb proof checker - chores},
institution={Logiweb},
note = {\href{\lgwrelay 64/\lgwThisBlockBaseSixtyFour /2/body/tex/chores.pdf}{\lgwBreakRelay 64/\lgwThisBreakBaseSixtyFour /2/body/tex/chores.pdf}}}

@techreport{base,
author = {K. Grue},
year = {2006},
title = {A Logiweb base page},
institution={Logiweb},
note = {\href{\lgwrelay 64/\lgwBaseBlockBaseSixtyFour /2/body/tex/page.html}{\lgwBreakRelay 64/\lgwBaseBreakBaseSixtyFour /2/body/tex/page.html}}}

" end text ,, text "page.tex" : "\documentclass[fleqn]{article}

% Include definitions generated by pyk
\input{lgwinclude}

% Make latexsym characters available
\usepackage{latexsym}

% Ensure reasonable rendering of strings
\everymath{\rm}
\everydisplay{\rm}

% Enable generation of an index
\usepackage{makeidx}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}

% Enable generation of a bibliography
\bibliographystyle{plain}

% Enable hyperlinks
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle=A Logiweb proof checker}
\hypersetup{colorlinks=true}

% Construct for listing statements with associated explanations
\newenvironment{statements}{\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}}{\end{list}}

\begin{document}
\title{A Logiweb proof checker}
\author{Klaus Grue}
\maketitle
\tableofcontents

"[ make macro expanded version ragged right ]"
"[ prepare proof indentation ]"



\section{Introduction}

\indexintro{Logiweb} \cite{Logiweb} is an open source system available under GNU GPL for distribution of mathematical definitions, lemmas, and proofs.

The present document is part of a \index{page, Logiweb}\indexintro{Logiweb page}. A Logiweb page is a cluster of documents which has been submitted to the Logiweb system. Such a cluster typically consists of a main document like the present one plus a number of electronic appendices.

The present Logiweb page (i.e.\ the document cluster to which the present document belongs) defines a general purpose proof checker.



\subsection{Electronic appendices}

The present Logiweb page comprises one html and two PDF files, located the following places:

\begin{itemize}
\item \href{\lgwrelay 64/\lgwThisBlockBaseSixtyFour /2/body/tex/page.pdf}{\lgwBreakRelay 64/\lgwThisBreakBaseSixtyFour /2/body/tex/page.pdf}
\item \href{\lgwrelay 64/\lgwThisBlockBaseSixtyFour /2/body/tex/chores.pdf}{\lgwBreakRelay 64/\lgwThisBreakBaseSixtyFour /2/body/tex/chores.pdf} \cite{chores}
\item \href{\lgwrelay 64/\lgwThisBlockBaseSixtyFour /2/body/tex/page.html}{\lgwBreakRelay 64/\lgwThisBreakBaseSixtyFour /2/body/tex/page.html}
\end{itemize}

The first link points to the present paper. The second link points to an electronic appendix with definitions that would bore most readers (such as definitions of how each construct should be rendered). The second link is included in the \textsc{Bib}\TeX\ bibliography \cite{chores} for easy reference. The third link points to a table of contents.



\subsection{Referenced Logiweb pages}

The present Logiweb page references the following other Logiweb page:

\begin{itemize}
\item \href{\lgwrelay 64/\lgwBaseBlockBaseSixtyFour/2/body/tex/chores.pdf}{\lgwBreakRelay 64/\lgwBaseBreakBaseSixtyFour/2/body/tex/chores.pdf} \cite{base}
\end{itemize}



\subsection{Bed page}

The present page may be used as `bed' page, i.e.\ as the first reference of other pages. Pages which use the present page as bed page and which do not define a verifier of their own use the verifier of the present page:

"[[[ verifier test1 &c proofcheck end verifier ]]]"

\noindent The verifier is a conjunction of "[[ proofcheck ]]" which is the proof checker defined on the present page and "[[ test1 ]]" which is defined on the bed page of the present page. The "[[ test1 ]]" verifier executes test suites and supports testing of computable functions.

Pages which use the present page as bed page and which do not define a macro expander of their own use the macro expander of the present page:

"[[[ expander macro1 end expander ]]]"

\noindent The expander is nothing but a reexport of the expander defined on the bed page of the present page.



\section{Terms}

\subsection{Aspect declarations}

We shall use several user aspects for implementing the proof checker.

Logiweb has a list of predefined aspects like `value', `pyk', `tex', and so on. Predefined aspects are built up from small letters and space characters. The list of predefined aspects may grow with time, so user defined aspects must contain at least one character which is neither a small letter, nor a space character.

Furthermore, to reduce the risk of name conflicts, one should give any user aspect a personal touch. The aspects defined in the following all end with a slash and the initials of the present author. If two authors use the same aspect for different things, then a third author may run into trouble when referencing both of the two first authors.

Logiweb has means for defining guaranteed unique aspects, but we shall not use that here. The aspects to be used are:

\begin{statements}

\item "[[ eager message define statement as "statement/kg" end define ]]"\index{statement} defines `"[[ statement ]]"' to represent the \index{aspect, statement}\indexintro{statement aspect}. The present page uses the statement aspect for expressing lemmas, theories, axioms, inference rules, and conjectures.

\item "[[ eager message define proof as "proof/kg" end define ]]"\index{proof} defines `"[[ proof ]]"' to represent the \index{aspect, proof}\index{proof aspect}\intro{proof} user aspect. The present page uses the proof aspect for expressing formal proofs.

\item "[[ eager message define meta as "meta/kg" end define ]]"\index{meta} defines `"[[ meta ]]"' to represent the \index{aspect, meta}\index{meta aspect}\intro{meta} user aspect. The present page uses the meta aspect for declaring constructs to be meta-variables, meta-quantifiers and sequent operators.

\item "[[ eager message define math as "math/kg" end define ]]"\index{math} defines `"[[ math ]]"' to represent the \index{aspect, math}\index{math aspect}\intro{math} user aspect. The semantics of this aspect is defined by individual axiomatic systems, the intension being that definition of new function letters are done using this aspect.

\item "[[ eager message define tactic as "tactic/kg" end define ]]"\index{tactic} defines `"[[ tactic ]]"' to represent the \index{aspect, tactic}\index{tactic aspect}\intro{tactic} user aspect. The present page uses the tactic aspect for specifying how proofs should be translated into sequent terms.

\item "[[ eager message define unitac as "unitac/kg" end define ]]"\index{unitac} defines `"[[ unitac ]]"' to represent the \index{aspect, unitac}\index{unitac aspect}\intro{unitac} user aspect. The unitac aspect defines a special kind of tactic which may occur inside arguments of the `unification tactic'. The unification tactic is described later.

\item "[[ eager message define locate as "locate/kg" end define ]]"\index{locate} defines `"[[ locate ]]"' to represent the \index{aspect, locate}\index{locate aspect}\intro{locate} user aspect. The present page uses the locate aspect for locating the source of errors for the sake of diagnostic messages.

\end{statements}



\subsection{Definition constructs}

The following constructs allow to define various aspects of a construct "[[ x ]]".

\begin{statements}

\item "[[ macro define statement define x as y end define as define statement of x as y end define end define ]]".

\item "[[ macro define proof define x as y end define as define proof of x as y end define end define ]]".

\item "[[ macro define meta define x as y end define as define meta of x as y end define end define ]]".

\item "[[ macro define math define x as y end define as define math of x as y end define end define ]]".

\item "[[ macro define tactic define x as y end define as define tactic of x as y end define end define ]]".

\item "[[ macro define unitac define x as y end define as define unitac of x as y end define end define ]]".

\item "[[ macro define locate define x as y end define as define locate of root protect x end protect as y end define end define ]]".

\end{statements}

In `locate' definitions, the construct being defined is protected against macro expansion. This is important because errors are located in the body of a page, i.e.\ in the page before macro expansion whereas locate definitions are interpretted after macro expansion. So protection is needed in cases where one needs to assign a locate aspect to some construct which also has a macro definition.



\subsection{Axioms, rules, theories, and lemmas}

Axioms, inference rules, theories, and lemmas are all represented by statement definitions. As an example, a lemma "[[ L ]]" saying that any statement infers itself could read

"[ hide lemma L : #a infer #a end lemma end hide ]"

\noindent which is simply shorthand for "[[ hide statement define L as #a infer #a end define end hide ]]". The lemma construct is defined thus: "[[ macro define lemma x : y end lemma as ensure math statement define x as y end define end math end define ]]".

A theory "[[ T ]]" comprising an inference rule named "[[ p.MP ]]" and three axioms "[[ p.A1 ]]", "[[ p.A2 ]]", and "[[ p.A3 ]]" could read

"[ hide theory T : p.MP oplus p.A1 oplus p.A2 oplus p.A3 end theory end hide ]"

\noindent which is shorthand for "[[ hide statement define T as p.MP oplus p.A1 oplus p.A2 oplus p.A3 end define end hide ]]". The theory construct is defined thus: "[[ macro define theory x : y end theory as ensure math define statement of x as y end define end math end define ]]".

An axiom "[[ p.A1 ]]" which says that "[[ #a p.imply #b p.imply #a ]]" for all terms "[[ #a ]]" and "[[ #b ]]" could read

"[ hide axiom p.A1 : All #a ,, #b : A p.imply B p.imply A end axiom end hide ]"

\noindent This is shorthand for "[[ hide statement define p.A1 as All #a ,, #b : #a p.imply #b p.imply #a end define end hide ]]" plus one more definition. The second definition is a unitac definition which explains how to prove the axiom. This may seem strange since, from a human point of view, axioms are assumed rather than proved. But in the present system, axioms actually do have to be proved, and the proof even depends on context. As an example, if axiom "[[ p.A1 ]]" occurs in a proof which is relative to the theory "[[ T ]]" above, then the proof of "[[ p.A1 ]]" will be one which accesses the second element of "[[ T ]]". In a proof relative to "[[ p.A1 oplus p.A2 oplus p.A3 oplus p.MP ]]", the proof would be one which accesses the first element.

A working logician need not care about how axioms are proved backstage. And need not even know that axioms do have to be proved. The working logician just needs to state proofs in a style close to that of \cite{Mendelson} and the definitions on the present page will take care of the rest.

The axiom construct is defined thus:

"[[[ macro define axiom x : y end axiom as ensure math define statement of x as y end define,unitac define x as \ u . unitac-rule ( u ) end define end math end define ]]]"

When an axiom like "[[ p.A1 ]]" occurs in a proof line which is expanded using the unification tactic, then the unification tactic evaluates "[[ unitac-rule ( << t ,, s ,, c >> ) ]]" where "[[ t ]]" is "[[ p.A1 ]]", "[[ s ]]" is a `state' which contains local information, and "[[ c ]]" is the cache of the page on which the proof occurs. Among other, the state "[[ s ]]" contains information about which theories may be used and which hypotheses have been assumed. The value of "[[ unitac-rule ( << t ,, s ,, c >> ) ]]" is a proof of "[[ All #a ,, #b : #a p.imply #b p.imply #a ]]" which the unification tactic will then try to instantiate suitably.

From the point of view of the proof checker, there is no difference between axioms and inference rules:

"[[[ macro define rule x : y end rule as ensure math define statement of x as y end define,unitac define x as \ u . unitac-rule ( u ) end define end math end define ]]]"



\subsection{Meta variables}

We use the meta aspect to declare that a construct is a meta variable. In general, several aspects are used when finding out what a construct means: Constructs which have a meta aspect mean whatever that aspect says they mean. Constructs without a meta aspect mean whatever the value aspect says they mean. Constructs with neither meta nor value aspect mean whatever the def aspect says they mean. Constructs with no meta, value, or def aspect are considered to be object variables. So e.g.\ "[[ a ]]", "[[ X ]]", and "[[ beta ]]" are object variables.

A construct is a meta variable if its "[[ meta ]]" aspect equals "[[ name "var" end name ]]". The following construct allows to declare meta variables:

"[[[ macro define metadeclare x as meta define x as "var" end define end define ]]]"

To have an arsenal of meta variables, we declare "[[ #a ]]", "[[ #b ]]", and so on to be meta variables:
"[[ metadeclare #a ]]",
"[[ metadeclare #b ]]",
"[[ metadeclare #c ]]",
"[[ metadeclare #d ]]",
"[[ metadeclare #e ]]",
"[[ metadeclare #f ]]",
"[[ metadeclare #g ]]",
"[[ metadeclare #h ]]",
"[[ metadeclare #i ]]",
"[[ metadeclare #j ]]",
"[[ metadeclare #k ]]",
"[[ metadeclare #l ]]",
"[[ metadeclare #m ]]",
"[[ metadeclare #n ]]",
"[[ metadeclare #o ]]",
"[[ metadeclare #p ]]",
"[[ metadeclare #q ]]",
"[[ metadeclare #r ]]",
"[[ metadeclare #s ]]",
"[[ metadeclare #t ]]",
"[[ metadeclare #u ]]",
"[[ metadeclare #v ]]",
"[[ metadeclare #w ]]",
"[[ metadeclare #x ]]",
"[[ metadeclare #y ]]", and
"[[ metadeclare #z ]]".

A term is a meta variable, if the "[[ meta ]]" aspect of the root of the term equals "[[ name "var" end name ]]". As an example of use, we declare the unary construct "[[ x# ]]" to be a meta variable:

"[[[ metadeclare x# ]]]"

\noindent The construct above allows to use e.g.\ "[[ a# ]]", "[[ beta# ]]", "[[ c prime# ]]", and "[[ d _ { 5 }# ]]" as meta variables.

Two meta variable are identical if they are identical as terms (i.e.\ w.r.t.\ "[[ x t= y ]]"). As a peculiarity this entails that "[[ ( 2 + 2 )# ]]" and "[[ 4# ]]" are distinct meta variables.

We shall need two more indexed meta variables: "[[ metadeclare tacfresh ( x ) ]]" and "[[ metadeclare unifresh ( x , y ) ]]". The unification tactic defined later uses these indexed meta variables to generate variables that are supposed to be `fresh'. If you use these indexed meta variables in proofs, you ask for trouble.



\subsection{Cache accessors}

Given a construct "[[ x ]]" and a cache "[[ c ]]", the following functions return various information about "[[ x ]]". The last construct below decides whether or not a construct "[[ x ]]" is a meta variable.

\begin{statements}

\item "[[ eager define x plist ( c ) as c [[ x ref ]] [[ "codex" ]] [[ x ref ]] [[ x idx ]] [[ 0 ]] end define ]]". Given a symbol "[[ x ]]", this construct looks up an array which maps strings to the associated aspects.

\item "[[ eager define x def ( c , a ) as x plist ( c ) [[ a ]] end define ]]". Look up aspect "[[ a ]]" of symbol "[[ x ]]".

\item "[[ eager define x lhs ( c , a ) as x def ( c , a ) second end define ]]". Look up the left hand side of the aspect "[[ a ]]" definition of symbol "[[ x ]]".

\item "[[ eager define x rhs ( c , a ) as x def ( c , a ) third end define ]]". Look up the right hand side of the aspect "[[ a ]]" definition of symbol "[[ x ]]".

\item "[[ eager define x metadef ( c ) as x rhs ( c , meta ) idx end define ]]". Look up the meta definition of symbol "[[ x ]]".

\item "[[ eager define x metavar ( c ) as x metadef ( c ) = "var" end define ]]". True if "[[ x ]]" is a meta variable.

\item "[[ eager define x stmt-rhs ( c ) as x rhs ( c , statement ) end define ]]". Look up the statement definition of symbol "[[ x ]]".

\item "[[ eager define x proof-rhs ( c ) as x rhs ( c , proof ) end define ]]". Look up the statement definition of symbol "[[ x ]]".

\item "[[ eager define x tactic-rhs ( c ) as x rhs ( c , tactic ) end define ]]". Look up the statement definition of symbol "[[ x ]]".

\item "[[ eager define x unitac-rhs ( c ) as x rhs ( c , unitac ) end define ]]". Look up the statement definition of symbol "[[ x ]]".

\item "[[ eager define x locate-rhs ( c ) as x rhs ( c , locate ) end define ]]". Look up the statement definition of symbol "[[ x ]]".

\end{statements}



\subsection{Meta operators}

In addition to meta variables, the five operators for building meta terms of the Logiweb sequent calculus are:

\begin{statements}

\item "[[ meta define x infer y as "infer" end define ]]". States that provability of "[[ x ]]" implies provability of "[[ y ]]".

\item "[[ meta define x endorse y as "endorse" end define ]]" States that if "[[ x ]]" evaluates to "[[ true ]]" then "[[ y ]]" is provable.

\item "[[ meta define x oplus y as "plus" end define ]]" States that both "[[ x ]]" and "[[ y ]]" are provable.

\item "[[ meta define All x : y as "all" end define ]]". States that "[[ y ]]" is provable for all "[[ x ]]"

\item "[[ meta define False as "false" end define ]]". Expresses absurdity. One may disprove "[[ x ]]" is by proving "[[ x infer False ]]"

\end{statements}



\subsection{Meta constructs}

We shall say that a construct is a \index{construct, meta}\indexintro{meta construct} iff the construct has a meta definition. In other words we shall say that a construct "[[ x ]]" is a meta construct iff "[[ x metadef ( self ) != true ]]".

We shall say that a meta construct is a \index{variable, meta}\indexintro{meta variable} iff it is meta defined as "[[ name "var" end name ]]". In other words, "[[ x ]]" is a meta variable iff "[[ x metadef ( self ) = "var" ]]".

We shall say that a meta construct "[[ x ]]" is a \index{binder, meta}\indexintro{meta binder} iff "[[ x metadef ( self ) = "all" ]]".

We shall say that a meta construct is a \index{operator, meta}\indexintro{meta operator} if it is neither a meta variable nor a meta binder.



\subsection{Object constructs}

We shall say that a construct is an \index{construct, object}\indexintro{object construct} iff it is not a meta construct. So "[[ x ]]" is an object construct iff "[[ x metadef ( self ) = true ]]"

We shall say that an object construct is an \index{binder, object}\indexintro{object binder} if the construct is declared to denote lambda abstraction. So "[[ x ]]" is an object binder iff "[[ self [[ x ref ]] [[ "code" ]] [[ x idx ]] = 0 ]]".

We shall say that an object construct "[[ x ]]" is a \indexintro{quote} if the construct is declared to denote quoting. So "[[ x ]]" is a quote iff "[[ self [[ x ref ]] [[ "code" ]] [[ x idx ]] = 1 ]]".

We shall say that an object construct is an \index{variable, object}\indexintro{object variable} if it neither has a value nor a math definition.

We shall say that object constructs other than object variables, object binders, and quotes are \index{operator, object}\index{object operator}\intro{object operators}.



\subsection{Object terms}

We shall say that a term is an \index{term, object}\indexintro{object term} if it is built up from the following:

\begin{itemize}

\item object operators applied to object terms.

\item quotes applied to arbitrary terms.

\item object variables applied to arbitrary terms (i.e.\ object variables with arbitrary indices).

\item object binders applied to an object or meta variable and an object term in that order.

\item meta variables applied to arbitrary terms (i.e.\ meta variables with arbitrary indices).

\end{itemize}

In other words, a term "[[ x ]]" is an object term iff "[[ x objectterm ( self ) ]]" where we define "[[ x objectterm ( c ) ]]" in the following.

\begin{statements}

\item "[[ eager define x valuedef ( c ) as c [[ x ref ]] [[ "code" ]] [[ x idx ]] end define ]]". The value definition of "[[ x ]]". This is "[[ 0 ]]" for lambda abstractions, "[[ 1 ]]" for quotes, and "[[ true ]]" for constructs with no value definition.

\item "[[ eager define x mathdef ( c ) as x rhs ( c , math ) idx end define ]]". The math definition of "[[ x ]]". This is "[[ true ]]" for constructs with no math definition.

\item "[[ eager define x objectvar ( c ) as x metadef ( c ) = true .and. x valuedef ( c ) = true .and. x mathdef ( c ) = true end define ]]". This is true if "[[ x ]]" is an object variable.

\item "[[ eager define x objectlambda ( c ) as x metadef ( c ) = true .and. x valuedef ( c ) = 0 end define ]]". This is true if "[[ x ]]" is a lambda abstraction.

\item "[[ eager define x objectquote ( c ) as x metadef ( c ) = true .and. x valuedef ( c ) = 1 end define ]]". This is true if "[[ x ]]" is a lambda abstraction.

\item "[[ eager define x objectterm ( c ) as newline let d = x metadef ( c ) in newline if d = "var" then true else newline if d != true then false else newline let d = x valuedef ( c ) in newline if d = 0 then ( x first objectvar ( c ) .or. x first metavar ( c ) ) .and. x second objectterm ( c ) else newline if d = 1 then true else if d .and. x mathdef ( c ) then true else x tail objectterm* ( c ) end define ]]"

\item "[[ eager define x objectterm* ( c ) as x atom .or. x head objectterm ( c ) .and. x tail objectterm* ( c ) end define ]]".

\end{statements}



\subsection{Meta terms}

We shall say that a term is a \index{term, meta}\indexintro{meta term} if it is built up from the following:

\begin{itemize}

\item object terms.

\item meta operators applied to meta terms.

\item meta binders applied to a meta variable and a meta term in that order.

\end{itemize}

In other words, a term "[[ x ]]" is a meta term iff "[[ x metaterm ( self ) ]]" where we define "[[ x metaterm ( c ) ]]" in the following.

\begin{statements}

\item "[[ eager define x metaterm ( c ) as newline let d = x metadef ( c ) in newline if d = "var" then true else newline if d = "all" then x first metavar ( c ) .and. x second metaterm ( c ) else newline if d != true then x tail metaterm* ( c ) else x objectterm ( c ) end define ]]"

\item "[[ eager define x metaterm* ( c ) as x atom .or. x head metaterm ( c ) .and. x tail metaterm* ( c ) end define ]]"

\end{statements}



\subsection{Avoidance}

We shall say that a variable "[[ x ]]" \index{avoid}\intro{avoids} a term "[[ t ]]" if "[[ x ]]" does not occur free in "[[ t ]]". The meta version of avoidance is defined thus:

\begin{statements}

\item "[[ eager define x metaavoid ( c ) y as x metavar ( c ) .and. metaavoid1 ( x , y , c ) end define ]]". True if "[[ x ]]" is a meta variable and "[[ x ]]" does not occur free in the meta term "[[ y ]]".

\item "[[ eager define x metaavoid* ( c ) y as newline if y atom then true else newline if x metaavoid ( c ) ( y head ) then x metaavoid* ( c ) ( y tail ) else y head end define ]]". True if "[[ x ]]" does not occur free in any element of the list "[[ y ]]" of meta terms. Otherwise returns the first element of "[[ y ]]" in which "[[ x ]]" occurs free.

\item "[[ eager define metaavoid1 ( x , y , c ) as newline let d = y metadef ( c ) in newline if d = "var" then .not. x t= y else newline if d = "all" then x t= y first .or. metaavoid1 ( x , y second , c ) else newline if d != true then metaavoid1* ( x , y tail , c ) else newline let d = y valuedef ( c ) in newline if d = 1 then true else metaavoid1* ( x , y tail , c ) end define ]]"

\item "[[ eager define metaavoid1* ( x , y , c ) as y atom .or. metaavoid1 ( x , y head , c ) .and. metaavoid1* ( x , y tail , c ) end define ]]"

\end{statements}

The object version of avoidance is defined in the following. We define a construct "[[ x objectavoid* ( c ) y ]]" which is true if "[[ x ]]" is a list of distinct object variables all of which avoid the term "[[ y ]]".

\begin{statements}

\item "[[ eager define distinctvar ( x , c ) as x atom .or. x head objectvar ( c ) .and. .not. x head member x tail .and. distinctvar ( x tail , c ) end define ]]". True if "[[ x ]]" is a list of distinct meta variables.

\item "[[ eager define x objectavoid* ( c ) y as distinctvar ( x , c ) .and. ( objectavoid1 ( x , y , c , true ) catch tail ) end define ]]". True if "[[ x ]]" is a list of object variables none of which occur free in the meta term "[[ y ]]". If some element of "[[ x ]]" definitely occur free in "[[ y ]]" then the function returns "[[ false ]]". If the term contains meta variables then the function returns a list of meta variables which the variables in "[[ x ]]" must avoid in order to avoid "[[ y ]]".

\item "[[ eager define x objectavoid ( c ) y as << x >> objectavoid* ( c ) y end define ]]". Same as above except that "[[ x ]]" is a term rather than a list of terms.

\item "[[ eager define objectavoid1 ( x , y , c , r ) as newline if x = <<>> then r else newline let d = y metadef ( c ) in newline if d = "var" then r set+ y else newline let d = y valuedef ( c ) in newline if d = true then if y member x then false raise else r else newline if d = 0 then objectavoid1 ( x set- y first , y second , c , r ) else newline if d = 1 then r else newline objectavoid1* ( x , y tail , c , r ) end define ]]"

\item "[[ eager define objectavoid1* ( x , y , c , r ) as if y atom then r else objectavoid1* ( x , y tail , c , objectavoid1 ( x , y head , c , r ) ) end define ]]"

\end{statements}



\subsection{Substitution freeness}

We shall say that a substitution is \index{free substitution}\index{substitution, free}\intro{free} if one can perform the substitution without renaming. The meta and object versions of freeness are defined in the following.

\begin{statements}

\item "[[ eager define metafree ( x , y , z , c ) as newline let d = x metadef ( c ) in newline if d = "var" then true else newline if d = true then z objectterm ( c ) .or. y metaavoid ( c ) x else newline if d != "all" then metafree* ( x tail , y , z , c ) else newline if y t= x first then true else newline if y metaavoid ( c ) x second then true else newline x first metaavoid ( c ) z .and. metafree ( x second , y , z , c ) end define ]]". True if one can freely replace the meta variable "[[ y ]]" by the meta term "[[ z ]]" in the meta term "[[ x ]]".

\item "[[ eager define metafree* ( x , y , z , c ) as x atom .or. metafree ( x head , y , z , c ) .and. metafree* ( x tail , y , z , c ) end define ]]" True if one can freely replace the meta variable "[[ y ]]" by the meta term "[[ z ]]" in any element of the list "[[ x ]]" of meta terms.

\item "[[ eager define objectfree ( x , y , z , c ) as newline if x metadef ( c ) != true then false else newline let d = x valuedef ( c ) in newline if d = true then true else newline if d = 1 then true else newline if d != 0 then objectfree* ( x tail , y , z , c ) else newline if y t= x first then true else newline if y objectavoid ( c ) x second then true else newline x first objectavoid ( c ) z .and. objectfree ( x second , y , z , c ) end define ]]". True if one can freely replace the object variable "[[ y ]]" by the object term "[[ z ]]" in the object term "[[ x ]]".

\item "[[ eager define objectfree* ( x , y , z , c ) as x atom .or. objectfree ( x head , y , z , c ) .and. objectfree* ( x tail , y , z , c ) end define ]]". True if one can freely replace the object variable "[[ y ]]" by the object term "[[ z ]]" in any element of the list "[[ x ]]" of object terms.

\end{statements}



\subsection{Substitution}

The function "[[ metasubst ( x , s , c ) ]]" defined in the following substitutes variables with terms as specified in the association list "[[ s ]]". Only free occurences of variables in "[[ x ]]" are replaced. The function performs substitution without renaming of free variables and does not check whether or not the substitution if free. Substitution is parallel so that one may use e.g.\ "[[ s = << quote x end quote :: quote y end quote ,, quote y end quote :: quote x end quote >> ]]" to swap "[[ x ]]" and "[[ y ]]".

\begin{statements}

\item "[[ eager define metasubst ( x , s , c ) as newline let d = x metadef ( c ) in newline if d = "var" then lookup ( x , s , x ) else newline if d != "all" then x head :: metasubst* ( x tail , s , c ) else newline let s = remove ( x first , s ) in newline << x head ,, x first ,, metasubst ( x second , s , c ) >> end define ]]".

\item "[[ eager define metasubst* ( x , s , c ) as newline if x atom then true else newline metasubst ( x head , s , c ) :: metasubst* ( x tail , s , c ) end define ]]"

\end{statements}

The following function is like "[[ metasubst ( x , s , c ) ]]" but also checks that the substitution is free, that "[[ z ]]" is a metaterm, and that if "[[ x ]]" is a metaterm then so is the return value. Returns "[[ true ]]" on error.

\begin{statements}

\item "[[ eager define metasubstc ( x , s , c ) as metasubstc1 ( x , s , true , c ) end define ]]"

\item "[[ eager define metasubstc1 ( x , s , b , c ) as newline let d = x metadef ( c ) in newline if d = "var" then metasubstc3 ( x , s , b , c ) else newline if d then metasubstc2 ( x , s , b , c ) else newline if d != "all" then x head :: metasubstc1* ( x tail , s , b , c ) else newline let s = remove ( x first , s ) in newline << x head ,, x first ,, metasubstc1 ( x second , s , x first :: b , c ) >> end define ]]".

\item "[[ eager define metasubstc1* ( x , s , b , c ) as newline if x atom then true else newline metasubstc1 ( x head , s , b , c ) :: metasubstc1* ( x tail , s , b , c ) end define ]]"

\item "[[ eager define metasubstc2 ( x , s , b , c ) as newline let d = x metadef ( c ) in newline if d then x head :: metasubstc2* ( x tail , s , b , c ) else newline let v = lookup ( x , s , true ) in newline if v then x else newline let d = v metadef ( c ) in newline if .not. d .and. d != "var" then newline error ( x , LocateProofLine ( x , c ) diag ( "Substitution of" ) disp ( x ) diag ( "with" ) disp ( v ) diag ( "produces non-meta-term" ) end diagnose ) else newline if metaavoid2* ( b , v , c ) then v else newline error ( x , LocateProofLine ( x , c ) diag ( "At-seqop used for non-free substitution. Attempt to instantiate" ) disp ( x ) diag ( "with" ) disp ( v ) end diagnose ) end define ]]"

\item "[[ eager define metasubstc2* ( x , s , b , c ) as newline if x atom then true else newline metasubstc2 ( x head , s , b , c ) :: metasubstc2* ( x tail , s , b , c ) end define ]]"

\item "[[ eager define metaavoid2* ( x , y , c ) as x .or. x head metaavoid ( c ) y .and. metaavoid2* ( x tail , y , c ) end define ]]"

\item "[[ eager define metasubstc3 ( x , s , b , c ) as newline let v = lookup ( x , s , true ) in newline if v then x else newline if metaavoid2* ( b , v , c ) then v else newline error ( x , LocateProofLine ( x , c ) diag ( "At-seqop used for non-free substitution. Attempt to instantiate" ) disp ( x ) diag ( "with" ) disp ( v ) end diagnose ) end define ]]"

\item "[[ eager define remove ( x , s ) as newline if s atom then s else newline if x t= s head head then remove ( x , s tail ) else newline s head :: remove ( x , s tail ) end define ]]"

\end{statements}



\subsection{Quantifiers}

The following macro definition allows to write e.g.\ "[[ All #x ,, #y ,, #z : #a ]]" instead of "[[ All #x : All #y : All #z : #a ]]".

\begin{statements}

\item "[[ Macro define All u : v as \ x . expand-All ( x ) end define ]]"

\item "[[ eager define expand-All ( x ) as newline let << t ,, s ,, c >> = x in newline let << true ,, u ,, v >> = t in newline let u = stateexpand ( u , s , c ) in newline let v = stateexpand ( v , s , c ) in newline expand-All1 ( t , u , v ) end define ]]"

\item "[[ eager define expand-All1 ( t , u , v ) as newline if .not. u r= quote x ,, y end quote then back t quote All u unquote : v unquote end quote else newline expand-All1 ( t , u first , expand-All1 ( t , u second , v ) ) end define ]]"

\end{statements}



\section{Sequents}

\subsection{Term sets}\label{sec:TermSets}

We represent sets of terms by tuples of terms without repetitions so that no two elements "[[ x ]]" and "[[ y ]]" of the tuple satisfy "[[ x t= y ]]".

\begin{statements}

\item "[[ eager define x member y as if y atom then false else x t= y head .or. x member y tail end define ]]". Membership of a set of terms.

\item "[[ eager define x set+ y as if y member x then x else y :: x end define ]]". Add the term "[[ y ]]" to the set "[[ x ]]" of terms.

\item "[[ eager define x set- y as if y member x then x set-- y else x end define ]]". Remove the term "[[ y ]]" from the set "[[ x ]]" of terms.

\item "[[ eager define x set-- y as if x atom then true else if x head t= y then x tail else x head :: x tail set-- y end define ]]"

\item "[[ eager define x subset y as if x atom then true else x head member y .and. x tail subset y end define ]]"

\item "[[ eager define x union y as if x atom then y else x tail union ( y set+ x head ) end define ]]"

\item "[[ eager define x set= y as x subset y .and. y subset x end define ]]"

\end{statements}



\subsection{Sequents}

The sequents of Logiweb sequent calculus have form "[[ << P ,, C ,, R >> ]]" where "[[ P ]]" is a pool of premisses, "[[ C ]]" is a pool of condition (i.e.\ side conditions), and "[[ R ]]" is a result which holds if the given premisses and conditions hold. "[[ P ]]" and "[[ C ]]" are sets of meta terms (c.f. Section \ref{sec:TermSets}) and "[[ R ]]" is a meta term.

\begin{statements}

\item "[[ eager define x sequent= y as x zeroth set= y zeroth .and. x first set= y first .and. x second t= y second end define ]]"

\end{statements}



\subsection{Sequent operators}

The thirteen sequent operators of the Logiweb sequent calculus are:

\begin{statements}

\item "[[ meta define x Init as "Init" end define ]]". Allows to build a sequent with "[[ x ]]" as both premise and result.

\item "[[ meta define x Ponens as "Ponens" end define ]]". Allows to move a premise from result to premise pool.

\item "[[ meta define x Probans as "Probans" end define ]]". Allows to move a condition from result to condition pool.

\item "[[ meta define x Verify as "Verify" end define ]]". Allows to evaluate and remove a condition from the result.

\item "[[ meta define x Curry as "Curry" end define ]]". Allows to change a result from "[[ x oplus y infer z ]]" to "[[ x infer y infer z ]]".

\item "[[ meta define x Uncurry as "Uncurry" end define ]]". Allows to change a result from "[[ x infer y infer z ]]" to "[[ x oplus y infer z ]]"

\item "[[ meta define x Deref as "Dereference" end define ]]". Allows to change the name of a result to the result itself.

\item "[[ meta define x at y as "at" end define ]]". Allows to instantiate a meta quantifier.

\item "[[ meta define x infer y as "infer" end define ]]". Allows to move a premise from premise pool to result.

\item "[[ meta define x endorse y as "endorse" end define ]]". Allows to move a condition from condition pool to result.

\item "[[ meta define x id est y as "id est" end define ]]". Allows to change the result of "[[ x ]]" to the name "[[ y ]]" for the result.

\item "[[ meta define All x : y as "all" end define ]]". Allows to perform meta generalization.

\item "[[ meta define x ;; y as "cut" end define ]]". Allows to perform a cut operation.

\end{statements}

The operators "[[ x infer y ]]", "[[ x endorse y ]]", and "[[ All x : y ]]" may be used both as meta and as sequent operators. Whether they denote the one or the other depends on context.



\subsection{Sequent pseudo operators}

In addition to the genuine sequent operators the following pseudo operators allow to build up the body of a proof. The pseudo operators disappear during unification.

\begin{statements}

\item "[[ meta define x ponens y as "ponens" end define ]]". Same as "[[ x Ponens ]]" but "[[ y ]]" specifies what the moved premise looks like as an aid to unification.

\item "[[ meta define x probans y as "probans" end define ]]". Same as "[[ x Probans ]]" but "[[ y ]]" specifies what the moved condition looks like as an aid to unification.

\item "[[ meta define x verify y as "verify" end define ]]". Same as "[[ x Verify ]]" but "[[ y ]]" specifies what the verified condition looks like as an aid to unification.

\item "[[ meta define x conclude y as "conclude" end define ]]". Same as "[[ x ]]" but "[[ y ]]" specifies what "[[ x ]]" is supposed to prove as an aid to unification.

\item "[[ meta define x At as "At" end define ]]". Same as "[[ x at y ]]" but leaves it to unification to determine "[[ y ]]".

\item "[[ meta define x Infer as "Infer" end define ]]". Same as "[[ y infer x ]]" but leaves it to unification to determine "[[ y ]]".

\item "[[ meta define x Endorse as "Endorse" end define ]]". Same as "[[ y endorse x ]]" but leaves it to unification to determine "[[ y ]]".

\item "[[ meta define x All as "All" end define ]]". Same as "[[ All y : x ]]" but leaves it to unification to determine "[[ y ]]".

\item "[[ meta define x Conclude as "Conclude" end define ]]". Add as many "[[ x at y ]]", "[[ x Ponens ]]", and "[[ x Verify ]]" operations as possible in an attempt to make "[[ x ]]" prove an object term.

\end{statements}



\subsection{Counting of sequent operators}

The following function can be used for profiling tactics in that it returns the number of tactic operators in the term t.

"[[ eager define seqcnt ( t , c ) as newline if t r= quote x Init end quote then 1 else newline if t r= quote x Ponens end quote then 1 + seqcnt ( t first , c ) else newline if t r= quote x Probans end quote then 1 + seqcnt ( t first , c ) else newline if t r= quote x Verify end quote then 1 + seqcnt ( t first , c ) else newline if t r= quote x Curry end quote then 1 + seqcnt ( t first , c ) else newline if t r= quote x Uncurry end quote then 1 + seqcnt ( t first , c ) else newline if t r= quote x Deref end quote then 1 + seqcnt ( t first , c ) else newline if t r= quote x at y end quote then 1 + seqcnt ( t first , c ) else newline if t r= quote x infer y end quote then 1 + seqcnt ( t second , c ) else newline if t r= quote x endorse y end quote then 1 + seqcnt ( t second , c ) else newline if t r= quote x id est y end quote then 1 + seqcnt ( t first , c ) else newline if t r= quote All x : y end quote then 1 + seqcnt ( t second , c ) else newline if t r= quote x ;; y end quote then 1 + seqcnt ( t first , c ) + seqcnt ( t second , c ) else newline error ( t , LocateProofLine ( t , c ) diag ( "In seqcnt: Unknown seqop in root of" ) disp ( t ) end diagnose ) end define ]]"



\subsection{Error message construct}

The "[[ eager define error ( x , y ) as ( dbug ( x ) y ) raise end define ]]" construct is useful for signaling errors. The construct signals that an error has occurred by raising an exception. Exceptions take one parameter, and "[[ error ( x , y ) ]]" raises an exception with parameter "[[ y ]]". That parameter is supposed to be a term which, when typeset, explains to a human reader what went wrong.

If the term "[[ y ]]" contains no useful ``debugging information'' then "[[ error ( x , y ) ]]" takes the debugging information from "[[ x ]]". At the time of writing, the debugging information is not used. As an example of use, a Logiweb browser could have a button for moving to the proof line in error. As another example, a custom renderer could add a hypertarget to the line in error such that one could navigate to it using an ordinary web browser.



\subsection{Pattern recognition}

The `mismatch' construct defined in the following is such that e.g.\ "[[ mismatch ( quote x infer y end quote , R , c ) ]]" is false if "[[ R ]]" has form "[[ x infer y ]]".

\begin{statements}

\item "[[ eager define mismatch ( x , y , c ) as newline let a = x metadef ( c ) in newline if a = true then false else newline if a != y metadef ( c ) then true else mismatch* ( x tail , y tail , c ) end define ]]"



\item "[[ eager define mismatch* ( x , y , c ) as newline if x atom .and. y atom then false else newline if x atom .or. y atom then true else newline mismatch ( x head , y head , c ) .or. mismatch* ( x tail , y tail , c ) end define ]]"

\end{statements}



\subsection{Sequent evaluator}

"[[ seqeval ( t , c ) ]]" evaluates the sequent term "[[ t ]]". The result is either an exception or a valid sequent "[[ s ]]". In the latter case, "[[ t ]]" is said to be a sequent proof of "[[ s ]]".

\vspace{\abovedisplayskip}

\noindent "[[ eager define seqeval ( t , c ) as newline if t r= quote x Init end quote then eval-Init ( t first , c ) else newline if t r= quote x Ponens end quote then eval-Ponens ( seqeval ( t first , c ) , t first , c ) else newline if t r= quote x Probans end quote then eval-Probans ( seqeval ( t first , c ) , t first , c ) else newline if t r= quote x Verify end quote then eval-Verify ( seqeval ( t first , c ) , t first , c ) else newline if t r= quote x Curry end quote then eval-Curry ( seqeval ( t first , c ) , t first , c ) else newline if t r= quote x Uncurry end quote then eval-Uncurry ( seqeval ( t first , c ) , t first , c ) else newline if t r= quote x Deref end quote then eval-Deref ( seqeval ( t first , c ) , t first , c ) else newline if t r= quote x at y end quote then eval-at ( t , true , c ) else newline if t r= quote x infer y end quote then eval-infer ( t first , seqeval ( t second , c ) , t second , c ) else newline if t r= quote x endorse y end quote then eval-endorse ( t first , seqeval ( t second , c ) , t second , c ) else newline if t r= quote x id est y end quote then eval-ie ( seqeval ( t first , c ) , t second , t first , c ) else newline if t r= quote All x : y end quote then eval-all ( t first , seqeval ( t second , c ) , t second , c ) else newline if t r= quote x ;; y end quote then eval-cut ( seqeval ( t first , c ) , seqeval ( t second , c ) , c ) else newline error ( t , LocateProofLine ( t , c ) diag ( "Unknown seqop in root of" ) disp ( t ) end diagnose ) end define ]]"



\subsection{Definitions of sequent operators}

The individual sequent operators of the Logiweb sequent calculus are defined as follows:

\begin{statements}

\item "[[ eager define eval-Init ( x , c ) as newline if x metaterm ( c ) then << << x >> ,, <<>> ,, x >> else newline error ( x , LocateProofLine ( x , c ) diag ( "Init-seqop used on non-meta term:" ) disp ( x ) end diagnose ) end define ]]"



\item "[[ eager define eval-Ponens ( x , d , c ) as newline let << P ,, C ,, R >> = x in newline if mismatch ( quote x infer y end quote , R , c ) then newline error ( d , LocateProofLine ( d , c ) diag ( "Ponens-seqop used on non-inference:" ) disp ( R ) end diagnose ) else newline let << true ,, P prime ,, R prime >> = R in newline << P set+ P prime ,, C ,, R prime >> end define ]]"



\item "[[ eager define eval-Probans ( x , d , c ) as newline let << P ,, C ,, R >> = x in newline if mismatch ( quote x endorse y end quote , R , c ) then newline error ( d , LocateProofLine ( d , c ) diag ( "Probans-seqop used on non-endorsement:" ) disp ( R ) end diagnose ) else newline let << true ,, C prime ,, R prime >> = R in newline << P ,, C set+ C prime ,, R prime >> end define ]]"



\item "[[ eager define eval-Verify ( x , d , c ) as newline let << P ,, C ,, R >> = x in newline if mismatch ( quote x endorse y end quote , R , c ) then newline error ( d , LocateProofLine ( d , c ) diag ( "Verify-seqop used on non-endorsement:" ) disp ( R ) end diagnose ) else newline let << true ,, C prime ,, R prime >> = R in newline if ( eval ( C prime , true , c ) apply c maptag ) untag catch = false :: true then << P ,, C ,, R prime >> else newline error ( d , LocateProofLine ( d , c ) diag ( "Verify-seqop used on false condition:" ) disp ( C prime ) end diagnose ) end define ]]"



\item "[[ eager define eval-Curry ( x , d , c ) as newline let << P ,, C ,, R >> = x in newline if mismatch ( quote ( x oplus y ) infer z end quote , R , c ) then newline error ( d , LocateProofLine ( d , c ) diag ( "Curry-seqop used on unfit argument:" ) disp ( R ) end diagnose ) else newline let back true quote ( X unquote oplus Y unquote ) infer Z unquote end quote = R in newline << P ,, C ,, back R quote X unquote infer Y unquote infer Z unquote end quote >> end define ]]"



\item "[[ eager define eval-Uncurry ( x , d , c ) as newline let << P ,, C ,, R >> = x in newline if mismatch ( quote x infer y infer z end quote , R , c ) then newline error ( d , LocateProofLine ( d , c ) diag ( "Uncurry-seqop used on unfit argument:" ) disp ( R ) end diagnose ) else newline let back true quote X unquote infer Y unquote infer Z unquote end quote = R in newline << P ,, C ,, back R quote ( X unquote oplus Y unquote ) infer Z unquote end quote >> end define ]]"



\item "[[ eager define eval-Deref ( x , d , c ) as newline let << P ,, C ,, R >> = x in newline let R prime = R stmt-rhs ( c ) in newline if R prime = true then newline error ( d , LocateProofLine ( d , c ) diag ( "Deref-seqop used on undefined statement:" ) disp ( R ) end diagnose ) else newline if R prime metaterm ( c ) then << P ,, C ,, R prime >> else newline error ( d , LocateProofLine ( d , c ) diag ( "Deref-seqop applied to" ) disp ( R ) diag ( "produced non-meta term:" ) disp ( R prime ) end diagnose ) end define ]]"



\item "[[ eager define eval-at ( x , v , c ) as newline if .not. x r= quote x at y end quote then let << P ,, C ,, R >> = seqeval ( x , c ) in newline << P ,, C ,, eval-at1 ( R , v , true , x , c ) >> else newline if x second metaterm ( c ) then eval-at ( x first , x second :: v , c ) else newline error ( x , LocateProofLine ( x , c ) diag ( "At-seqop used on non-meta-term:" ) disp ( x second ) end diagnose ) end define ]]"

\item "[[ eager define eval-at1 ( R , v , s , d , c ) as newline if v then metasubstc ( R , s , c ) else newline if mismatch ( quote All x : y end quote , R , c ) then error ( d , LocateProofLine ( d , c ) diag ( "At-seqop used on non-quantifier:" ) disp ( R ) end diagnose ) else newline eval-at1 ( R second , v tail , ( R first :: v head ) :: s , d , c ) end define ]]"



\item "[[ eager define eval-infer ( x , y , d , c ) as newline if .not. x metaterm ( c ) then newline error ( d , LocateProofLine ( d , c ) diag ( "Infer-seqop used on non-meta term:" ) disp ( x ) end diagnose ) else newline let << P ,, C ,, R >> = y in newline << P set- x ,, C ,, back R quote x unquote infer R unquote end quote >> end define ]]"



\item "[[ eager define eval-endorse ( x , y , d , c ) as newline if .not. x metaterm ( c ) then newline error ( d , LocateProofLine ( d , c ) diag ( "Endorse-seqop used on non-meta term:" ) disp ( x ) end diagnose ) else newline let << P ,, C ,, R >> = y in newline << P ,, C set- x ,, back R quote x unquote endorse R unquote end quote >> end define ]]"



\item "[[ eager define eval-ie ( x , y , d , c ) as newline let << P ,, C ,, R >> = x in newline if R t= y stmt-rhs ( c ) then newline << P ,, C ,, y >> else newline error ( d , LocateProofLine ( d , c ) diag ( "IdEst-seqop used on non-matching result. Attempt to match" ) disp ( y ) diag ( "with" ) disp ( R ) end diagnose ) end define ]]"



\item "[[ eager define eval-all ( x , y , d , c ) as newline let << P ,, C ,, R >> = y in newline if .not. x metaavoid* ( c ) P then newline error ( d , LocateProofLine ( d , c ) diag ( "All-seqop catches variable" ) disp ( x ) diag ( "which is free in the following premise:" ) disp ( x metaavoid* ( c ) P ) end diagnose ) else newline if .not. x metaavoid* ( c ) C then newline error ( d , LocateProofLine ( d , c ) diag ( "All-seqop catches variable" ) disp ( x ) diag ( "which is free in the following condition:" ) disp ( x metaavoid* ( c ) C ) end diagnose ) else newline << P ,, C ,, back R quote All x unquote : R unquote end quote >> end define ]]"



\item "[[ eager define eval-cut ( x , y , c ) as newline let << P ,, C ,, R >> = x in newline let << P prime ,, C prime ,, R prime >> = y in newline << P union ( P prime set- R ) ,, C union C prime ,, R prime >> end define ]]"

\end{statements}



\section{Proof construction}

\subsection{Location information}

\begin{statements}

\item "[[ locate define proof of x : y as "proof" :: 1 end define ]]". State that the given construct defines a proof and that the name of the proof is the first argument.

\item "[[ locate define x proof of y : z as "proof" :: 2 end define ]]". State that the given construct defines a proof and that the name of the proof is the second argument.

\item "[[ locate define proof define x as y end define as "proof" :: 1 end define ]]". State that the given construct defines a proof and that the name of the proof is the first argument.

\item "[[ locate define line asterisk : asterisk >> asterisk ; asterisk as "line" :: 1 end define ]]". State that the given construct defines a proof line and that the name of the proof line is the first argument.

\item "[[ locate define line asterisk : asterisk >> asterisk ; as "line" :: 1 end define ]]"

\item "[[ locate define line asterisk : asterisk >> asterisk qed as "line" :: 1 end define ]]"

\item "[[ locate define line asterisk : Premise >> asterisk ; asterisk as "line" :: 1 end define ]]"

\item "[[ locate define line asterisk : Condition >> asterisk ; asterisk as "line" :: 1 end define ]]"

\item "[[ locate define line asterisk : Arbitrary >> asterisk ; asterisk as "line" :: 1 end define ]]"

\item "[[ locate define line asterisk : Local >> asterisk = asterisk ; asterisk as "line" :: 1 end define ]]"

\item "[[ locate define line asterisk : Block >> Begin ; asterisk line asterisk : Block >> End ; asterisk as "line" :: 3 end define ]]"

\end{statements}



\subsection{Error message generation}

\begin{statements}

\item "[[ eager define make-string ( d , x ) as << << 0 ,, x ,, d >> >> end define ]]". Convert the string "[[ x ]]" to a tree which represents the term

\item "[[ eager define dbug ( x ) y as newline if y debug != true then y else newline make-root ( x , y ) :: dbug* ( x ) y tail end define ]]"

\item "[[ eager define dbug* ( x ) y as if y then true else ( dbug ( x ) y head ) :: dbug* ( x ) y tail end define ]]"

\item "[[ eager define glue ( x ) y as << make-root ( true , name quote glue' ( x ) y end quote end name ) ,, make-string ( true , x ) ,, y >> end define ]]"

\item "[[ eager define diag ( x ) y as << make-root ( true , name quote diag' ( x ) y end quote end name ) ,, make-string ( true , x ) ,, y >> end define ]]"

\item "[[ eager define disp ( x ) y as << make-root ( true , name quote disp' ( x ) y end quote end name ) ,, x ,, y >> end define ]]"

\item "[[ eager define form ( x ) y as << make-root ( true , name quote form' ( x ) y end quote end name ) ,, x ,, y >> end define ]]"

\item "[[ eager define end diagnose as make-string ( true , name "" end name ) end define ]]"

\end{statements}



\subsection{Error location}

\begin{statements}

\item "[[ eager define Locate ( t , s , c ) as newline let true :: d = reverse ( t debug head ) catch in newline let e :: v = Locate1 ( d tail , c [[ d head ]] [[ "body" ]] , s , true , c ) catch in newline if e then exception else v end define ]]". "[[ t ]]" is supposed to be a term which has been macro expanded. If macro expansion has been set up properly, then it is possible to locate where "[[ t ]]" came from before macro expansion. "[[ d ]]" is set to that location encoded as a list "[[ << r ,, i _ { 0 } ,, --- ,, i _ { n } >> ]]" where "[[ r ]]" is the reference of the page where the term occurred and "[[ i _ { 0 } ,, --- ,, i _ { n } ]]" is a path from the root of that page to the term. That path is traversed and for each symbol on the path, the locate aspect is looked up. The locate aspect is supposed to be a pair of a string and a value. If the string equals "[[ s ]]" then a pair of the symbol with subtrees and the value is returned. If more than one node matches, the last one (the one closest to "[[ t ]]") is returned. If no nodes match, then "[[ true ]]" is returned.

\item "[[ eager define Locate1 ( d , t , s , r , c ) as newline if t then r else newline let v = t locate-rhs ( c ) in newline let v = if v then true else eval ( v , true , c ) untag in newline let r = if v head = s then t :: v tail else r in newline if d atom then r else newline Locate1 ( d tail , nth ( d head , t tail ) , s , r , c ) end define ]]"

\item "[[ eager define LocateProofLine ( v , c ) y as newline let p = Locate ( v , "proof" , c ) in newline let l = Locate ( v , "line" , c ) in newline if .not. p .and. .not. l then newline dbug ( v ) diag ( "Line" ) form ( nth ( l tail , l head ) ) diag ( "in proof of" ) form ( nth ( p tail , p head ) ) glue ( ":\newline " ) y else newline if .not. p then newline dbug ( v ) diag ( "In proof of" ) form ( nth ( p tail , p head ) ) glue ( ":\newline " ) y else newline dbug ( v ) diag ( "Cannot locate error." ) diag ( "Look at ``macro'' and ``locate'' definitions." ) diag ( "" ) y end define ]]"

\end{statements}



\subsection{Proof checker}

\begin{statements}

\item "[[ eager define claiming ( x , y ) as newline if .not. y r= quote u &c v end quote then x t= y else newline claiming ( x , y first ) .or. claiming ( x , y second ) end define ]]".

True if "[[ x ]]" is among the conjuncts of a term "[[ y ]]" built up from conjunctions and "[[ u &c v ]]".

\item "[[ value define proofcheck as \ c . proofcheck1 ( c ) end define ]]".

Suited as conjunct in the claim of a page.

\item "[[ verifier test1 &c proofcheck end verifier ]]".

Use both proofcheck and test1 as verifiers.

\item "[[ eager define proofcheck1 ( c ) as newline let e :: v = proofcheck2 ( c ) catch in newline if v != true then v else newline if .not. e then true else newline name quote "In proof checker: unprocessed exception" end quote end name end define ]]".

Proofcheck page. Errors are reported as exceptions whose value is a term to be typeset as diagnose and for which the debugging information of the root indicates the location of the error.

\item "[[ eager define proofcheck2 ( c ) as newline let r = c [[ 0 ]] in newline let a = seqeval* ( c [[ r ]] [[ "codex" ]] [[ r ]] , c ) in newline let x = circularitycheck1 ( r , c , a , a ) in true end define ]]".

Check all proofs on the page using "[[ seqeval* ( a , c ) ]]", then check that the proofs do not reference each other in a circular way.

\item "[[ eager define seqeval* ( a , c ) as newline if a = true then true else newline let x :: y = a in newline if .not. x intp then seqeval* ( x , c ) :: seqeval* ( y , c ) else newline let d = y [[ 0 ]] [[ proof ]] in if d = true then true else newline print ( d second ) .then. newline let e :: p = ( eval ( d third , true , c ) apply d maptag apply c maptag ) untag [[ hook-arg ]] catch in newline if e .and. p then error ( d second , diag ( "Malformed proof of" ) form ( d second ) end diagnose ) else newline if e then p raise else newline let e :: S = seqeval ( p , c ) catch in newline if e .and. S then error ( d second , diag ( "Malformed sequent proof of" ) form ( d second ) end diagnose ) else newline if e then S raise else newline let << P ,, C ,, R >> = S in newline if C != <<>> then error ( d second , diag ( "In proof of" ) form ( d second ) glue ( ":\newline " ) diag ( "Unchecked sidecondition:" ) disp ( C head ) end diagnose ) else newline let l = y [[ 0 ]] [[ statement ]] in newline if l = true then error ( d second , diag ( "Proof of non-existent lemma:" ) disp ( d second ) end diagnose ) else newline if .not. l third t= R then newline error ( d , diag ( "The proof of" ) disp ( d second ) diag ( "does not prove what the lemma says." ) diag ( "After macro expansion, the lemma says:" ) disp ( l third ) diag ( "After macro, tactic, and sequent expansion, the proof concludes:" ) disp ( R ) end diagnose ) else newline premisecheck* ( P , c ) .and. x :: S end define ]]".

Sequent evaluate all proofs in the array "[[ a ]]" and return an array of sequents. Proofs are tactic evaluated first end the resulting sequents are checked for everything except circularities.

\item "[[ eager define premisecheck* ( P , c ) as newline if P atom then true else premisecheck ( P head , c ) .and. premisecheck* ( P tail , c ) end define ]]".

Check each premise in the list "[[ P ]]" of premisses.

\item "[[ eager define checked ( r , c ) as newline let x = c [[ r ]] [[ "codex" ]] [[ r ]] [[ 0 ]] [[ 0 ]] [[ "claim" ]] third in newline if claiming ( quote proofcheck end quote , x ) then true else newline if .not. x then false else newline let r = c [[ r ]] [[ "bibliography" ]] first in newline if r then false else newline let x = c [[ r ]] [[ "codex" ]] [[ r ]] [[ 0 ]] [[ 0 ]] [[ "claim" ]] third in newline claiming ( quote proofcheck end quote , x ) end define ]]". True if the page with reference "[[ r ]]" has been checked by "[[ proofcheck ]]".

\item "[[ eager define premisecheck ( P , c ) as newline let r = P ref in let i = P idx in newline if c [[ r ]] [[ "diagnose" ]] != true then newline error ( P , diag ( "Lemma" ) disp ( P ) diag ( "occurs on a page with a non-empty diagnose." ) diag ( "Avoid referencing that lemma." ) end diagnose ) else newline if .not. checked ( r , c ) then newline error ( P , diag ( "Lemma" ) disp ( P ) diag ( "occurs on a page which has not been checked" ) diag ( "by the present proof checker." ) diag ( "Avoid referencing that lemma." ) end diagnose ) else newline if P proof-rhs ( c ) then newline error ( P , LocateProofLine ( P , c ) diag ( "Lemma" ) disp ( P ) diag ( "has no proof. Avoid referencing that lemma." ) end diagnose ) else true end define ]]".

Check that a referenced lemma occurs on a correct page ("[[ "diagnose" = true ]]"), has been checked (claim contains verifier), and has been proved (has non-empty proof aspect).

\item "[[ eager define circularitycheck1 ( r , c , a , q ) as newline if a = true then q else newline let x :: y = a in newline if x intp then circularitycheck2 ( r , c , x , q ) else circularitycheck1 ( r , c , y , circularitycheck1 ( r , c , x , q ) ) end define ]]".

Check all indices in "[[ a ]]" for circularities. "[[ q ]]" is an array of sequents. The elements of "[[ q ]]" are set to "[[ 0 ]]" while they are being checked for circularities and are set to "[[ 1 ]]" when it has been verified that they are not circular.

\item "[[ eager define circularitycheck2 ( r , c , i , q ) as newline let v = q [[ i ]] in newline if v = 0 then newline let n = c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ proof ]] second in newline error ( n , diag ( "Circular proof. The vicious circle includes lemma" ) disp ( n ) end diagnose ) else newline if v = 1 then q else newline circularitycheck2* ( r , c , v head , q [[ i -> 0 ]] ) [[ i -> 1 ]] end define ]]".

Check the proof with index "[[ i ]]" for circularities.

\item "[[ eager define circularitycheck2* ( r , c , l , q ) as newline if l atom then q else newline let p :: l = l in newline let q = circularitycheck2* ( r , c , l , q ) in newline if r != p ref then q else circularitycheck2 ( r , c , p idx , q ) end define ]]".

Check all proofs in the list "[[ l ]]" of terms for circularity.

\item "[[ statement define lemma1 as All #x : All #y : #x infer #y infer #x end define ]]".

Manually stated lemma for testing.

\item "[[ proof define lemma1 as \ p . \ c . true [[ hook-arg -> quote All #x : All #y : #x infer #y infer #x Init end quote ]] end define ]]".

Manually stated proof for testing.

\end{statements}



\subsection{Conversions from values to terms}

The following are useful for constructing indexed variables:

\begin{statements}

\item "[[ eager define int2string ( t , v ) as newline if v > 0 then << 0 :: int2string1 ( v , "" ) :: t debug >> else newline if v = 0 then << 0 :: "0" :: t debug >> else newline << 0 :: 256 * int2string1 ( - v , "" ) + logand ( "-" , 255 ) :: t debug >> end define ]]"

\item "[[ eager define int2string1 ( v , r ) as newline if v = 0 then r else newline let z = logand ( "0" , 255 ) in newline let x :: y = floor ( v , 10 ) in newline int2string1 ( x , 256 * r + z + y ) end define ]]"

\item "[[ eager define val2term ( t , v ) as newline if v = true then back t quote true end quote else newline if v = false then back t quote false end quote else newline if v pairp then back t quote val2term ( t , v head ) unquote :: val2term ( t , v tail ) unquote end quote else newline if v mapp then back t quote map ( --- ) end quote else newline if v objectp then back t quote object ( val2term ( t , destruct ( v ) ) unquote ) end quote else if v = 0 then back t quote 0 end quote else newline if v < 0 then back t quote - card2term ( t , - v ) unquote end quote else newline card2term ( t , v ) end define ]]"

\item "[[ eager define card2term ( t , v ) as newline if v = 0 then back t quote %% end quote else newline if evenp ( v ) then back t quote card2term ( t , half ( v ) ) unquote %0 end quote else back t quote card2term ( t , half ( v ) ) unquote %1 end quote end define ]]".

\end{statements}



\subsection{Unification}

\begin{statements}

\item "[[ eager define univar ( t , v , i ) as back t quote unifresh ( v unquote , int2string ( t , i ) unquote ) end quote end define ]]"

\item "[[ eager define pterm ( t , c ) as pterm1 ( t , true , 1 , c ) end define ]]".

We shall refer to terms in which some of the bound meta variables are replaced by fresh variables indexed by numbers as \index{term, parameter}\index{parameter term}\intro{parameter terms}. "[[ pterm ( t , c ) ]]" replaces meta variables bound at the top level in "[[ t ]]". The function is used e.g.\ on instances of lemmas in proofs before unification. That allows to recognize instantiable meta variables after their associated quantifiers have been removed. "[[ c ]]" should be the cache of the page.

\item "[[ eager define pterm1 ( t , s , n , c ) as newline let d = t metadef ( c ) in newline if d != "all" then pterm2 ( t , s , c ) else newline let v = univar ( t first , t first , n ) in newline let t prime = pterm1 ( t second , ( t first :: v ) :: s , n + 1 , c ) in newline back t quote All v unquote : t prime unquote end quote end define ]]".

\item "[[ eager define pterm2 ( t , s , c ) as newline let d = t metadef ( c ) in newline let s = if d = "all" then ( t first :: t first ) :: s else s in newline if d != "var" then t head :: pterm2* ( t tail , s , c ) else newline let n = lookup ( t , s , true ) in newline if n = true then t else n end define ]]"

\item "[[ eager define pterm2* ( t , s , c ) as newline if t atom then true else newline pterm2 ( t head , s , c ) :: pterm2* ( t tail , s , c ) end define ]]"

\item "[[ eager define inst ( t , d , a ) as newline if .not. t r= quote unifresh ( true , true ) end quote then ( t ref :: t idx :: d debug ) :: inst* ( t tail , d , a ) else newline let u = a [[ t second idx ]] in if u != true then inst ( u , d , a ) else newline error ( d , diag ( "Incomplete unification. Uninstantiated variable:" ) disp ( t ) end diagnose ) end define ]]".

Instantiate the parameter term "[[ t ]]" as specified by the array "[[ a ]]". May loop indefinitely. As an example, a substitution which maps "[[ #x ]]" to "[[ #x :: #x ]]" will keep expanding "[[ #x ]]" forever. We shall say that a substitution is \index{circular substitution}\index{substitution, circular}\intro{circular} if there exists a term "[[ t ]]" for which "[[ inst ( t , d , x ) ]]" loops indefinitely.

\item "[[ eager define inst* ( t , d , a ) as if t atom then true else inst ( t head , d , a ) :: inst* ( t tail , d , a ) end define ]]".

\item "[[ eager define occur ( t , u , s ) as newline if u r= quote unifresh ( true , true ) end quote then t t= u .or. occur ( t , s [[ u second idx ]] , s ) else newline occur* ( t , u tail , s ) end define ]]".

True if "[[ t ]]" occurs in "[[ inst ( u , d , s ) ]]". May loop indefinitely if "[[ s ]]" is circular.

\item "[[ eager define occur* ( t , u , s ) as newline if u atom then false else occur ( t , u head , s ) .or. occur* ( t , u tail , s ) end define ]]".

\item "[[ eager define unify ( t , u , s ) as newline if t r= quote unifresh ( true , true ) end quote then unify2 ( t , u , s ) else newline if u r= quote unifresh ( true , true ) end quote then unify2 ( u , t , s ) else newline if t r= u then unify* ( t tail , u tail , s ) else newline error ( t , diag ( "Unable to unify" ) disp ( t ) diag ( "with" ) disp ( u ) end diagnose ) end define ]]".

If possible, return the `smallest' substitution which contains "[[ s ]]" and unifies the parameter terms "[[ t ]]" and "[[ u ]]", i.e.\ a substitution which, if applied to "[[ t ]]" and "[[ u ]]" yield identical terms. Raise an exception if unification is impossible.

\item "[[ eager define unify* ( t , u , s ) as newline if t atom then s else newline unify* ( t tail , u tail , unify ( t head , u head , s ) ) end define ]]".

\item "[[ eager define unify2 ( t , u , s ) as newline if t t= u then s else newline let t prime = s [[ t second idx ]] in newline if t prime != true then unify ( t prime , u , s ) else newline if occur ( t , u , s ) then exception else s [[ t second idx -> u ]] end define ]]".

Does the same as "[[ unify ( t , u , s ) ]]" but only when "[[ t ]]" is a number.

\end{statements}



\subsection{Hooks for the tactic state}

\begin{statements}

\item "[[ eager define hook-arg as "arg" end define ]]"

Argumentation hook. States returned from tactic or unitac evaluation contain the returned argumentation on this hook.

\item "[[ eager define hook-res as "con" end define ]]"

Result hook. States returned from tactic or unitac evaluation contain the expected conclusion on this hook.

\item "[[ eager define hook-idx as "idx" end define ]]"

Index hook. During unitac evaluation, the index hook contains an accumulating index used for generating fresh variables.

\item "[[ eager define hook-uni as "uni" end define ]]"

Unification hook. During unitac evaluation, the result of unification is accumulated here.

\item "[[ eager define hook-pre as "pre" end define ]]"

Premise hook. Premises are stacked here during tactic evaluation. Premises may be explicitly assumed premises, the conclusion of the left hand side of a cut, or a theory assumed at the beginning of a proofs. Elements of the premise hook have form "[[ l :: p :: x ]]" where "[[ l ]]" is a label for referring to the premise, "[[ p ]]" is the premise itself, and "[[ x ]]" may be used by individual tactics.

\item "[[ eager define hook-cond as "cond" end define ]]"

Condition hook. Side conditions are stacked here during tactic evaluation.

\item "[[ eager define hook-parm as "parm" end define ]]"

Parameter hook. Tactic evaluation of "[[ x at y ]]" stacks "[[ y ]]" on the parameter hook. Tactic evaluation of "[[ All x : y ]]" unstacks. Useful for parameterized tactics.

\end{statements}



\subsection{Tactic evaluation}

\begin{statements}

\item "[[ eager define taceval ( t , s , c ) as newline let d = t tactic-rhs ( c ) in newline if .not. d then ( eval ( d , true , c ) apply << t ,, s ,, c >> maptag ) untag else newline let << r ,, a >> = lookup ( t , s [[ hook-pre ]] , true ) in newline if .not. a then s [[ hook-res -> r ]] [[ hook-arg -> a ]] else newline error ( t , newline diag ( "Unknown tactic operator in root of argumentation:" ) newline disp ( t ) end diagnose ) end define ]]".

Evaluate the `tactic' aspect of "[[ t ]]".

\item "[[ eager define tactic-push ( n , v , s ) as newline s [[ n -> v :: s [[ n ]] ]] end define ]]"

Push the value "[[ v ]]" onto the stack named "[[ n ]]" in the tactic state "[[ s ]]".

\item "[[ eager define tactic-pop ( n , s ) as newline s [[ n -> s [[ n ]] tail ]] end define ]]"

Pop a value from the stack named "[[ n ]]" in the tactic state "[[ s ]]" and return the new state (not the popped value).

\item "[[ eager define taceval1 ( t , p , c ) as newline let d = t tactic-rhs ( c ) in newline let t = back t quote t unquote infer p unquote end quote in newline if d then taceval ( t , tacstate0 , c ) else newline ( eval ( d , true , c ) apply << t ,, tacstate0 ,, c >> maptag ) untag end define ]]"

Evaluate the `tactic' aspect of "[[ t infer p ]]" using the tactic definition of "[[ t ]]". If "[[ t ]]" has no tactic definition then use taceval.

\end{statements}



\subsection{Proof macros}

\begin{statements}

\item "[[ macro define x lemma y : z end lemma as ensure math statement define y as x infer z end define,unitac define y as \ u . unitac-lemma ( u ) end define end math end define ]]".

A lemma declaration is the same as a statement definition plus a unitac definition which says how to sequent-prove a lemma plus what the lemma concludes.

\item "[[ macro define proof of x : y as ensure math define proof of x as \ p . \ c . taceval ( quote y end quote , tacstate0 , c ) end define end math end define ]]".

A proof is the same as a proof definition.

\item "[[ macro define x proof of y : z as ensure math define proof of y as \ p . \ c . taceval1 ( quote x end quote , quote z end quote , c ) end define end math end define ]]".

Assume "[[ x ]]", then prove "[[ y ]]" using the proof "[[ z ]]". If "[[ x ]]" has a tactic definition then that tactic is applied to the entire proof.

\end{statements}



\subsection{Proof line macros}

\begin{statements}

\item "[[ macro define line l : a >> x ; as a conclude x end define ]]"

\item "[[ macro define line l : a >> x qed as a conclude x end define ]]"

\item "[[ macro define line l : Arbitrary >> x ; n as All x : n end define ]]"

\item "[[ macro define line l : Local >> x = y ; n as let x := y in n end define ]]"

\end{statements}



\section{Tactic definitions of sequent operators}

\subsection{Init tactic}

\begin{statements}

\item "[[ tactic define x Init as \ u . tactic-Init ( u ) end define ]]".

\item "[[ eager define tactic-Init ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, x >> = t in newline s [[ hook-arg -> t ]] [[ hook-res -> x ]] end define ]]"

\end{statements}



\subsection{Ponens tactic}

\begin{statements}

\item "[[ tactic define x Ponens as \ u . tactic-Ponens ( u ) end define ]]".

\item "[[ eager define tactic-Ponens ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, x >> = t in newline let s = taceval ( x , s , c ) in newline let a = back t quote s [[ hook-arg ]] unquote Ponens end quote in newline let r = s [[ hook-res ]] in newline if mismatch ( quote x infer y end quote , r , c ) then newline error ( t , diag ( "Ponens tactic used on non-inference:" ) disp ( r ) end diagnose ) else newline s [[ hook-arg -> a ]] [[ hook-res -> r second ]] end define ]]"

\end{statements}



\subsection{Probans tactic}

\begin{statements}

\item "[[ tactic define x Probans as \ u . tactic-Probans ( u ) end define ]]".

\item "[[ eager define tactic-Probans ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, x >> = t in newline let s = taceval ( x , s , c ) in newline let a = back t quote s [[ hook-arg ]] unquote Probans end quote in newline let r = s [[ hook-res ]] in newline if mismatch ( quote x endorse y end quote , r , c ) then newline error ( t , diag ( "Probans tactic used on non-endorsement:" ) disp ( r ) end diagnose ) else newline s [[ hook-arg -> a ]] [[ hook-res -> r second ]] end define ]]"

\end{statements}



\subsection{Verify tactic}

\begin{statements}

\item "[[ tactic define x Verify as \ u . tactic-Verify ( u ) end define ]]".

\item "[[ eager define tactic-Verify ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, x >> = t in newline let s = taceval ( x , s , c ) in newline let a = back t quote s [[ hook-arg ]] unquote Verify end quote in newline let r = s [[ hook-res ]] in newline if mismatch ( quote x endorse y end quote , r , c ) then newline error ( t , diag ( "Verify tactic used on non-endorsement:" ) disp ( r ) end diagnose ) else newline s [[ hook-arg -> a ]] [[ hook-res -> r second ]] end define ]]"

\end{statements}



\subsection{Curry tactic}

\begin{statements}

\item "[[ tactic define x Curry as \ u . tactic-Curry ( u ) end define ]]".

\item "[[ eager define tactic-Curry ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, x >> = t in newline let s = taceval ( x , s , c ) in newline let a = back t quote s [[ hook-arg ]] unquote Curry end quote in newline let r = s [[ hook-res ]] in newline if mismatch ( quote ( x oplus y ) infer z end quote , r , c ) then newline error ( t , diag ( "Curry tactic used on unfit argument:" ) disp ( r ) end diagnose ) else newline let r = back r quote r first first unquote infer r first second unquote infer r second unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Uncurry tactic}

\begin{statements}

\item "[[ tactic define x Uncurry as \ u . tactic-Uncurry ( u ) end define ]]".

\item "[[ eager define tactic-Uncurry ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, x >> = t in newline let s = taceval ( x , s , c ) in newline let a = back t quote s [[ hook-arg ]] unquote Uncurry end quote in newline let r = s [[ hook-res ]] in newline if mismatch ( quote x infer y infer z end quote , r , c ) then newline error ( t , diag ( "Uncurry tactic used on unfit argument:" ) disp ( r ) end diagnose ) else newline let r = back r quote ( r first unquote oplus r second first unquote ) infer r second second unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Deref tactic}

\begin{statements}

\item "[[ tactic define x Deref as \ u . tactic-Deref ( u ) end define ]]".

\item "[[ eager define tactic-Deref ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, x >> = t in newline let s = taceval ( x , s , c ) in newline let a = back t quote s [[ hook-arg ]] unquote Deref end quote in newline let r = s [[ hook-res ]] in newline let r prime = r stmt-rhs ( c ) in newline if r prime = true then newline error ( t , diag ( "Deref tactic used on undefined statement:" ) disp ( r ) end diagnose ) else newline s [[ hook-arg -> a ]] [[ hook-res -> r prime ]] end define ]]"

\end{statements}



\subsection{At tactic}

Accumulate instantiations on the ``parameters'' stack. To do multiple instantiations in parallel, "[[ tactic-at1 ( t , s , v , c ) ]]" accumulates instantiations on the "[[ v ]]" list and then "[[ tactic-at2 ( t , s , v , s prime , c ) ]]" accumulates instantiations on the "[[ s prime ]]" association list of substitutions to be performed in parallel.

\begin{statements}

\item "[[ tactic define x at y as \ u . tactic-at ( u ) end define ]]".

\item "[[ eager define tactic-at ( u ) as newline let << t ,, s ,, c >> = u in tactic-at1 ( t , s , true , c ) end define ]]"

\item "[[ eager define tactic-at1 ( t , s , v , c ) as newline if mismatch ( quote x at y end quote , t , c ) then newline tactic-at2 ( t , taceval ( t , s , c ) , v , true , c ) else newline let << true ,, x ,, y >> = t in newline let s = tactic-push ( hook-parm , y , s ) in newline tactic-at1 ( x , s , y :: v , c ) end define ]]"

\item "[[ eager define tactic-at2 ( t , s , v , s prime , c ) as newline if v then s [[ hook-res -> metasubst ( s [[ hook-res ]] , s prime , c ) ]] else newline let y :: v = v in newline let a = back t quote s [[ hook-arg ]] unquote at y unquote end quote in newline let r = s [[ hook-res ]] in newline if mismatch ( quote All x : y end quote , r , c ) then newline error ( t , diag ( "At tactic used on non-quantifier:" ) disp ( r ) end diagnose ) else newline let s = s [[ hook-arg -> a ]] [[ hook-res -> r second ]] in newline tactic-at2 ( t , s , v , ( r first :: y ) :: s prime , c ) end define ]]"

\end{statements}



\subsection{Infer tactic}

Accumulate premises on the ``premises'' stack.

\begin{statements}

\item "[[ tactic define x infer y as \ u . tactic-infer ( u ) end define ]]".

\item "[[ eager define tactic-infer ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, x ,, y >> = t in newline let s = tactic-push ( hook-pre , << true ,, x ,, back x quote x unquote Init end quote >> , s ) in newline let s = taceval ( y , s , c ) in newline let a = back t quote x unquote infer s [[ hook-arg ]] unquote end quote in newline let r = back t quote x unquote infer s [[ hook-res ]] unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Endorse tactic}

Accumulate side conditions on the ``conditions'' stack.

\begin{statements}

\item "[[ tactic define x endorse y as \ u . tactic-endorse ( u ) end define ]]".

\item "[[ eager define tactic-endorse ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, x ,, y >> = t in newline let s = taceval ( y , tactic-push ( hook-cond , << true ,, x >> , s ) , c ) in newline let a = back t quote x unquote endorse s [[ hook-arg ]] unquote end quote in newline let r = back t quote x unquote endorse s [[ hook-res ]] unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Id est tactic}

\begin{statements}

\item "[[ tactic define x id est y as \ u . tactic-ie ( u ) end define ]]".

\item "[[ eager define tactic-ie ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, x ,, y >> = t in newline let s = taceval ( x , s , c ) in newline let a = back t quote s [[ hook-arg ]] unquote id est y unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> y ]] end define ]]"

\end{statements}



\subsection{All tactic}

Pop instantiations from the ``parameters'' stack.

\begin{statements}

\item "[[ tactic define All x : y as \ u . tactic-all ( u ) end define ]]".

\item "[[ eager define tactic-all ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, x ,, y >> = t in newline let s = taceval ( y , tactic-pop ( hook-parm , s ) , c ) in newline let a = back t quote All x unquote : s [[ hook-arg ]] unquote end quote in newline let r = back t quote All x unquote : s [[ hook-res ]] unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Cut tactic}

Accumulate conclusions of left hand sides of cuts on the ``premises'' stack.

\begin{statements}

\item "[[ tactic define x ;; y as \ u . tactic-cut ( u ) end define ]]".

\item "[[ eager define tactic-cut ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, x ,, y >> = t in newline let s prime = taceval ( x , s , c ) in newline let a = s prime [[ hook-arg ]] in newline let r = s prime [[ hook-res ]] in newline let s = tactic-push ( hook-pre , << true ,, r ,, back r quote r unquote Init end quote >> , s ) in newline let s = taceval ( y , s , c ) in newline let a = back t quote a unquote ;; s [[ hook-arg ]] unquote end quote in newline s [[ hook-arg -> a ]] end define ]]"

\end{statements}



\section{Unification tactic}

\subsection{Main definitions}

\begin{statements}

\item "[[ tactic define a conclude a prime as \ x . unitac ( x ) end define ]]".

Proof tactic which tries to modify the argumentation "[[ a ]]" so that it proves the term "[[ a prime ]]". The tactic adds missing "[[ x at y ]]", "[[ x Ponens ]]", and "[[ x Verify ]]" operations and determines the "[[ y ]]" in "[[ x at y ]]" using unification.



\item "[[ eager define unitac ( x ) as newline let << t ,, s ,, c >> = x in newline let e :: v = unitac1 ( t , s , c ) catch in newline if .not. e then v else newline if .not. v then error ( t , LocateProofLine ( t , c ) v ) else newline error ( t , newline LocateProofLine ( t , c ) newline diag ( "During unification: Uncaught exception" ) newline end diagnose ) end define ]]"

Hand the term "[[ t ]]" of form "[[ a conclude a prime ]]", the tactic state "[[ s ]]", and the codex "[[ c ]]" to unitac1. Locate any errors found by unitac1.



\item "[[ eager define unitac1 ( t , s , c ) as newline let s = s [[ hook-idx -> 1 ]] [[ hook-uni -> true ]] in newline let s = unieval ( t , s , c ) in newline let t = inst ( s [[ hook-arg ]] , t , s [[ hook-uni ]] ) in newline let e :: v = taceval ( t , s , c ) catch in if .not. e then v else newline if .not. v then v raise else newline error ( t , newline diag ( "Post unification tactic evalutation: Uncaught exception" ) newline end diagnose ) end define ]]"

Call unieval to unitac expand the proof term "[[ t ]]" to a unification and an uninstantiated argumentation. The unification and argumentation are added to the state "[[ s ]]". "[[ c ]]" is the cache. Then instantiate the argumentation and do usual tactic expansion.

\end{statements}



\subsection{Adaption}

\begin{statements}

\item "[[ eager define unitac-adapt ( t , s , c ) as newline if t = "var" then s else newline let a = s [[ hook-arg ]] in newline let r = s [[ hook-res ]] in newline let d = r metadef ( c ) in newline if d = "var" then s else newline if d = t then s else newline if d = "infer" then newline unitac-adapt ( t , s [[ hook-arg -> back a quote a unquote Ponens end quote ]] [[ hook-res -> r second ]] , c ) else newline if d = "endorse" then newline unitac-adapt ( t , s [[ hook-arg -> back a quote a unquote Verify end quote ]] [[ hook-res -> r second ]] , c ) else newline if d = "all" then newline let i = s [[ hook-idx ]] in newline let s = s [[ hook-idx -> i + 1 ]] in newline let v = univar ( a , r first , i ) in newline let r prime = metasubst ( r second , << r first :: v >> , c ) in newline unitac-adapt ( t , s [[ hook-arg -> back a quote a unquote at v unquote end quote ]] [[ hook-res -> r prime ]] , c ) else newline if t then s else newline error ( a , newline diag ( "Cannot convert" ) disp ( r ) newline diag ( "to type ``" ) diag ( t ) diag ( "''" ) end diagnose ) end define ]]".

Add Ponens, Verify, and At operations to the argumentation inside "[[ s ]]" until the root of the conclusion is of type "[[ t ]]". As examples, "[[ t ]]" could be ``infer'', ``endorse'', ``all'', ``var'' or "[[ true ]]". In the latter case, a maximum of Ponens, Verify, and At operations are added. When "[[ t ]]" is ``var'', a minimum of operators are added (meaning that "[[ s ]]" is returned unchanged).

\end{statements}



\subsection{Unitac evaluation}

\begin{statements}

\item "[[ eager define unieval ( t , s , c ) as newline let d = t unitac-rhs ( c ) in newline if d then newline let << r ,, a >> = lookup ( t , s [[ hook-pre ]] , true ) in newline if .not. a then s [[ hook-arg -> a ]] [[ hook-res -> r ]] else newline error ( t , newline diag ( "Unknown unitac operator in root of argumentation:" ) newline disp ( t ) end diagnose ) else newline let e :: s = ( eval ( d , true , c ) apply << t ,, s ,, c >> maptag ) untag catch in newline if .not. e then s else newline if .not. s then s raise else newline error ( t , newline diag ( "Exception raised by the unitac aspect of:" ) disp ( t ) end diagnose ) end define ]]"

Unitac expand the argumentation "[[ t ]]" to a unification, an uninstantiated argumentation, and an expected conclusion. The unification, argumentation, and conclusion are added to the state "[[ s ]]" as "[[ s [[ hook-uni ]] ]]", "[[ s [[ hook-arg ]] ]]", and "[[ s [[ hook-res ]] ]]", respectively. "[[ c ]]" is the cache.

During unitac expansion, fresh variables are generated using "[[ univar ( t prime , v , s [[ hook-idx ]] ) ]]" where "[[ s [[ hook-idx ]] ]]" is supposed to be a unique index. "[[ v ]]" is the varible which receives the unique index and debugging information is taken from "[[ t prime ]]". The index is supposed to guarantee uniqueness in itself. The purpose of "[[ v ]]" is to make error messages more readable.

\end{statements}



\section{Unitac definitions}

\subsection{Init}

\begin{statements}

\item "[[ unitac define x Init as \ u . unitac-Init ( u ) end define ]]"

\item "[[ eager define unitac-Init ( u ) as newline let << t ,, s ,, c >> = u in newline s [[ hook-res -> t first ]] [[ hook-arg -> t ]] end define ]]"

If "[[ t ]]" has form "[[ r Init ]]" then the conclusion is "[[ r ]]" and the argumentation is "[[ r Init ]]".

\end{statements}



\subsection{Ponens}

\begin{statements}

\item "[[ unitac define x Ponens as \ u . unitac-Ponens ( u ) end define ]]"

\item "[[ unitac define x ponens y as \ u . unitac-ponens ( u ) end define ]]"

\item "[[ eager define unitac-Ponens ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let s = unitac-adapt ( "infer" , s , c ) in newline let a = s [[ hook-arg ]] in newline let r = s [[ hook-res ]] in newline s [[ hook-arg -> back t quote a unquote Ponens end quote ]] [[ hook-res -> r second ]] end define ]]"

If the argumentation has form "[[ a Ponens ]]" then convert the argumentation "[[ a ]]" into something whose conclusion "[[ r ]]" is expected to be of form "[[ x infer y ]]".

\item "[[ eager define unitac-ponens ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let s = unitac-adapt ( "infer" , s , c ) in newline let a = s [[ hook-arg ]] in newline let r = s [[ hook-res ]] in newline let s = unieval ( t second , s , c ) in newline let s = unitac-adapt ( r first metadef ( c ) , s , c ) in newline let a prime = s [[ hook-arg ]] in newline let r prime = s [[ hook-res ]] in newline let u = s [[ hook-uni ]] in newline let u = unify ( r first , r prime , u ) in newline let s = s [[ hook-uni -> u ]] in newline s [[ hook-arg -> back t quote a prime unquote ;; a unquote Ponens end quote ]] [[ hook-res -> r second ]] end define ]]"

If the argumentation has form "[[ a ponens a prime ]]" then convert "[[ a ]]" into something whose result is expected to be of form "[[ x infer y ]]". Convert "[[ a prime ]]" into something whose result is expected to be of form "[[ r prime ]]". Unify "[[ x ]]" with "[[ r prime ]]" and return argumentation "[[ ( a prime ;; a Ponens ) ]]" and conclusion "[[ y ]]".

\end{statements}



\subsection{Probans}

\begin{statements}

\item "[[ unitac define x Probans as \ u . unitac-Probans ( u ) end define ]]"

\item "[[ unitac define x probans y as \ u . unitac-probans ( u ) end define ]]"

\item "[[ eager define unitac-Probans ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let s = unitac-adapt ( "endorse" , s , c ) in newline let a = s [[ hook-arg ]] in newline let r = s [[ hook-res ]] in newline s [[ hook-arg -> back t quote a unquote Probans end quote ]] [[ hook-res -> r second ]] end define ]]"

If the argumentation has form "[[ a probans p ]]" then convert the argumentation "[[ a ]]" into something whose conclusion "[[ r ]]" is expected to be of form "[[ x endorse y ]]".

\item "[[ eager define unitac-probans ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let s = unitac-adapt ( "endorse" , s , c ) in newline let a = s [[ hook-arg ]] in newline let r = s [[ hook-res ]] in newline let u = s [[ hook-uni ]] in newline let << p >> = lookup ( t second , s [[ hook-cond ]] , << t second >> ) in newline let u = unify ( r first , p , u ) in newline let s = s [[ hook-uni -> u ]] in newline s [[ hook-arg -> back t quote a unquote Probans end quote ]] [[ hook-res -> r second ]] end define ]]"

If the argumentation has form "[[ a probans s ]]" then convert "[[ a ]]" into something whose result is expected to be of form "[[ x endorse y ]]". Unify "[[ x ]]" with "[[ s ]]" and return argumentation "[[ a Probans ]]" and conclusion "[[ y ]]".

\end{statements}



\subsection{Verify}

\begin{statements}

\item "[[ unitac define x Verify as \ u . unitac-Verify ( u ) end define ]]"

\item "[[ unitac define x verify y as \ u . unitac-verify ( u ) end define ]]"

\item "[[ eager define unitac-Verify ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let s = unitac-adapt ( "endorse" , s , c ) in newline let a = s [[ hook-arg ]] in newline let r = s [[ hook-res ]] in newline s [[ hook-arg -> back t quote a unquote Verify end quote ]] [[ hook-res -> r second ]] end define ]]"

If the argumentation has form "[[ a Verify ]]" then convert the argumentation "[[ a ]]" into something whose conclusion "[[ r ]]" is expected to be of form "[[ x endorse y ]]".

\item "[[ eager define unitac-verify ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let s = unitac-adapt ( "endorse" , s , c ) in newline let a = s [[ hook-arg ]] in newline let r = s [[ hook-res ]] in newline let u = s [[ hook-uni ]] in newline let u = unify ( r first , t second , u ) in newline let s = s [[ hook-uni -> u ]] in newline s [[ hook-arg -> back t quote a unquote Verify end quote ]] [[ hook-res -> r second ]] end define ]]"

If the argumentation has form "[[ a verify s ]]" then convert "[[ a ]]" into something whose result is expected to be of form "[[ x endorse y ]]". Unify "[[ x ]]" with "[[ s ]]" and return argumentation "[[ a Verify ]]" and conclusion "[[ y ]]".

\end{statements}



\subsection{Curry and decurry}

\begin{statements}

\item "[[ unitac define x Curry as \ u . unitac-Curry ( u ) end define ]]"

\item "[[ unitac define x Uncurry as \ u . unitac-Uncurry ( u ) end define ]]"

\item "[[ eager define unitac-Curry ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let s = unitac-adapt ( "infer" , s , c ) in newline let a = s [[ hook-arg ]] in newline let r = s [[ hook-res ]] in newline if .not. r first r= quote x oplus y end quote then newline error ( r , diag ( "Unsuited for currying:" ) disp ( r ) end diagnose ) else newline let r = back r quote r first first infer r first second infer r second end quote in newline s [[ hook-arg -> back t quote a unquote Curry end quote ]] [[ hook-res -> r ]] end define ]]"

If the argumentation has form "[[ a Curry ]]" then convert the argumentation "[[ a ]]" into something with conclusion "[[ x oplus y infer z ]]" and return conclusion "[[ x infer y infer z ]]".

\item "[[ eager define unitac-Uncurry ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let s = unitac-adapt ( "infer" , s , c ) in newline let a = s [[ hook-arg ]] in newline let r = s [[ hook-res ]] in newline if .not. r second r= quote x infer y end quote then newline error ( r , diag ( "Unsuited for uncurrying:" ) disp ( r ) end diagnose ) else newline let r = back r quote ( r first oplus r second first ) infer r second second end quote in newline s [[ hook-arg -> back t quote a unquote Uncurry end quote ]] [[ hook-res -> r ]] end define ]]"

If the argumentation has form "[[ a Uncurry ]]" then convert the argumentation "[[ a ]]" into something with conclusion "[[ x infer y infer z ]]" and return conclusion "[[ ( x oplus y ) infer z ]]".

\end{statements}



\subsection{At}

\begin{statements}

\item "[[ unitac define x At as \ u . unitac-At ( u ) end define ]]"

\item "[[ unitac define x at y as \ u . unitac-at ( u ) end define ]]"

\item "[[ eager define unitac-At ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let s = unitac-adapt ( "all" , s , c ) in newline let a = s [[ hook-arg ]] in newline let r = s [[ hook-res ]] in newline let i = s [[ hook-idx ]] in newline let s = s [[ hook-idx -> i + 1 ]] in newline let v = univar ( a , r first , i ) in newline let a = back t quote a unquote at v unquote end quote in newline let r = metasubst ( r second , << r first :: v >> , c ) in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

If the argumentation has form "[[ a At ]]" then convert "[[ a ]]" into something whose conclusion is expected to be of form "[[ All x : y ]]". Then replace "[[ x ]]" by a fresh variable "[[ v ]]" in "[[ y ]]" and return argumentation "[[ a at v ]]" and conclusion "[[ y ]]".

\item "[[ eager define unitac-at ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let s = unitac-adapt ( "all" , s , c ) in newline let a = s [[ hook-arg ]] in newline let r = s [[ hook-res ]] in newline let i = s [[ hook-idx ]] in newline let s = s [[ hook-idx -> i + 1 ]] in newline let v = univar ( a , r first , i ) in newline let a = back t quote a unquote at v unquote end quote in newline let r = metasubst ( r second , << r first :: v >> , c ) in newline let u = s [[ hook-uni ]] in newline let u = unify ( t second , v , u ) in newline let s = s [[ hook-uni -> u ]] in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

If the argumentation has form "[[ a at a prime ]]" then convert "[[ a ]]" into something whose conclusion is expected to be of form "[[ All x : y ]]". Then replace "[[ x ]]" by a fresh variable "[[ v ]]" in "[[ y ]]", unify "[[ v ]]" with "[[ a prime ]]", and return argumentation "[[ a at v ]]" and conclusion "[[ y ]]".

\end{statements}



\subsection{Reference and dereference}

\begin{statements}

\item "[[ unitac define x Deref as \ u . unitac-Deref ( u ) end define ]]"

\item "[[ eager define unitac-Deref ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let s = unitac-adapt ( true , s , c ) in newline let r = s [[ hook-res ]] in newline let l = r stmt-rhs ( c ) in newline if l then s else newline let a = s [[ hook-arg ]] in newline let a = back t quote a unquote Deref end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> l ]] end define ]]"

\item Let "[[ r ]]" be the conclusion of "[[ t first ]]". "[[ r ]]" is supposed to be a lemma. Let "[[ l ]]" be the contents of that lemma. Use "[[ l ]]" as conclusion of "[[ t first Deref ]]".

\item "[[ unitac define x id est y as \ u . unitac-idest ( u ) end define ]]"

\item "[[ eager define unitac-idest ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let l = t second stmt-rhs ( c ) in newline let s = unitac-adapt ( l metadef ( c ) , s , c ) in newline let r = s [[ hook-res ]] in newline let u = s [[ hook-uni ]] in newline let u = unify ( r , l , u ) in newline let s = s [[ hook-uni -> u ]] in newline let a = s [[ hook-arg ]] in newline let a = back t quote a unquote id est t second unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> t second ]] end define ]]"

\item Let "[[ l ]]" be the contents of the lemma named "[[ t second ]]". Unify the conclusion "[[ r ]]" of "[[ t first ]]" with "[[ l ]]" and take "[[ t second ]]" to be the conclusion of "[[ t first id est t second ]]".

\end{statements}



\subsection{Infer}

\begin{statements}

\item "[[ unitac define x Infer as \ u . unitac-Infer ( u ) end define ]]"

\item "[[ eager define unitac-Infer ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let i = s [[ hook-idx ]] in newline let s = s [[ hook-idx -> i + 1 ]] in newline let v = univar ( t , quote cla end quote , i ) in newline let r = s [[ hook-res ]] in newline let a = s [[ hook-arg ]] in newline let r = back t quote v unquote infer r unquote end quote in newline let a = back t quote v unquote infer a unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\item "[[ unitac define x infer y as \ u . unitac-infer ( u ) end define ]]"

\item "[[ eager define unitac-infer ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t second , s , c ) in newline let r = s [[ hook-res ]] in newline let a = s [[ hook-arg ]] in newline let r = back t quote t first unquote infer r unquote end quote in newline let a = back t quote t first unquote infer a unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Endorse}

\begin{statements}

\item "[[ unitac define x Endorse as \ u . unitac-Endorse ( u ) end define ]]"

\item "[[ eager define unitac-Endorse ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let i = s [[ hook-idx ]] in newline let s = s [[ hook-idx -> i + 1 ]] in newline let v = univar ( t , quote cla end quote , i ) in newline let r = s [[ hook-res ]] in newline let a = s [[ hook-arg ]] in newline let r = back t quote v unquote endorse r unquote end quote in newline let a = back t quote v unquote endorse a unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\item "[[ unitac define x endorse y as \ u . unitac-endorse ( u ) end define ]]"

\item "[[ eager define unitac-endorse ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t second , s , c ) in newline let r = s [[ hook-res ]] in newline let a = s [[ hook-arg ]] in newline let r = back t quote t first unquote endorse r unquote end quote in newline let a = back t quote t first unquote endorse a unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{All}

\begin{statements}

\item "[[ unitac define x All as \ u . unitac-All ( u ) end define ]]"

\item "[[ eager define unitac-All ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let i = s [[ hook-idx ]] in newline let s = s [[ hook-idx -> i + 1 ]] in newline let v = univar ( t , quote cla end quote , i ) in newline let r = s [[ hook-res ]] in newline let a = s [[ hook-arg ]] in newline let r = back t quote All v unquote : r unquote end quote in newline let a = back t quote All v unquote : a unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\item "[[ unitac define All x : y as \ u . unitac-all ( u ) end define ]]"

\item "[[ eager define unitac-all ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t second , s , c ) in newline let r = s [[ hook-res ]] in newline let a = s [[ hook-arg ]] in newline let r = back t quote All t first unquote : r unquote end quote in newline let a = back t quote All t first unquote : a unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Cut}

\begin{statements}

\item "[[ unitac define x ;; y as \ u . unitac-cut ( u ) end define ]]"

\item "[[ eager define unitac-cut ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let a prime = s [[ hook-arg ]] in newline let s = unieval ( t second , s , c ) in newline let r = s [[ hook-res ]] in newline let a = s [[ hook-arg ]] in newline let a = back t quote a prime unquote ;; a unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Unary conclude}

The "[[ x Conclude ]]" operator adds Ponens, Verify, and At operations to the argumentation inside "[[ x ]]" until all occurrences of "[[ u infer v ]]", "[[ u endorse v ]]", and "[[ All u : v ]]" have been removed. One may think of "[[ x Conclude ]]" as a unary version of "[[ x conclude y ]]" in which "[[ y ]]" is missing but for which it is known that "[[ y ]]" is an object term.

\begin{statements}

\item "[[ unitac define x Conclude as \ u . unitac-Conclude ( u ) end define ]]"

\item "[[ eager define unitac-Conclude ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline unitac-adapt ( true , s , c ) end define ]]"

If "[[ t ]]" has form "[[ a Conclude ]]" then find the conclusion "[[ r ]]" of "[[ a ]]", add as many "[[ x at y ]]", "[[ x Ponens ]]", and "[[ x Verify ]]" operations as possible, and return "[[ a :: r :: u ]]".

\end{statements}



\section{Lemmas, rules, and proof lines}

Lemmas, rules, and proof lines do not always say what they seem to say. As an example, a lemma stating that "[[ x = x ]]" in Mendelsons "[[ System S ]]" does not say "[[ x = x ]]". Rather, it says "[[ System S infer x = x ]]". As another example, if one allows the use of deduction in FOL-based proofs then a proof line proving e.g. "[[ x + 1 = 0 + ( x + 1 ) ]]" under the hypothesis "[[ x = 0 + x ]]" really proves "[[ x = 0 + x p.imply x + 1 = 0 + ( x + 1 ) ]]". Or, rather, it proves "[[ System S infer x = 0 + x p.imply x + 1 = 0 + ( x + 1 ) ]]" if the proof is stated in "[[ System S ]]".

No single way of handling lemmas, rules, and proofs will satisfy all theories. As an example, deduction in FOL is different from deduction in map theory, and for that reason those two theories need different ways of treating proof lines in hypothetical proofs.

For that reason, the way lemmas, rules, and proofs are treated is embedded in the tactic state.



\subsection{The initial tactic state}

The initial tactic state "[[ tacstate0 ]]" contains "[[ unitac0 ]]". "[[ unitac0 ]]" in turn defines how to treat lemmas, rules, and proof lines during unitac evaluation. The definition of "[[ tacstate0 ]]" reads:

\begin{statements}

\item "[[ eager define hook-unitac as "unitac" end define ]]"

\item "[[ eager define tacstate0 as true [[ hook-unitac -> unitac0 ]] end define ]]"

\end{statements}

\noindent The "[[ unitac0 ]]" structure defines how to handle lemmas, rules, and proof lines during unitac evaluation. Handling of proof lines really means how to handle the conclude construct "[[ x conclude y ]]".

\begin{statements}

\item "[[ eager define hook-lemma as "lemma" end define ]]"

\item "[[ eager define hook-rule as "rule" end define ]]"

\item "[[ eager define hook-conclude as "conclude" end define ]]"

\item "[[ eager define unitac0 as true [[ hook-lemma -> quote \ u . unitac-lemma-std ( u ) end quote ]] [[ hook-rule -> quote \ u . unitac-rule-std ( u ) end quote ]] [[ hook-conclude -> quote \ u . unitac-conclude-std ( u ) end quote ]] end define ]]".

\end{statements}



\subsection{Conclude}

\begin{statements}

\item "[[ unitac define x conclude y as \ u . unitac-conclude ( u ) end define ]]"

\item "[[ eager define unitac-conclude ( u ) as newline let << t ,, s ,, c >> = u in newline let d = s [[ hook-unitac ]] [[ hook-conclude ]] in newline ( eval ( d , true , c ) apply << t ,, s ,, c >> maptag ) untag end define ]]"

\item "[[ eager define unitac-conclude-std ( u ) as newline let << t ,, s ,, c >> = u in newline let s = unieval ( t first , s , c ) in newline let s = unitac-adapt ( t second metadef ( c ) , s , c ) in newline let u = unify ( s [[ hook-res ]] , t second , s [[ hook-uni ]] ) in newline s [[ hook-uni -> u ]] [[ hook-res -> t second ]] end define ]]"

If "[[ t ]]" has form "[[ t first conclude t second ]]" then convert "[[ t first ]]" into something whose conclusion fits "[[ t second ]]". Unify the conclusion with "[[ t second ]]" and return the resulting state "[[ s ]]".

\end{statements}



\subsection{Rules}

We define two rule tactics: "[[ x Rule ]]" for explicit use and "[[ unitac-rule ( x ) ]]" which is implicitly attached to axioms and inference rules. The ``implicit attachment'' is done by the axiom and rule macros. As an example of use, "[[ p.A1 Rule ]]" explicitly proves "[[ p.A1 ]]" whereas "[[ p.A1 ]]" implicitly proves "[[ All #a ,, #b : A p.imply B p.imply A ]]". Note that the former proves the name and the latter proves the contents of "[[ p.A1 ]]".

\begin{statements}

\item "[[ unitac define r Rule as \ u . unitac-Rule ( u ) end define ]]"

\item "[[ eager define unitac-Rule ( x ) as newline let << t ,, s ,, c >> = x in newline let r = t first in newline let a = unitac-theo ( r , s , c ) in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"



\item "[[ eager define unitac-rule ( u ) as newline let << t ,, s ,, c >> = u in newline let d = s [[ hook-unitac ]] [[ hook-rule ]] in newline ( eval ( d , true , c ) apply << t ,, s ,, c >> maptag ) untag end define ]]"

\item "[[ eager define unitac-rule-std ( x ) as newline let << t ,, s ,, c >> = x in newline let r = t stmt-rhs ( c ) in newline let a = unitac-theo ( t , s , c ) in newline let a = back r quote a unquote Deref end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\item "[[ eager define unitac-theo ( t , s , c ) as newline let p = reverse ( s [[ hook-pre ]] ) in newline unitac-rule0 ( t , p , c ) end define ]]"

Construct a proof of the rule "[[ t ]]" assuming the premisses contained in the tactic state "[[ s ]]". Complain if no proof is found.

\item "[[ eager define unitac-rule0 ( r , P , c ) as newline let p = unitac-rule1 ( r , P , c ) in newline if .not. p then p else newline if r metadef ( c ) = "plus" then unitac-rule-plus ( r , P , c ) else newline let d = r stmt-rhs ( c ) in newline if .not. d then unitac-rule-stmt ( d , r , P , c ) else newline error ( r , newline diag ( "No locally assumed theory includes the following rule:" ) disp ( r ) newline end diagnose ) end define ]]"

Construct a proof of the rule "[[ r ]]" assuming the premisses "[[ P ]]". Complain if no proof is found. The function first tries to find "[[ r ]]" verbatim among the premisses (where each premise is tree searched). If no proof is found, "[[ r ]]" is decomposed.

\item "[[ eager define unitac-rule-plus ( R , P , c ) as newline let << true ,, r ,, r prime >> = R in newline let p = unitac-rule0 ( r , P , c ) in newline if p then true else newline let p prime = unitac-rule0 ( r prime , P , c ) in newline if p prime then true else back R quote p unquote ;; p prime unquote ;; ( ( r unquote oplus r prime unquote ) infer ( r unquote oplus r prime unquote ) Init ) Curry Ponens Ponens end quote end define ]]"

Construct a proof of the rule "[[ R ]]" of form "[[ r oplus r prime ]]" assuming the premisses "[[ P ]]". Return "[[ true ]]" if no proof is found.

\item "[[ eager define unitac-rule-stmt ( d , r , P , c ) as newline let p = unitac-rule0 ( d , P , c ) in newline if p then true else newline back r quote p unquote ;; d unquote Init id est r unquote end quote end define ]]"

Construct a proof of the rule "[[ r ]]" with definition "[[ d ]]" assuming the premisses "[[ P ]]". Return "[[ true ]]" if no proof is found.

\item "[[ eager define unitac-rule1 ( r , P , c ) as newline if P atom then true else newline unitac-rule2 ( r , P head first , c ) .and. newline unitac-rule1 ( r , P tail , c ) end define ]]"

Construct a proof of the rule "[[ r ]]" assuming the premisses "[[ P ]]". Return "[[ true ]]" if the rule is not found among the premisses.

\item "[[ eager define unitac-rule2 ( r , T , c ) as newline let p = unitac-search ( r , T , c ) in newline if p then true else newline unitac-rule3 ( r , p ) end define ]]"

Construct a proof of the rule "[[ r ]]" assuming the theory "[[ T ]]". Sequent evaluating the proof gives "[[ << << T >> ,, true ,, r prime >> ]]" where "[[ r prime ]]" is what the rule with name "[[ r ]]" says. Return "[[ true ]]" if no proof is found (i.e.\ if the rule does not belong to the theory).



\item "[[ eager define unitac-search ( r , T , c ) as newline unitac-search1 ( r , T , true , << T >> , c ) catch tail end define ]]".

Search for the rule "[[ r ]]" in the theory "[[ T ]]" and return the ``path'' of "[[ r ]]". Return "[[ true ]]" is "[[ r ]]" is not found.

A path is a non-empty list of ``addresses''. An address is a pair of a tree and a list of ``edges''. Each edge is one of the strings ``head'' and ``tail''. As an example, the address "[[ << ( x oplus y ) oplus z ,, "head" ,, "tail" >> ]]" points out the "[[ y ]]" in the tree "[[ ( x oplus y ) oplus z ]]".

A path "[[ << a ,, b >> ]]" adresses some term "[[ a prime ]]" which, when dereferenced, is supposed to be the starting point of "[[ b ]]". As an example, "[[ << << p.Prop oplus p.A3 ,, "head" >> ,, << p.A1 oplus p.A2 oplus p.MP ,, "tail" ,, "head" >> >> ]]" is a path to "[[ p.A2 ]]" within "[[ p.Prop oplus p.A3 ]]".

The path is returned in reverse order.



\item "[[ eager define unitac-search1 ( r , T , p , a , c ) as newline if r t= T then ( reverse ( a ) :: p ) raise else newline let T prime = T stmt-rhs ( c ) in newline if .not. T prime then unitac-search1 ( r , T prime , reverse ( a ) :: p , << T prime >> , c ) else newline if T metadef ( c ) != "plus" then true else newline unitac-search1 ( r , T first , p , "head" :: a , c ) .and. newline unitac-search1 ( r , T second , p , "tail" :: a , c ) end define ]]".

Search for "[[ r ]]" in "[[ T ]]" and throw the path of "[[ r ]]" when found. Return "[[ true ]]" if "[[ r ]]" is not found. Accumulate the path in "[[ p ]]" in reverse order and the addresses in "[[ a ]]" in reverse order. The path is returned in reverse order.



\item "[[ eager define unitac-rule3 ( r , p ) as newline let q = unitac-rule4 ( r , p head ) in newline if p tail then q else let p = unitac-rule3 ( r , p tail ) in newline back r quote p unquote Deref ;; q unquote end quote end define ]]"



\item "[[ eager define unitac-rule4 ( r , a ) as newline let p = unitac-rule5 ( r , a head , a tail , true ) in newline back r quote p unquote Ponens end quote end define ]]".

Given an address "[[ T :: a ]]", construct a proof which generates the sequent "[[ << << T >> ,, true ,, a prime >> ]]" where "[[ a prime ]]" is the conjunct at address "[[ a ]]" in conjunction "[[ T ]]".



\item "[[ eager define unitac-rule5 ( r , T , a , s ) as newline if a atom then newline let p = unitac-stack ( r , s , back r quote T unquote Init end quote ) in back r quote T unquote infer p unquote end quote else let e :: a = a in newline if e = "head" then newline back r quote unitac-rule5 ( r , T first , a , T second :: s ) unquote Uncurry end quote else newline back r quote ( T first unquote infer unitac-rule5 ( r , T second , a , s ) unquote ) Uncurry end quote end define ]]".

Given a conjunction "[[ T ]]" and a list "[[ a ]]" of edges, prove "[[ T infer a prime ]]" where "[[ a prime ]]" is the conjunct at address "[[ a ]]".



\item "[[ eager define unitac-stack ( r , s , t ) as newline if s atom then t else newline let p :: s = s in newline let t = unitac-stack ( r , s , t ) in newline back r quote p unquote infer t unquote end quote end define ]]".

Add the premisses on the stack "[[ s ]]" to the term "[[ t ]]".

\end{statements}



\subsection{Lemmas}

\begin{statements}

\item "[[ eager define unitac-lemma ( u ) as newline let << t ,, s ,, c >> = u in newline let d = s [[ hook-unitac ]] [[ hook-lemma ]] in newline ( eval ( d , true , c ) apply << t ,, s ,, c >> maptag ) untag end define ]]"

\item "[[ eager define unitac-lemma-std ( x ) as newline let << t ,, s ,, c >> = x in newline let << true ,, T ,, r >> = t stmt-rhs ( c ) in newline let a prime = unitac-theo ( T , s , c ) in newline let a = back t quote a prime unquote ;; t unquote Init Deref Ponens end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]".

Define how to sequent prove a lemma and what the lemma concludes.

\end{statements}



\section{Tactic definitions of proof line constructs}

\subsection{Conclude-cut lines}

\begin{statements}

\item "[[ macro define line l : a >> x ; n as Line l : a >> x ; n end define ]]"

\item "[[ tactic define Line l : a >> x ; n as \ u . tactic-conclude-cut ( u ) end define ]]"

\item "[[ eager define tactic-conclude-cut ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, l ,, a ,, x ,, n >> = t in newline let s prime = taceval ( back t quote a unquote conclude x unquote end quote , s , c ) in newline let a prime = s prime [[ hook-arg ]] in newline let r = s prime [[ hook-res ]] in newline let s = tactic-push ( hook-pre , << l ,, r ,, back r quote r unquote Init end quote >> , s ) in newline let s = taceval ( n , s , c ) in newline let a = s [[ hook-arg ]] in newline s [[ hook-arg -> back t quote a prime unquote ;; a unquote end quote ]] end define ]]"

\end{statements}



\subsection{Premise line}

\begin{statements}

\item "[[ macro define line l : Premise >> x ; n as Line l : Premise >> x ; n end define ]]"

\item "[[ tactic define Line l : Premise >> x ; n as \ u . tactic-premise-line ( u ) end define ]]"

\item "[[ eager define tactic-premise-line ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, l ,, x ,, n >> = t in newline let s = taceval ( n , tactic-push ( hook-pre , << l ,, x ,, back x quote x unquote Init end quote >> , s ) , c ) in newline let a = back t quote x unquote infer s [[ hook-arg ]] unquote end quote in newline let r = back t quote x unquote infer s [[ hook-res ]] unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Condition line}

\begin{statements}

\item "[[ macro define line l : Condition >> x ; n as Line l : Condition >> x ; n end define ]]"

\item "[[ tactic define Line l : Condition >> x ; n as \ u . tactic-condition-line ( u ) end define ]]"

\item "[[ eager define tactic-condition-line ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, l ,, x ,, n >> = t in newline let s = taceval ( n , tactic-push ( hook-cond , << l ,, x >> , s ) , c ) in newline let a = back t quote x unquote endorse s [[ hook-arg ]] unquote end quote in newline let r = back t quote x unquote endorse s [[ hook-res ]] unquote end quote in newline s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Blocks}

\begin{statements}

\item "[[ macro define line l : Block >> Begin ; x line k : Block >> End ; n as Line l : Block >> Begin ; x line k : Block >> End ; n end define ]]"

\item "[[ tactic define Line l : Block >> Begin ; x line k : Block >> End ; n as \ u . tactic-block ( u ) end define ]]"

\item "[[ eager define tactic-block ( u ) as newline let << t ,, s ,, c >> = u in newline let << true ,, l ,, x ,, k ,, n >> = t in newline let s prime = taceval ( x , s , c ) in newline let a prime = s prime [[ hook-arg ]] in newline let r = s prime [[ hook-res ]] in newline let s = tactic-push ( hook-pre , << k ,, r ,, back r quote r unquote Init end quote >> , s ) in newline let s = taceval ( n , s , c ) in newline let a = s [[ hook-arg ]] in newline s [[ hook-arg -> back t quote a prime unquote ;; a unquote end quote ]] end define ]]"

\end{statements}



\section{Sample proofs}

\subsection{Propositional Calculus}

We now define Propositional Calculus ("[[ p.Prop ]]") as in \cite{Mendelson}. We also define Intuitionistic Propositional Calculus ("[[ p.IProp ]]").

"[ axiom p.A1 : All #x ,, #y : #x p.imply #y p.imply #x end axiom ]"

"[ axiom p.A2 : All #x ,, #y ,, #z : ( #x p.imply #y p.imply #z ) p.imply ( #x p.imply #y ) p.imply #x p.imply #z end axiom ]"

"[ axiom p.A3 : All #x ,, #y : ( p.not #y p.imply p.not #x ) p.imply ( p.not #y p.imply #x ) p.imply #y end axiom ]"

"[ rule p.MP : All #x ,, #y : #x p.imply #y infer #x infer #y end rule ]"

"[ theory p.IProp : p.A1 oplus p.A2 oplus p.MP end theory ]"

"[ theory p.Prop : p.IProp oplus p.A3 end theory ]"

\noindent The inference rule of Modus Ponens ("[[ p.MP ]]") is typically applied to two arguments, so we introduce a macro for that:

"[[[ macro define x p.mp y as p.MP ponens x ponens y Conclude end define ]]]"

\noindent In the macro, "[[ y Conclude ]]" is argument "[[ y ]]" from which all occurences of "[[ All #u : #v ]]", "[[ #u infer #v ]]", and "[[ #u endorse #v ]]" are stripped by applications of "[[ #a at #b ]]", "[[ #a Ponens ]]", and "[[ #a Verify ]]", respectively. Stripping is done during tactic evaluation. The macro does not strip "[[ x ]]" since that happens automatically: During tactic evaluation, the "[[ p.MP ]]" rules forces "[[ x ]]" to be of form "[[ #x p.imply #y ]]" which causes "[[ x ]]" to be stripped.

As an example of a proof, take the first lemma proved in \cite{Mendelson}:



"[ p.Prop lemma lemma2 : All #x : #x p.imply #x end lemma ]"

"[ p.Prop proof of lemma2 : line L01 : Arbitrary >> #x ; line L02 : p.A2 >> ( #x p.imply ( #y p.imply #x ) p.imply #x ) p.imply newline ( #x p.imply #y p.imply #x ) p.imply #x p.imply #x ; line L03 : p.A1 >> #x p.imply ( #y p.imply #x ) p.imply #x ; line L04 : L02 p.mp L03 >> ( #x p.imply #y p.imply #x ) p.imply #x p.imply #x ; line L05 : p.A1 >> #x p.imply #y p.imply #x ; line L06 : L04 p.mp L05 >> #x p.imply #x qed ]"

\noindent We may leave more work to unification simply by omitting line "[[ L02 ]]" and "[[ L03 ]]":

"[ p.Prop lemma lemma2a : All #x : #x p.imply #x end lemma ]"

"[ p.Prop proof of lemma2a : line L01 : Arbitrary >> #x ; line L04 : p.A2 p.mp p.A1 >> ( #x p.imply #y p.imply #x ) p.imply #x p.imply #x ; line L05 : p.A1 >> #x p.imply #y p.imply #x ; line L06 : L04 p.mp L05 >> #x p.imply #x qed ]"

\noindent We may state the proof even shorter as follows:

"[ p.Prop lemma lemma2b : All #x : #x p.imply #x end lemma ]"

"[ p.Prop proof of lemma2b : line L01 : Arbitrary >> #x ; line L05 : p.A1 >> #x p.imply #y p.imply #x ; line L06 : p.A2 p.mp p.A1 p.mp L05 >> #x p.imply #x qed ]"

\noindent It would be tempting to change the argumentation of line "[[ L06 ]]" to "[[ p.A2 p.mp p.A1 p.mp p.A1 ]]", but then unification would be unable to determine how to instantiate the second quantifier of "[[ p.A1 ]]". We may specify that instantiation explicitly, though:

"[ p.Prop lemma lemma2c : All #x : #x p.imply #x end lemma ]"

"[ p.Prop proof of lemma2c : line L01 : Arbitrary >> #x ; line L06 : p.A2 p.mp p.A1 p.mp ( p.A1 At at #y ) >> #x p.imply #x qed ]"

\noindent In the proof above, "[[ p.A1 At ]]" tells unification to instantiate the first quantifier of "[[ p.A1 ]]" suitably. "[[ p.A1 At at #y ]]" tells unification to instantiate the first quantifier suitably and to instantiate the second one to "[[ #y ]]".

Line "[[ L01 ]]" above applies the generalization sequent operator "[[ All #x : #y ]]" to the rest of the proof. The same effect may be achieved by putting that operator in the argumentation of line "[[ L06 ]]". But then one must also add a meta-quantifier to the conclusion of line "[[ L06 ]]". The "[[ All #x : #y ]]" construct happens to denote both the generalization sequent operator and the meta-quantifier:

"[ p.Prop lemma lemma2d : All #x : #x p.imply #x end lemma ]"

"[ p.Prop proof of lemma2d : line L06 : All #x : p.A2 p.mp p.A1 p.mp ( p.A1 At at #y ) >> All #x : #x p.imply #x qed ]"

\noindent One may even leave to unification to guess the quantified variable:

"[ p.Prop lemma lemma2e : All #x : #x p.imply #x end lemma ]"

"[ p.Prop proof of lemma2e : line L06 : ( p.A2 p.mp p.A1 p.mp ( p.A1 At at #y ) ) All >> All #x : #x p.imply #x qed ]"

\noindent The theory part of a lemma and a proof may be stated as a conjunction in an arbitrary order. Each conjunct may be a rule or a theory, where each theory recursively may be an arbitrary conjunction of rules and theories. As an example, "[[ p.IProp oplus p.A3 ]]" contains the rules "[[ p.A1 ]]", "[[ p.A2 ]]", "[[ p.A3 ]]", and "[[ p.MP ]]" which makes the following lemma and proof correct:

"[ p.IProp oplus p.A3 lemma lemma2f : All #x : #x p.imply #x end lemma ]"

"[ p.IProp oplus p.A3 proof of lemma2f : line L01 : Arbitrary >> #x ; line L06 : p.A2 p.mp p.A1 p.mp ( p.A1 At at #y ) >> #x p.imply #x qed ]"



\subsection{Blocks}

Blocks allow subproofs inside other proofs. The following example stress test the block concept in that it first proves that any statement "[[ #x ]]" implies itself, then applies that to the statement itself. The proof is much like applying the identity function to itself which of course yeilds the identity function.

"[ p.Prop lemma lemma3 : All #x : #x infer #x end lemma ]"

"[ p.Prop proof of lemma3 : line L01 : Block >> Begin ; line L02 : Arbitrary >> #x ; line L03 : Premise >> #x ; line L04 : L03 >> #x ; line L05 : Block >> End ; line L06 : L05 ponens L05 >> All #x : #x infer #x qed ]"



\subsection{System S}

For the sake of testing we introduce a small subset of Mendelsons System S. For historical reasons, this system is used in the Logiweb test suites.

"[ theory System S : S.S1 oplus S.S5 end theory ]"

"[ rule S.S1 : All #x ,, #y ,, #z : #x = #y infer #x = #z infer #y = #z end rule ]"

"[ rule S.S5 : All #x : #x + 0 = #x end rule ]"

"[ System S lemma S.reflexivity : All #x : #x = #x end lemma ]"

"[ System S proof of S.reflexivity : line L01 : Arbitrary >> #x ; line L02 : S.S5 >> #x + 0 = #x ; line L03 : S.S1 ponens L02 ponens L02 >> #x = #x qed ]"



\subsection{Rules}



"[ p.Prop lemma lemma4a : p.IProp end lemma ]"

"[ p.Prop proof of lemma4a : line L01 : p.IProp Rule >> p.IProp qed ]"



"[ p.Prop lemma lemma4b : p.A1 end lemma ]"

"[ p.Prop proof of lemma4b : line L01 : p.A1 Rule >> p.A1 qed ]"



"[ p.Prop lemma lemma4c : p.A2 end lemma ]"

"[ p.Prop proof of lemma4c : line L01 : p.A2 Rule >> p.A2 qed ]"



"[ p.Prop lemma lemma4d : p.A3 end lemma ]"

"[ p.Prop proof of lemma4d : line L01 : p.A3 Rule >> p.A3 qed ]"



"[ p.IProp oplus p.A3 lemma lemma4e : p.Prop end lemma ]"

"[ p.IProp oplus p.A3 proof of lemma4e : line L01 : p.Prop Rule >> p.Prop qed ]"



"[ p.IProp lemma lemma4f : p.A3 infer p.Prop end lemma ]"

"[ p.IProp proof of lemma4f : line L01 : Premise >> p.A3 ; line L02 : p.Prop Rule >> p.Prop qed ]"



"[ p.IProp lemma lemma4g : p.A3 infer x p.imply x end lemma ]"

"[ p.IProp proof of lemma4g : line L01 : Premise >> p.A3 ; line L02 : lemma2 >> x p.imply x qed ]"



\printindex



\bibliography{./page}



\end{document}
" end text ,, latex ( "page" ) ,, makeindex ( "page" ) ,, bibtex ( "page" ) ,, latex ( "page" ) ,, makeindex ( "page" ) ,, latex ( "page" ) ,, dvipdfm ( "page" ) ,, text "chores.tex" : "\documentclass[fleqn]{article}

% Include definitions generated by pyk
\input{lgwinclude}

% Make latexsym characters available
\usepackage{latexsym}

% Ensure reasonable rendering of strings
\everymath{\rm}
\everydisplay{\rm}

% Enable generation of an index
\usepackage{makeidx}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}

% Enable generation of a bibliography
\bibliographystyle{plain}

% Enable hyperlinks
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle=A Logiweb proof checker - chores}
\hypersetup{colorlinks=true}

% Construct for listing statements with associated explanations
\newenvironment{statements}{\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}}{\end{list}}

\begin{document}
\title{A Logiweb proof checker - chores}
\author{Klaus Grue}
\maketitle
\tableofcontents



\section{\TeX\ definitions}

\begin{statements}

\item "[[ tex define alpha as "
\alpha " end define ]]"

\item "[[ tex define beta as "
\beta " end define ]]"

\item "[[ tex define gamma as "
\gamma " end define ]]"

\item "[[ tex define delta as "
\delta " end define ]]"

\item "[[ tex define epsilon as "
\epsilon " end define ]]"

\item "[[ tex define varepsilon as "
\varepsilon " end define ]]"

\item "[[ tex define zeta as "
\zeta " end define ]]"

\item "[[ tex define eta as "
\eta " end define ]]"

\item "[[ tex define theta as "
\theta " end define ]]"

\item "[[ tex define vartheta as "
\vartheta " end define ]]"

\item "[[ tex define iota as "
\iota " end define ]]"

\item "[[ tex define kappa as "
\kappa " end define ]]"

\item "[[ tex define lambda as "
\lambda " end define ]]"

\item "[[ tex define mu as "
\mu " end define ]]"

\item "[[ tex define nu as "
\nu " end define ]]"

\item "[[ tex define xi as "
\xi " end define ]]"

\item "[[ tex define pi as "
\pi " end define ]]"

\item "[[ tex define varpi as "
\varpi " end define ]]"

\item "[[ tex define rho as "
\rho " end define ]]"

\item "[[ tex define varrho as "
\varrho " end define ]]"

\item "[[ tex define sigma as "
\sigma " end define ]]"

\item "[[ tex define varsigma as "
\varsigma " end define ]]"

\item "[[ tex define tau as "
\tau " end define ]]"

\item "[[ tex define upsilon as "
\upsilon " end define ]]"

\item "[[ tex define phi as "
\phi " end define ]]"

\item "[[ tex define chi as "
\chi " end define ]]"

\item "[[ tex define psi as "
\psi " end define ]]"

\item "[[ tex define omega as "
\omega " end define ]]"

\item "[[ tex define Gamma as "
\Gamma " end define ]]"

\item "[[ tex define Delta as "
\Delta " end define ]]"

\item "[[ tex define Theta as "
\Theta " end define ]]"

\item "[[ tex define Lambda as "
\Lambda " end define ]]"

\item "[[ tex define Xi as "
\Xi " end define ]]"

\item "[[ tex define Pi as "
\Pi " end define ]]"

\item "[[ tex define Sigma as "
\Sigma " end define ]]"

\item "[[ tex define Upsilon as "
\Upsilon " end define ]]"

\item "[[ tex define Phi as "
\Phi " end define ]]"

\item "[[ tex define Psi as "
\Psi " end define ]]"

\item "[[ tex define Omega as "
\Omega " end define ]]"

\item "[[ tex define cla as "{\cal A}" end define ]]"

\item "[[ tex define clb as "{\cal B}" end define ]]"

\item "[[ tex define clc as "{\cal C}" end define ]]"

\item "[[ tex define cld as "{\cal D}" end define ]]"

\item "[[ tex define cle as "{\cal E}" end define ]]"

\item "[[ tex define clf as "{\cal F}" end define ]]"

\item "[[ tex define clg as "{\cal G}" end define ]]"

\item "[[ tex define clh as "{\cal H}" end define ]]"

\item "[[ tex define cli as "{\cal I}" end define ]]"

\item "[[ tex define clj as "{\cal J}" end define ]]"

\item "[[ tex define clk as "{\cal K}" end define ]]"

\item "[[ tex define cll as "{\cal L}" end define ]]"

\item "[[ tex define clm as "{\cal M}" end define ]]"

\item "[[ tex define cln as "{\cal N}" end define ]]"

\item "[[ tex define clo as "{\cal O}" end define ]]"

\item "[[ tex define clp as "{\cal P}" end define ]]"

\item "[[ tex define clq as "{\cal Q}" end define ]]"

\item "[[ tex define clr as "{\cal R}" end define ]]"

\item "[[ tex define cls as "{\cal S}" end define ]]"

\item "[[ tex define clt as "{\cal T}" end define ]]"

\item "[[ tex define clu as "{\cal U}" end define ]]"

\item "[[ tex define clv as "{\cal V}" end define ]]"

\item "[[ tex define clw as "{\cal W}" end define ]]"

\item "[[ tex define clx as "{\cal X}" end define ]]"

\item "[[ tex define cly as "{\cal Y}" end define ]]"

\item "[[ tex define clz as "{\cal Z}" end define ]]"

\item "[[ tex define statement as "
stmt" end define ]]"

\item "[[ tex define proof as "
proof" end define ]]"

\item "[[ tex define statement define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{stmt}{=} "[ texname y end texname ]"
]" end define ]]"

\item "[[ tex define proof define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{proof}{=} "[ texname y end texname ]"
]" end define ]]"

\item "[[ tex define meta define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{meta}{=} "[ texname y end texname ]"
]" end define ]]"

\item "[[ tex define math define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{math}{=} "[ texname y end texname ]"
]" end define ]]"

\item "[[ tex define tactic define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{tactic}{=} "[ texname y end texname ]"
]" end define ]]"

\item "[[ tex define unitac define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{unitac}{=} "[ texname y end texname ]"
]" end define ]]"

\item "[[ tex define locate define x as y end define as "
[ "[ texname x end texname ]"
\stackrel{locate}{=} "[ y ]"
]" end define ]]"

\item "[[ tex define ensure math x end math as "
\ensuremath{ "[ x ]"
}" end define ]]"

\item "[[ tex name define ensure math x end math as "
\backslash ensuremath \{ "[ x ]"
\}" end define ]]"

\item "[[ tex define #a as "
\mathsf{a}" end define ]]"

\item "[[ tex define #b as "
\mathsf{b}" end define ]]"

\item "[[ tex define #c as "
\mathsf{c}" end define ]]"

\item "[[ tex define #d as "
\mathsf{d}" end define ]]"

\item "[[ tex define #e as "
\mathsf{e}" end define ]]"

\item "[[ tex define #f as "
\mathsf{f}" end define ]]"

\item "[[ tex define #g as "
\mathsf{g}" end define ]]"

\item "[[ tex define #h as "
\mathsf{h}" end define ]]"

\item "[[ tex define #i as "
\mathsf{i}" end define ]]"

\item "[[ tex define #j as "
\mathsf{j}" end define ]]"

\item "[[ tex define #k as "
\mathsf{k}" end define ]]"

\item "[[ tex define #l as "
\mathsf{l}" end define ]]"

\item "[[ tex define #m as "
\mathsf{m}" end define ]]"

\item "[[ tex define #n as "
\mathsf{n}" end define ]]"

\item "[[ tex define #o as "
\mathsf{o}" end define ]]"

\item "[[ tex define #p as "
\mathsf{p}" end define ]]"

\item "[[ tex define #q as "
\mathsf{q}" end define ]]"

\item "[[ tex define #r as "
\mathsf{r}" end define ]]"

\item "[[ tex define #s as "
\mathsf{s}" end define ]]"

\item "[[ tex define #t as "
\mathsf{t}" end define ]]"

\item "[[ tex define #u as "
\mathsf{u}" end define ]]"

\item "[[ tex define #v as "
\mathsf{v}" end define ]]"

\item "[[ tex define #w as "
\mathsf{w}" end define ]]"

\item "[[ tex define #x as "
\mathsf{x}" end define ]]"

\item "[[ tex define #y as "
\mathsf{y}" end define ]]"

\item "[[ tex define #z as "
\mathsf{z}" end define ]]"

\item "[[ tex define False as "
\mathrel{\makebox[0mm][l]{$\bot$}\,{\bot}}" end define ]]"

\item "[[ tex define p.A1 as "
A1" end define ]]"

\item "[[ tex define p.A2 as "
A2" end define ]]"

\item "[[ tex define p.A3 as "
A3" end define ]]"

\item "[[ tex define p.MP as "
MP" end define ]]"

\item "[[ tex define p.Prop as "
Prop" end define ]]"

\item "[[ tex define p.IProp as "
IProp" end define ]]"



\item "[[ tex define x# as ""[ x ]"
{}^{\#}" end define ]]"



\item "[[ tex define x member y as ""[ x ]"
\in "[ y ]"" end define ]]"



\item "[[ tex define p.not x as "
\neg "[ x ]"" end define ]]"



\item "[[ tex define x p.imply y as ""[ x ]"
\Rightarrow "[ y ]"" end define ]]"



\item "[[ tex define metadeclare x as "
meta\ \linebreak [0]"[ x ]"" end define ]]"



\item "[[ tex define x Init as ""[ x ]"
{}^I " end define ]]"

\item "[[ tex define x Ponens as ""[ x ]"
{}^{\rhd} " end define ]]"

\item "[[ tex define x Probans as ""[ x ]"
{\makebox[0mm][l]{${}^\rhd$}\,{}^\rhd} " end define ]]"

\item "[[ tex define x Verify as ""[ x ]"
{}^{\ast} " end define ]]"

\item "[[ tex define x Curry as ""[ x ]"
{}^C " end define ]]"

\item "[[ tex define x Uncurry as ""[ x ]"
{}^U " end define ]]"

\item "[[ tex define x Deref as ""[ x ]"
{}^D " end define ]]"

\item "[[ tex define x At as ""[ x ]"
{}^@ " end define ]]"

\item "[[ tex define x Infer as ""[ x ]"
{}^{\vdash} " end define ]]"

\item "[[ tex define x Endorse as ""[ x ]"
{\makebox[0mm][l]{${}^\vdash$}\,{}^\vdash} " end define ]]"

\item "[[ tex define x All as ""[ x ]"
{}^{\Pi} " end define ]]"

\item "[[ tex define x Conclude as ""[ x ]"
{}^{\gg}" end define ]]"



\item "[[ tex define x at y as ""[ x ]"
\mathrel{@} "[ y ]"" end define ]]"

\item "[[ tex define x ponens y as ""[ x ]"
\rhd "[ y ]"" end define ]]"

\item "[[ tex define x probans y as ""[ x ]"
\mathrel{\makebox[0mm][l]{$\rhd$}\,{\rhd}} "[ y ]"" end define ]]"

\item "[[ tex define x infer y as ""[ x ]"
\vdash "[ y ]"" end define ]]"

\item "[[ tex define x endorse y as ""[ x ]"
\mathrel{\makebox[0mm][l]{$\vdash$}\,{\vdash}} "[ y ]"" end define ]]"

\item "[[ tex define x id est y as ""[ x ]"
\mathrel{ie} "[ y ]"" end define ]]"

\item "[[ tex define x verify y as ""[ x ]"
\mathrel{\ast} "[ y ]"" end define ]]"

\item "[[ tex define x conclude y as ""[ x ]"
\gg "[ y ]"" end define ]]"

\item "[[ tex define x p.mp y as ""[ x ]"
\unrhd "[ y ]"" end define ]]"



\item "[[ tex define All x : y as "
\Pi "[ x ]"
\colon "[ y ]"" end define ]]"



\item "[[ tex define x oplus y as ""[ x ]"
\oplus "[ y ]"" end define ]]"



\item "[[ tex define line x : y >> z ; u as "
\newline%
\makebox[0.1\textwidth]{}%
\parbox[b]{0.4\textwidth}{\raggedright%
\makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}%
$"[ y ]" {} \gg {}$}%
\parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}%
$"[ z ]"$\hfill
\makebox[0mm][l]{\quad ;}} "[ u ]"" end define ]]"

\item "[[ tex name define line x : y >> z ; u as "
L "[ x ]"
\colon "[ y ]"
\gg "[ z ]"
; "[ u ]"" end define ]]"

\item "[[ tex define line x : y >> z ; as "
\newline%
\makebox[0.1\textwidth]{}%
\parbox[b]{0.4\textwidth}{\raggedright%
\makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}%
$"[ y ]" {} \gg {}$}%
\parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}%
$"[ z ]"$\hfill
\makebox[0mm][l]{\quad ;}}" end define ]]"

\item "[[ tex name define line x : y >> z ; as "
L "[ x ]"
\colon "[ y ]"
\gg "[ z ]"
;" end define ]]"

\item "[[ tex define line x : y >> z qed as "
\newline%
\makebox[0.1\textwidth]{}%
\parbox[b]{0.4\textwidth}{\raggedright%
\makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}%
$"[ y ]" {} \gg {}$}%
\parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}%
$"[ z ]"$\hfill
\makebox[0mm][l]{\quad $\Box$}}" end define ]]"

\item "[[ tex name define line x : y >> z qed as "
L "[ x ]"
\colon "[ y ]"
\gg "[ z ]"
\Box" end define ]]"

\item "[[ tex define line x : Premise >> z ; u as "
\newline%
\makebox[0.1\textwidth]{}%
\parbox[b]{0.4\textwidth}{\raggedright%
\makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}%
$Premise {} \gg {}$}%
\parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}%
$"[ z ]"$\hfill
\makebox[0mm][l]{\quad ;}} "[ u ]"" end define ]]"

\item "[[ tex name define line x : Premise >> z ; u as "
L "[ x ]"
\colon Premise
\gg "[ z ]"
; "[ u ]"" end define ]]"

\item "[[ tex define line x : Condition >> z ; u as "
\newline%
\makebox[0.1\textwidth]{}%
\parbox[b]{0.4\textwidth}{\raggedright%
\makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}%
$Condition {} \gg {}$}%
\parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}%
$"[ z ]"$\hfill
\makebox[0mm][l]{\quad ;}} "[ u ]"" end define ]]"

\item "[[ tex name define line x : Condition >> z ; u as "
L "[ x ]"
\colon Condition
\gg "[ z ]"
; "[ u ]"" end define ]]"

\item "[[ tex define line x : Arbitrary >> z ; u as "
\newline%
\makebox[0.1\textwidth]{}%
\parbox[b]{0.4\textwidth}{\raggedright%
\makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}%
$Arbitrary {} \gg {}$}%
\parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}%
$"[ z ]"$\hfill
\makebox[0mm][l]{\quad ;}} "[ u ]"" end define ]]"

\item "[[ tex name define line x : Arbitrary >> z ; u as "
L "[ x ]"
\colon Arbitrary
\gg "[ z ]"
; "[ u ]"" end define ]]"

\item "[[ tex define line x : Local >> y = z ; u as "
\newline%
\makebox[0.1\textwidth]{}%
\parbox[b]{0.4\textwidth}{\raggedright%
\makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}%
$Local {} \gg {}$}%
\parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}%
$"[ y ]" \mathrel{\ddot{=}} "[ z ]"$\hfill
\makebox[0mm][l]{\quad ;}} "[ u ]"" end define ]]"

\item "[[ tex name define line x : Local >> y = z ; u as "
L "[ x ]"
\colon Local
\gg "[ y ]" \mathrel{\ddot{=}} "[ z ]"
; "[ u ]"" end define ]]"

\item "[[ tex define line x : Block >> Begin ; y line z : Block >> End ; u as "
\newline%
\makebox[0.1\textwidth]{}%
\parbox[b]{0.4\textwidth}{\raggedright%
\makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}%
$Block {} \gg {}$}%
\parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}%
$Begin$\hfill
\makebox[0mm][l]{\quad ;}}\addtolength{\indentation}{1em} "[ y ]"
\newline\addtolength{\indentation}{-1em}%
\makebox[0.1\textwidth]{}%
\parbox[b]{0.4\textwidth}{\raggedright%
\makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ z ]"{:}$}}%
$Block {} \gg {}$}%
\parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}%
$End$\hfill
\makebox[0mm][l]{\quad ;}} "[ u ]"" end define ]]"

\item "[[ tex name define line x : Block >> Begin ; y line z : Block >> End ; u as "
L "[ x ]"
\colon Block \gg Begin ; \quad "[ y ]"
\quad L "[ z ]"
\colon Block \gg End ; "[ u ]"" end define ]]"

\item "[[ tex define prepare proof indentation as "
\ifx\indentation\undefined
\newlength{\indentation}\setlength{\indentation}{0em}
\fi" end define ]]"

\item "[[ tex name define prepare proof indentation as "
prepare\ proof\ indentation" end define ]]"



\item "[[ tex define x ;; y as ""[ x ]"
; "[ y ]"" end define ]]"



\item "[[ tex define axiom x : y end axiom as "
\addvspace{\abovedisplayskip}
\noindent $\mathbf{Axiom\ }"[ x ]"
\colon "[ y ]"
\;\Box$

\addvspace{\belowdisplayskip}" end define ]]"

\item "[[ tex name define axiom x : y end axiom as "
\mathbf{Axiom\ }"[ x ]"
\colon "[ y ]"
\;\Box" end define ]]"

\item "[[ tex define rule x : y end rule as "
\addvspace{\abovedisplayskip}
\noindent $\mathbf{Rule\ }"[ x ]"
\colon "[ y ]"
\;\Box$

\addvspace{\belowdisplayskip}" end define ]]"

\item "[[ tex name define rule x : y end rule as "
\mathbf{Rule\ }"[ x ]"
\colon "[ y ]"
\;\Box" end define ]]"

\item "[[ tex define theory x : y end theory as "
\addvspace{\abovedisplayskip}
\noindent $\mathbf{Theory\ }"[ x ]"
\colon "[ y ]"
\;\Box$

\addvspace{\belowdisplayskip}" end define ]]"

\item "[[ tex name define theory x : y end theory as "
\mathbf{Theory\ }"[ x ]"
\colon "[ y ]"
\;\Box" end define ]]"

\item "[[ tex define lemma x : y end lemma as "
\addvspace{\abovedisplayskip}
\noindent $\mathbf{Lemma\ }"[ x ]"
\colon "[ y ]"
\;\Box$

\addvspace{\belowdisplayskip}" end define ]]"

\item "[[ tex name define lemma x : y end lemma as "
\mathbf{Lemma\ }"[ x ]"
\colon "[ y ]"
\;\Box" end define ]]"

\item "[[ tex define x lemma y : z end lemma as "
\addvspace{\abovedisplayskip}
\noindent $"[ x ]"
\mathbf{\ lemma\ }"[ y ]"
\colon "[ z ]"
\;\Box$

\addvspace{\belowdisplayskip}" end define ]]"

\item "[[ tex name define x lemma y : z end lemma as ""[ x ]"
\mathbf{\ lemma\ }"[ y ]"
\colon "[ z ]"
\;\Box" end define ]]"

\item "[[ tex define proof of x : y as "
\addvspace{\abovedisplayskip}
\noindent $\mathbf{Proof\ of\ }"[ x ]"
\colon "[ y ]"$

\addvspace{\belowdisplayskip}" end define ]]"

\item "[[ tex name define proof of x : y as "
\mathbf{Proof\ of\ }"[ x ]"
\colon "[ y ]"" end define ]]"

\item "[[ tex define x proof of y : z as "
\addvspace{\abovedisplayskip}
\noindent $"[ x ]"
\mathbf{\ proof\ of\ }"[ y ]"
\colon "[ z ]"$

\addvspace{\belowdisplayskip}" end define ]]"

\item "[[ tex name define x proof of y : z as ""[ x ]"
\mathbf{\ proof\ of\ }"[ y ]"
\colon "[ z ]"" end define ]]"



\item "[[ tex define glue ( x ) y as "
glue\linebreak [0]\ (\linebreak [0]\ "[ texname x end texname ]"
\linebreak [0]\ )\linebreak [0]\ "[ y ]"" end define ]]"

\item "[[ tex define diag ( x ) y as "
diag\linebreak [0]\ (\linebreak [0]\ "[ texname x end texname ]"
\linebreak [0]\ )\linebreak [0]\ "[ y ]"" end define ]]"

\item "[[ tex define glue' ( x ) y as ""[ x ]""[ y ]"" end define ]]"

\item "[[ tex name define glue' ( x ) y as "
glue' ( "[ x ]"
) "[ y ]"" end define ]]"

\item "[[ tex define diag' ( x ) y as "
"[ x ]" "[ y ]"" end define ]]"

\item "[[ tex name define diag' ( x ) y as "
diag' ( "[ x ]"
) "[ y ]"" end define ]]"

\item "[[ tex define disp' ( x ) y as "
\begin{quotation} \noindent $ "[ x ]"
$ \end{quotation} "[ y ]"" end define ]]"

\item "[[ tex name define disp' ( x ) y as "
disp' ( "[ x ]"
) "[ y ]"" end define ]]"

\item "[[ tex define form' ( x ) y as "
$ "[ x ]"
$"[ y ]"" end define ]]"

\item "[[ tex name define form' ( x ) y as "
form' ( "[ x ]"
) "[ y ]"" end define ]]"



\end{statements}



\section{Pyk definitions}

\begin{flushleft}
"[[ protect Define pyk of alpha as "alpha" end define linebreak Define pyk of beta as "beta" end define linebreak Define pyk of gamma as "gamma" end define linebreak Define pyk of delta as "delta" end define linebreak Define pyk of epsilon as "epsilon" end define linebreak Define pyk of varepsilon as "varepsilon" end define linebreak Define pyk of zeta as "zeta" end define linebreak Define pyk of eta as "eta" end define linebreak Define pyk of theta as "theta" end define linebreak Define pyk of vartheta as "vartheta" end define linebreak Define pyk of iota as "iota" end define linebreak Define pyk of kappa as "kappa" end define linebreak Define pyk of lambda as "lambda" end define linebreak Define pyk of mu as "mu" end define linebreak Define pyk of nu as "nu" end define linebreak Define pyk of xi as "xi" end define linebreak Define pyk of pi as "pi" end define linebreak Define pyk of varpi as "varpi" end define linebreak Define pyk of rho as "rho" end define linebreak Define pyk of varrho as "varrho" end define linebreak Define pyk of sigma as "sigma" end define linebreak Define pyk of varsigma as "varsigma" end define linebreak Define pyk of tau as "tau" end define linebreak Define pyk of upsilon as "upsilon" end define linebreak Define pyk of phi as "phi" end define linebreak Define pyk of chi as "chi" end define linebreak Define pyk of psi as "psi" end define linebreak Define pyk of omega as "omega" end define linebreak Define pyk of Gamma as "Gamma" end define linebreak Define pyk of Delta as "Delta" end define linebreak Define pyk of Theta as "Theta" end define linebreak Define pyk of Lambda as "Lambda" end define linebreak Define pyk of Xi as "Xi" end define linebreak Define pyk of Pi as "Pi" end define linebreak Define pyk of Sigma as "Sigma" end define linebreak Define pyk of Upsilon as "Upsilon" end define linebreak Define pyk of Phi as "Phi" end define linebreak Define pyk of Psi as "Psi" end define linebreak Define pyk of Omega as "Omega" end define linebreak Define pyk of cla as "cla" end define linebreak Define pyk of clb as "clb" end define linebreak Define pyk of clc as "clc" end define linebreak Define pyk of cld as "cld" end define linebreak Define pyk of cle as "cle" end define linebreak Define pyk of clf as "clf" end define linebreak Define pyk of clg as "clg" end define linebreak Define pyk of clh as "clh" end define linebreak Define pyk of cli as "cli" end define linebreak Define pyk of clj as "clj" end define linebreak Define pyk of clk as "clk" end define linebreak Define pyk of cll as "cll" end define linebreak Define pyk of clm as "clm" end define linebreak Define pyk of cln as "cln" end define linebreak Define pyk of clo as "clo" end define linebreak Define pyk of clp as "clp" end define linebreak Define pyk of clq as "clq" end define linebreak Define pyk of clr as "clr" end define linebreak Define pyk of cls as "cls" end define linebreak Define pyk of clt as "clt" end define linebreak Define pyk of clu as "clu" end define linebreak Define pyk of clv as "clv" end define linebreak Define pyk of clw as "clw" end define linebreak Define pyk of clx as "clx" end define linebreak Define pyk of cly as "cly" end define linebreak Define pyk of clz as "clz" end define linebreak Define pyk of statement as "statement" end define linebreak Define pyk of proof as "proof" end define linebreak Define pyk of meta as "meta" end define linebreak Define pyk of math as "math" end define linebreak Define pyk of tactic as "tactic" end define linebreak Define pyk of unitac as "unitac" end define linebreak Define pyk of locate as "locate" end define linebreak Define pyk of statement define asterisk as asterisk end define as "statement define "! as "! end define" end define linebreak Define pyk of proof define asterisk as asterisk end define as "proof define "! as "! end define" end define linebreak Define pyk of meta define asterisk as asterisk end define as "meta define "! as "! end define" end define linebreak Define pyk of math define asterisk as asterisk end define as "math define "! as "! end define" end define linebreak Define pyk of tactic define asterisk as asterisk end define as "tactic define "! as "! end define" end define linebreak Define pyk of unitac define asterisk as asterisk end define as "unitac define "! as "! end define" end define linebreak Define pyk of locate define asterisk as asterisk end define as "locate define "! as "! end define" end define linebreak Define pyk of ensure math asterisk end math as "ensure math "! end math" end define linebreak Define pyk of #a as "#a" end define linebreak Define pyk of #b as "#b" end define linebreak Define pyk of #c as "#c" end define linebreak Define pyk of #d as "#d" end define linebreak Define pyk of #e as "#e" end define linebreak Define pyk of #f as "#f" end define linebreak Define pyk of #g as "#g" end define linebreak Define pyk of #h as "#h" end define linebreak Define pyk of #i as "#i" end define linebreak Define pyk of #j as "#j" end define linebreak Define pyk of #k as "#k" end define linebreak Define pyk of #l as "#l" end define linebreak Define pyk of #m as "#m" end define linebreak Define pyk of #n as "#n" end define linebreak Define pyk of #o as "#o" end define linebreak Define pyk of #p as "#p" end define linebreak Define pyk of #q as "#q" end define linebreak Define pyk of #r as "#r" end define linebreak Define pyk of #s as "#s" end define linebreak Define pyk of #t as "#t" end define linebreak Define pyk of #u as "#u" end define linebreak Define pyk of #v as "#v" end define linebreak Define pyk of #w as "#w" end define linebreak Define pyk of #x as "#x" end define linebreak Define pyk of #y as "#y" end define linebreak Define pyk of #z as "#z" end define linebreak Define pyk of tacfresh ( asterisk ) as "tacfresh ( "! )" end define linebreak Define pyk of unifresh ( asterisk , asterisk ) as "unifresh ( "! , "! )" end define linebreak Define pyk of L00 as "L00" end define linebreak Define pyk of L01 as "L01" end define linebreak Define pyk of L02 as "L02" end define linebreak Define pyk of L03 as "L03" end define linebreak Define pyk of L04 as "L04" end define linebreak Define pyk of L05 as "L05" end define linebreak Define pyk of L06 as "L06" end define linebreak Define pyk of L07 as "L07" end define linebreak Define pyk of L08 as "L08" end define linebreak Define pyk of L09 as "L09" end define linebreak Define pyk of L10 as "L10" end define linebreak Define pyk of L11 as "L11" end define linebreak Define pyk of L12 as "L12" end define linebreak Define pyk of L13 as "L13" end define linebreak Define pyk of L14 as "L14" end define linebreak Define pyk of L15 as "L15" end define linebreak Define pyk of L16 as "L16" end define linebreak Define pyk of L17 as "L17" end define linebreak Define pyk of L18 as "L18" end define linebreak Define pyk of L19 as "L19" end define linebreak Define pyk of L20 as "L20" end define linebreak Define pyk of L21 as "L21" end define linebreak Define pyk of L22 as "L22" end define linebreak Define pyk of L23 as "L23" end define linebreak Define pyk of L24 as "L24" end define linebreak Define pyk of L25 as "L25" end define linebreak Define pyk of L26 as "L26" end define linebreak Define pyk of L27 as "L27" end define linebreak Define pyk of L28 as "L28" end define linebreak Define pyk of L29 as "L29" end define linebreak Define pyk of L30 as "L30" end define linebreak Define pyk of L31 as "L31" end define linebreak Define pyk of L32 as "L32" end define linebreak Define pyk of L33 as "L33" end define linebreak Define pyk of L34 as "L34" end define linebreak Define pyk of L35 as "L35" end define linebreak Define pyk of L36 as "L36" end define linebreak Define pyk of L37 as "L37" end define linebreak Define pyk of L38 as "L38" end define linebreak Define pyk of L39 as "L39" end define linebreak Define pyk of L40 as "L40" end define linebreak Define pyk of L41 as "L41" end define linebreak Define pyk of L42 as "L42" end define linebreak Define pyk of L43 as "L43" end define linebreak Define pyk of L44 as "L44" end define linebreak Define pyk of L45 as "L45" end define linebreak Define pyk of L46 as "L46" end define linebreak Define pyk of L47 as "L47" end define linebreak Define pyk of L48 as "L48" end define linebreak Define pyk of L49 as "L49" end define linebreak Define pyk of L50 as "L50" end define linebreak Define pyk of L51 as "L51" end define linebreak Define pyk of L52 as "L52" end define linebreak Define pyk of L53 as "L53" end define linebreak Define pyk of L54 as "L54" end define linebreak Define pyk of L55 as "L55" end define linebreak Define pyk of L56 as "L56" end define linebreak Define pyk of L57 as "L57" end define linebreak Define pyk of L58 as "L58" end define linebreak Define pyk of L59 as "L59" end define linebreak Define pyk of L60 as "L60" end define linebreak Define pyk of L61 as "L61" end define linebreak Define pyk of L62 as "L62" end define linebreak Define pyk of L63 as "L63" end define linebreak Define pyk of L64 as "L64" end define linebreak Define pyk of L65 as "L65" end define linebreak Define pyk of L66 as "L66" end define linebreak Define pyk of L67 as "L67" end define linebreak Define pyk of L68 as "L68" end define linebreak Define pyk of L69 as "L69" end define linebreak Define pyk of L70 as "L70" end define linebreak Define pyk of L71 as "L71" end define linebreak Define pyk of L72 as "L72" end define linebreak Define pyk of L73 as "L73" end define linebreak Define pyk of L74 as "L74" end define linebreak Define pyk of L75 as "L75" end define linebreak Define pyk of L76 as "L76" end define linebreak Define pyk of L77 as "L77" end define linebreak Define pyk of L78 as "L78" end define linebreak Define pyk of L79 as "L79" end define linebreak Define pyk of L80 as "L80" end define linebreak Define pyk of L81 as "L81" end define linebreak Define pyk of L82 as "L82" end define linebreak Define pyk of L83 as "L83" end define linebreak Define pyk of L84 as "L84" end define linebreak Define pyk of L85 as "L85" end define linebreak Define pyk of L86 as "L86" end define linebreak Define pyk of L87 as "L87" end define linebreak Define pyk of L88 as "L88" end define linebreak Define pyk of L89 as "L89" end define linebreak Define pyk of L90 as "L90" end define linebreak Define pyk of L91 as "L91" end define linebreak Define pyk of L92 as "L92" end define linebreak Define pyk of L93 as "L93" end define linebreak Define pyk of L94 as "L94" end define linebreak Define pyk of L95 as "L95" end define linebreak Define pyk of L96 as "L96" end define linebreak Define pyk of L97 as "L97" end define linebreak Define pyk of L98 as "L98" end define linebreak Define pyk of L99 as "L99" end define linebreak Define pyk of False as "False" end define linebreak Define pyk of p.A1 as "p.A1" end define linebreak Define pyk of p.A2 as "p.A2" end define linebreak Define pyk of p.A3 as "p.A3" end define linebreak Define pyk of p.MP as "p.MP" end define linebreak Define pyk of p.Prop as "p.Prop" end define linebreak Define pyk of p.IProp as "p.IProp" end define linebreak Define pyk of distinctvar ( asterisk , asterisk ) as "distinctvar ( "! , "! )" end define linebreak Define pyk of metaavoid1 ( asterisk , asterisk , asterisk ) as "metaavoid1 ( "! , "! , "! )" end define linebreak Define pyk of metaavoid1* ( asterisk , asterisk , asterisk ) as "metaavoid1* ( "! , "! , "! )" end define linebreak Define pyk of objectavoid1 ( asterisk , asterisk , asterisk , asterisk ) as "objectavoid1 ( "! , "! , "! , "! )" end define linebreak Define pyk of objectavoid1* ( asterisk , asterisk , asterisk , asterisk ) as "objectavoid1* ( "! , "! , "! , "! )" end define linebreak Define pyk of metafree ( asterisk , asterisk , asterisk , asterisk ) as "metafree ( "! , "! , "! , "! )" end define linebreak Define pyk of metafree* ( asterisk , asterisk , asterisk , asterisk ) as "metafree* ( "! , "! , "! , "! )" end define linebreak Define pyk of objectfree ( asterisk , asterisk , asterisk , asterisk ) as "objectfree ( "! , "! , "! , "! )" end define linebreak Define pyk of objectfree* ( asterisk , asterisk , asterisk , asterisk ) as "objectfree* ( "! , "! , "! , "! )" end define linebreak Define pyk of remove ( asterisk , asterisk ) as "remove ( "! , "! )" end define linebreak Define pyk of metaavoid2* ( asterisk , asterisk , asterisk ) as "metaavoid2* ( "! , "! , "! )" end define linebreak Define pyk of metasubst ( asterisk , asterisk , asterisk ) as "metasubst ( "! , "! , "! )" end define linebreak Define pyk of metasubst* ( asterisk , asterisk , asterisk ) as "metasubst* ( "! , "! , "! )" end define linebreak Define pyk of metasubstc ( asterisk , asterisk , asterisk ) as "metasubstc ( "! , "! , "! )" end define linebreak Define pyk of metasubstc1 ( asterisk , asterisk , asterisk , asterisk ) as "metasubstc1 ( "! , "! , "! , "! )" end define linebreak Define pyk of metasubstc1* ( asterisk , asterisk , asterisk , asterisk ) as "metasubstc1* ( "! , "! , "! , "! )" end define linebreak Define pyk of metasubstc2 ( asterisk , asterisk , asterisk , asterisk ) as "metasubstc2 ( "! , "! , "! , "! )" end define linebreak Define pyk of metasubstc2* ( asterisk , asterisk , asterisk , asterisk ) as "metasubstc2* ( "! , "! , "! , "! )" end define linebreak Define pyk of metasubstc3 ( asterisk , asterisk , asterisk , asterisk ) as "metasubstc3 ( "! , "! , "! , "! )" end define linebreak Define pyk of expand-All ( asterisk ) as "expand-All ( "! )" end define linebreak Define pyk of expand-All1 ( asterisk , asterisk , asterisk ) as "expand-All1 ( "! , "! , "! )" end define linebreak Define pyk of make-string ( asterisk , asterisk ) as "make-string ( "! , "! )" end define linebreak Define pyk of end diagnose as "end diagnose" end define linebreak Define pyk of Locate ( asterisk , asterisk , asterisk ) as "Locate ( "! , "! , "! )" end define linebreak Define pyk of Locate1 ( asterisk , asterisk , asterisk , asterisk , asterisk ) as "Locate1 ( "! , "! , "! , "! , "! )" end define linebreak Define pyk of error ( asterisk , asterisk ) as "error ( "! , "! )" end define linebreak Define pyk of mismatch ( asterisk , asterisk , asterisk ) as "mismatch ( "! , "! , "! )" end define linebreak Define pyk of mismatch* ( asterisk , asterisk , asterisk ) as "mismatch* ( "! , "! , "! )" end define linebreak Define pyk of eval-Init ( asterisk , asterisk ) as "eval-Init ( "! , "! )" end define linebreak Define pyk of eval-Ponens ( asterisk , asterisk , asterisk ) as "eval-Ponens ( "! , "! , "! )" end define linebreak Define pyk of eval-Probans ( asterisk , asterisk , asterisk ) as "eval-Probans ( "! , "! , "! )" end define linebreak Define pyk of eval-Verify ( asterisk , asterisk , asterisk ) as "eval-Verify ( "! , "! , "! )" end define linebreak Define pyk of eval-Curry ( asterisk , asterisk , asterisk ) as "eval-Curry ( "! , "! , "! )" end define linebreak Define pyk of eval-Uncurry ( asterisk , asterisk , asterisk ) as "eval-Uncurry ( "! , "! , "! )" end define linebreak Define pyk of eval-Deref ( asterisk , asterisk , asterisk ) as "eval-Deref ( "! , "! , "! )" end define linebreak Define pyk of eval-at ( asterisk , asterisk , asterisk ) as "eval-at ( "! , "! , "! )" end define linebreak Define pyk of eval-at1 ( asterisk , asterisk , asterisk , asterisk , asterisk ) as "eval-at1 ( "! , "! , "! , "! , "! )" end define linebreak Define pyk of eval-infer ( asterisk , asterisk , asterisk , asterisk ) as "eval-infer ( "! , "! , "! , "! )" end define linebreak Define pyk of eval-endorse ( asterisk , asterisk , asterisk , asterisk ) as "eval-endorse ( "! , "! , "! , "! )" end define linebreak Define pyk of eval-ie ( asterisk , asterisk , asterisk , asterisk ) as "eval-ie ( "! , "! , "! , "! )" end define linebreak Define pyk of eval-all ( asterisk , asterisk , asterisk , asterisk ) as "eval-all ( "! , "! , "! , "! )" end define linebreak Define pyk of eval-cut ( asterisk , asterisk , asterisk ) as "eval-cut ( "! , "! , "! )" end define linebreak Define pyk of seqeval ( asterisk , asterisk ) as "seqeval ( "! , "! )" end define linebreak Define pyk of Repeat as "Repeat" end define linebreak Define pyk of prepare proof indentation as "prepare proof indentation" end define linebreak Define pyk of claiming ( asterisk , asterisk ) as "claiming ( "! , "! )" end define linebreak Define pyk of proofcheck as "proofcheck" end define linebreak Define pyk of proofcheck1 ( asterisk ) as "proofcheck1 ( "! )" end define linebreak Define pyk of proofcheck2 ( asterisk ) as "proofcheck2 ( "! )" end define linebreak Define pyk of seqeval* ( asterisk , asterisk ) as "seqeval* ( "! , "! )" end define linebreak Define pyk of premisecheck* ( asterisk , asterisk ) as "premisecheck* ( "! , "! )" end define linebreak Define pyk of checked ( asterisk , asterisk ) as "checked ( "! , "! )" end define linebreak Define pyk of premisecheck ( asterisk , asterisk ) as "premisecheck ( "! , "! )" end define linebreak Define pyk of circularitycheck1 ( asterisk , asterisk , asterisk , asterisk ) as "circularitycheck1 ( "! , "! , "! , "! )" end define linebreak Define pyk of circularitycheck2 ( asterisk , asterisk , asterisk , asterisk ) as "circularitycheck2 ( "! , "! , "! , "! )" end define linebreak Define pyk of circularitycheck2* ( asterisk , asterisk , asterisk , asterisk ) as "circularitycheck2* ( "! , "! , "! , "! )" end define linebreak Define pyk of lemma1 as "lemma1" end define linebreak Define pyk of lemma2 as "lemma2" end define linebreak Define pyk of lemma2a as "lemma2a" end define linebreak Define pyk of lemma2b as "lemma2b" end define linebreak Define pyk of lemma2c as "lemma2c" end define linebreak Define pyk of lemma2d as "lemma2d" end define linebreak Define pyk of lemma2e as "lemma2e" end define linebreak Define pyk of lemma2f as "lemma2f" end define linebreak Define pyk of lemma3 as "lemma3" end define linebreak Define pyk of lemma4a as "lemma4a" end define linebreak Define pyk of lemma4b as "lemma4b" end define linebreak Define pyk of lemma4c as "lemma4c" end define linebreak Define pyk of lemma4d as "lemma4d" end define linebreak Define pyk of lemma4e as "lemma4e" end define linebreak Define pyk of lemma4f as "lemma4f" end define linebreak Define pyk of lemma4g as "lemma4g" end define linebreak Define pyk of int2string ( asterisk , asterisk ) as "int2string ( "! , "! )" end define linebreak Define pyk of int2string1 ( asterisk , asterisk ) as "int2string1 ( "! , "! )" end define linebreak Define pyk of val2term ( asterisk , asterisk ) as "val2term ( "! , "! )" end define linebreak Define pyk of card2term ( asterisk , asterisk ) as "card2term ( "! , "! )" end define linebreak Define pyk of univar ( asterisk , asterisk , asterisk ) as "univar ( "! , "! , "! )" end define linebreak Define pyk of pterm ( asterisk , asterisk ) as "pterm ( "! , "! )" end define linebreak Define pyk of pterm1 ( asterisk , asterisk , asterisk , asterisk ) as "pterm1 ( "! , "! , "! , "! )" end define linebreak Define pyk of pterm2 ( asterisk , asterisk , asterisk ) as "pterm2 ( "! , "! , "! )" end define linebreak Define pyk of pterm2* ( asterisk , asterisk , asterisk ) as "pterm2* ( "! , "! , "! )" end define linebreak Define pyk of inst ( asterisk , asterisk , asterisk ) as "inst ( "! , "! , "! )" end define linebreak Define pyk of inst* ( asterisk , asterisk , asterisk ) as "inst* ( "! , "! , "! )" end define linebreak Define pyk of occur ( asterisk , asterisk , asterisk ) as "occur ( "! , "! , "! )" end define linebreak Define pyk of occur* ( asterisk , asterisk , asterisk ) as "occur* ( "! , "! , "! )" end define linebreak Define pyk of unify ( asterisk , asterisk , asterisk ) as "unify ( "! , "! , "! )" end define linebreak Define pyk of unify* ( asterisk , asterisk , asterisk ) as "unify* ( "! , "! , "! )" end define linebreak Define pyk of unify2 ( asterisk , asterisk , asterisk ) as "unify2 ( "! , "! , "! )" end define linebreak Define pyk of taceval ( asterisk , asterisk , asterisk ) as "taceval ( "! , "! , "! )" end define linebreak Define pyk of taceval1 ( asterisk , asterisk , asterisk ) as "taceval1 ( "! , "! , "! )" end define linebreak Define pyk of tacstate0 as "tacstate0" end define linebreak Define pyk of unitac0 as "unitac0" end define linebreak Define pyk of tactic-push ( asterisk , asterisk , asterisk ) as "tactic-push ( "! , "! , "! )" end define linebreak Define pyk of tactic-pop ( asterisk , asterisk ) as "tactic-pop ( "! , "! )" end define linebreak Define pyk of tactic-Init ( asterisk ) as "tactic-Init ( "! )" end define linebreak Define pyk of tactic-Ponens ( asterisk ) as "tactic-Ponens ( "! )" end define linebreak Define pyk of tactic-Probans ( asterisk ) as "tactic-Probans ( "! )" end define linebreak Define pyk of tactic-Verify ( asterisk ) as "tactic-Verify ( "! )" end define linebreak Define pyk of tactic-Curry ( asterisk ) as "tactic-Curry ( "! )" end define linebreak Define pyk of tactic-Uncurry ( asterisk ) as "tactic-Uncurry ( "! )" end define linebreak Define pyk of tactic-Deref ( asterisk ) as "tactic-Deref ( "! )" end define linebreak Define pyk of tactic-at ( asterisk ) as "tactic-at ( "! )" end define linebreak Define pyk of tactic-at1 ( asterisk , asterisk , asterisk , asterisk ) as "tactic-at1 ( "! , "! , "! , "! )" end define linebreak Define pyk of tactic-at2 ( asterisk , asterisk , asterisk , asterisk , asterisk ) as "tactic-at2 ( "! , "! , "! , "! , "! )" end define linebreak Define pyk of tactic-infer ( asterisk ) as "tactic-infer ( "! )" end define linebreak Define pyk of tactic-endorse ( asterisk ) as "tactic-endorse ( "! )" end define linebreak Define pyk of tactic-ie ( asterisk ) as "tactic-ie ( "! )" end define linebreak Define pyk of tactic-all ( asterisk ) as "tactic-all ( "! )" end define linebreak Define pyk of tactic-cut ( asterisk ) as "tactic-cut ( "! )" end define linebreak Define pyk of tactic-cut1 ( asterisk , asterisk , asterisk ) as "tactic-cut1 ( "! , "! , "! )" end define linebreak Define pyk of hook-arg as "hook-arg" end define linebreak Define pyk of hook-res as "hook-res" end define linebreak Define pyk of hook-idx as "hook-idx" end define linebreak Define pyk of hook-uni as "hook-uni" end define linebreak Define pyk of hook-pre as "hook-pre" end define linebreak Define pyk of hook-cond as "hook-cond" end define linebreak Define pyk of hook-parm as "hook-parm" end define linebreak Define pyk of hook-unitac as "hook-unitac" end define linebreak Define pyk of hook-rule as "hook-rule" end define linebreak Define pyk of hook-lemma as "hook-lemma" end define linebreak Define pyk of hook-conclude as "hook-conclude" end define linebreak Define pyk of unitac ( asterisk ) as "unitac ( "! )" end define linebreak Define pyk of unitac1 ( asterisk , asterisk , asterisk ) as "unitac1 ( "! , "! , "! )" end define linebreak Define pyk of unieval ( asterisk , asterisk , asterisk ) as "unieval ( "! , "! , "! )" end define linebreak Define pyk of unitac-Init ( asterisk ) as "unitac-Init ( "! )" end define linebreak Define pyk of unitac-Conclude ( asterisk ) as "unitac-Conclude ( "! )" end define linebreak Define pyk of unitac-conclude ( asterisk ) as "unitac-conclude ( "! )" end define linebreak Define pyk of unitac-conclude-std ( asterisk ) as "unitac-conclude-std ( "! )" end define linebreak Define pyk of unitac-Ponens ( asterisk ) as "unitac-Ponens ( "! )" end define linebreak Define pyk of unitac-ponens ( asterisk ) as "unitac-ponens ( "! )" end define linebreak Define pyk of unitac-Probans ( asterisk ) as "unitac-Probans ( "! )" end define linebreak Define pyk of unitac-probans ( asterisk ) as "unitac-probans ( "! )" end define linebreak Define pyk of unitac-Verify ( asterisk ) as "unitac-Verify ( "! )" end define linebreak Define pyk of unitac-verify ( asterisk ) as "unitac-verify ( "! )" end define linebreak Define pyk of unitac-Curry ( asterisk ) as "unitac-Curry ( "! )" end define linebreak Define pyk of unitac-Uncurry ( asterisk ) as "unitac-Uncurry ( "! )" end define linebreak Define pyk of unitac-Deref ( asterisk ) as "unitac-Deref ( "! )" end define linebreak Define pyk of unitac-idest ( asterisk ) as "unitac-idest ( "! )" end define linebreak Define pyk of unitac-At ( asterisk ) as "unitac-At ( "! )" end define linebreak Define pyk of unitac-at ( asterisk ) as "unitac-at ( "! )" end define linebreak Define pyk of unitac-Infer ( asterisk ) as "unitac-Infer ( "! )" end define linebreak Define pyk of unitac-infer ( asterisk ) as "unitac-infer ( "! )" end define linebreak Define pyk of unitac-Endorse ( asterisk ) as "unitac-Endorse ( "! )" end define linebreak Define pyk of unitac-endorse ( asterisk ) as "unitac-endorse ( "! )" end define linebreak Define pyk of unitac-All ( asterisk ) as "unitac-All ( "! )" end define linebreak Define pyk of unitac-all ( asterisk ) as "unitac-all ( "! )" end define linebreak Define pyk of unitac-cut ( asterisk ) as "unitac-cut ( "! )" end define linebreak Define pyk of unitac-adapt ( asterisk , asterisk , asterisk ) as "unitac-adapt ( "! , "! , "! )" end define linebreak Define pyk of unitac-rule ( asterisk ) as "unitac-rule ( "! )" end define linebreak Define pyk of unitac-rule-std ( asterisk ) as "unitac-rule-std ( "! )" end define linebreak Define pyk of unitac-theo ( asterisk , asterisk , asterisk ) as "unitac-theo ( "! , "! , "! )" end define linebreak Define pyk of unitac-rule0 ( asterisk , asterisk , asterisk ) as "unitac-rule0 ( "! , "! , "! )" end define linebreak Define pyk of unitac-rule-plus ( asterisk , asterisk , asterisk ) as "unitac-rule-plus ( "! , "! , "! )" end define linebreak Define pyk of unitac-rule-stmt ( asterisk , asterisk , asterisk , asterisk ) as "unitac-rule-stmt ( "! , "! , "! , "! )" end define linebreak Define pyk of unitac-rule1 ( asterisk , asterisk , asterisk ) as "unitac-rule1 ( "! , "! , "! )" end define linebreak Define pyk of unitac-rule2 ( asterisk , asterisk , asterisk ) as "unitac-rule2 ( "! , "! , "! )" end define linebreak Define pyk of unitac-search ( asterisk , asterisk , asterisk ) as "unitac-search ( "! , "! , "! )" end define linebreak Define pyk of unitac-search1 ( asterisk , asterisk , asterisk , asterisk , asterisk ) as "unitac-search1 ( "! , "! , "! , "! , "! )" end define linebreak Define pyk of unitac-rule3 ( asterisk , asterisk ) as "unitac-rule3 ( "! , "! )" end define linebreak Define pyk of unitac-rule4 ( asterisk , asterisk ) as "unitac-rule4 ( "! , "! )" end define linebreak Define pyk of unitac-rule5 ( asterisk , asterisk , asterisk , asterisk ) as "unitac-rule5 ( "! , "! , "! , "! )" end define linebreak Define pyk of unitac-stack ( asterisk , asterisk , asterisk ) as "unitac-stack ( "! , "! , "! )" end define linebreak Define pyk of unitac-lemma ( asterisk ) as "unitac-lemma ( "! )" end define linebreak Define pyk of unitac-lemma-std ( asterisk ) as "unitac-lemma-std ( "! )" end define linebreak Define pyk of unitac-Rule ( asterisk ) as "unitac-Rule ( "! )" end define linebreak Define pyk of seqcnt ( asterisk , asterisk ) as "seqcnt ( "! , "! )" end define linebreak Define pyk of tactic-conclude-cut ( asterisk ) as "tactic-conclude-cut ( "! )" end define linebreak Define pyk of tactic-premise-line ( asterisk ) as "tactic-premise-line ( "! )" end define linebreak Define pyk of tactic-condition-line ( asterisk ) as "tactic-condition-line ( "! )" end define linebreak Define pyk of tactic-block ( asterisk ) as "tactic-block ( "! )" end define linebreak Define pyk of System S as "System S" end define linebreak Define pyk of S.S1 as "S.S1" end define linebreak Define pyk of S.S5 as "S.S5" end define linebreak Define pyk of S.reflexivity as "S.reflexivity" end define linebreak Define pyk of asterisk# as ""!#" end define linebreak Define pyk of asterisk plist ( asterisk ) as ""! plist ( "! )" end define linebreak Define pyk of asterisk def ( asterisk , asterisk ) as ""! def ( "! , "! )" end define linebreak Define pyk of asterisk lhs ( asterisk , asterisk ) as ""! lhs ( "! , "! )" end define linebreak Define pyk of asterisk rhs ( asterisk , asterisk ) as ""! rhs ( "! , "! )" end define linebreak Define pyk of asterisk metadef ( asterisk ) as ""! metadef ( "! )" end define linebreak Define pyk of asterisk metavar ( asterisk ) as ""! metavar ( "! )" end define linebreak Define pyk of asterisk stmt-rhs ( asterisk ) as ""! stmt-rhs ( "! )" end define linebreak Define pyk of asterisk proof-rhs ( asterisk ) as ""! proof-rhs ( "! )" end define linebreak Define pyk of asterisk tactic-rhs ( asterisk ) as ""! tactic-rhs ( "! )" end define linebreak Define pyk of asterisk unitac-rhs ( asterisk ) as ""! unitac-rhs ( "! )" end define linebreak Define pyk of asterisk locate-rhs ( asterisk ) as ""! locate-rhs ( "! )" end define linebreak Define pyk of asterisk mathdef ( asterisk ) as ""! mathdef ( "! )" end define linebreak Define pyk of asterisk valuedef ( asterisk ) as ""! valuedef ( "! )" end define linebreak Define pyk of asterisk objectvar ( asterisk ) as ""! objectvar ( "! )" end define linebreak Define pyk of asterisk objectlambda ( asterisk ) as ""! objectlambda ( "! )" end define linebreak Define pyk of asterisk objectquote ( asterisk ) as ""! objectquote ( "! )" end define linebreak Define pyk of asterisk objectterm ( asterisk ) as ""! objectterm ( "! )" end define linebreak Define pyk of asterisk objectterm* ( asterisk ) as ""! objectterm* ( "! )" end define linebreak Define pyk of asterisk metaterm ( asterisk ) as ""! metaterm ( "! )" end define linebreak Define pyk of asterisk metaterm* ( asterisk ) as ""! metaterm* ( "! )" end define linebreak Define pyk of asterisk metaavoid ( asterisk ) asterisk as ""! metaavoid ( "! ) "!" end define linebreak Define pyk of asterisk metaavoid* ( asterisk ) asterisk as ""! metaavoid* ( "! ) "!" end define linebreak Define pyk of asterisk objectavoid ( asterisk ) asterisk as ""! objectavoid ( "! ) "!" end define linebreak Define pyk of asterisk objectavoid* ( asterisk ) asterisk as ""! objectavoid* ( "! ) "!" end define linebreak Define pyk of asterisk set+ asterisk as ""! set+ "!" end define linebreak Define pyk of asterisk set- asterisk as ""! set- "!" end define linebreak Define pyk of asterisk set-- asterisk as ""! set-- "!" end define linebreak Define pyk of asterisk union asterisk as ""! union "!" end define linebreak Define pyk of asterisk member asterisk as ""! member "!" end define linebreak Define pyk of asterisk subset asterisk as ""! subset "!" end define linebreak Define pyk of asterisk set= asterisk as ""! set= "!" end define linebreak Define pyk of asterisk sequent= asterisk as ""! sequent= "!" end define linebreak Define pyk of p.not asterisk as "p.not "!" end define linebreak Define pyk of asterisk p.imply asterisk as ""! p.imply "!" end define linebreak Define pyk of metadeclare asterisk as "metadeclare "!" end define linebreak Define pyk of asterisk Init as ""! Init" end define linebreak Define pyk of asterisk Ponens as ""! Ponens" end define linebreak Define pyk of asterisk Probans as ""! Probans" end define linebreak Define pyk of asterisk Verify as ""! Verify" end define linebreak Define pyk of asterisk Curry as ""! Curry" end define linebreak Define pyk of asterisk Uncurry as ""! Uncurry" end define linebreak Define pyk of asterisk Deref as ""! Deref" end define linebreak Define pyk of asterisk At as ""! At" end define linebreak Define pyk of asterisk Infer as ""! Infer" end define linebreak Define pyk of asterisk Endorse as ""! Endorse" end define linebreak Define pyk of asterisk All as ""! All" end define linebreak Define pyk of asterisk Conclude as ""! Conclude" end define linebreak Define pyk of asterisk Rule as ""! Rule" end define linebreak Define pyk of asterisk at asterisk as ""! at "!" end define linebreak Define pyk of asterisk ponens asterisk as ""! ponens "!" end define linebreak Define pyk of asterisk probans asterisk as ""! probans "!" end define linebreak Define pyk of asterisk verify asterisk as ""! verify "!" end define linebreak Define pyk of asterisk p.mp asterisk as ""! p.mp "!" end define linebreak Define pyk of asterisk infer asterisk as ""! infer "!" end define linebreak Define pyk of asterisk endorse asterisk as ""! endorse "!" end define linebreak Define pyk of asterisk id est asterisk as ""! id est "!" end define linebreak Define pyk of All asterisk : asterisk as "All "! : "!" end define linebreak Define pyk of asterisk oplus asterisk as ""! oplus "!" end define linebreak Define pyk of asterisk conclude asterisk as ""! conclude "!" end define linebreak Define pyk of line asterisk : asterisk >> asterisk ; asterisk as "line "! : "! >> "! ; "!" end define linebreak Define pyk of Line asterisk : asterisk >> asterisk ; asterisk as "Line "! : "! >> "! ; "!" end define linebreak Define pyk of line asterisk : asterisk >> asterisk ; as "line "! : "! >> "! ;" end define linebreak Define pyk of line asterisk : asterisk >> asterisk qed as "line "! : "! >> "! qed" end define linebreak Define pyk of line asterisk : Premise >> asterisk ; asterisk as "line "! : Premise >> "! ; "!" end define linebreak Define pyk of Line asterisk : Premise >> asterisk ; asterisk as "Line "! : Premise >> "! ; "!" end define linebreak Define pyk of line asterisk : Condition >> asterisk ; asterisk as "line "! : Condition >> "! ; "!" end define linebreak Define pyk of Line asterisk : Condition >> asterisk ; asterisk as "Line "! : Condition >> "! ; "!" end define linebreak Define pyk of line asterisk : Arbitrary >> asterisk ; asterisk as "line "! : Arbitrary >> "! ; "!" end define linebreak Define pyk of line asterisk : Local >> asterisk = asterisk ; asterisk as "line "! : Local >> "! = "! ; "!" end define linebreak Define pyk of line asterisk : Block >> Begin ; asterisk line asterisk : Block >> End ; asterisk as "line "! : Block >> Begin ; "! line "! : Block >> End ; "!" end define linebreak Define pyk of Line asterisk : Block >> Begin ; asterisk line asterisk : Block >> End ; asterisk as "Line "! : Block >> Begin ; "! line "! : Block >> End ; "!" end define linebreak Define pyk of asterisk ;; asterisk as ""! ;; "!" end define linebreak Define pyk of asterisk proves asterisk as ""! proves "!" end define linebreak Define pyk of axiom asterisk : asterisk end axiom as "axiom "! : "! end axiom" end define linebreak Define pyk of rule asterisk : asterisk end rule as "rule "! : "! end rule" end define linebreak Define pyk of theory asterisk : asterisk end theory as "theory "! : "! end theory" end define linebreak Define pyk of lemma asterisk : asterisk end lemma as "lemma "! : "! end lemma" end define linebreak Define pyk of asterisk lemma asterisk : asterisk end lemma as ""! lemma "! : "! end lemma" end define linebreak Define pyk of proof of asterisk : asterisk as "proof of "! : "!" end define linebreak Define pyk of asterisk proof of asterisk : asterisk as ""! proof of "! : "!" end define linebreak Define pyk of dbug ( asterisk ) asterisk as "dbug ( "! ) "!" end define linebreak Define pyk of dbug* ( asterisk ) asterisk as "dbug* ( "! ) "!" end define linebreak Define pyk of glue ( asterisk ) asterisk as "glue ( "! ) "!" end define linebreak Define pyk of diag ( asterisk ) asterisk as "diag ( "! ) "!" end define linebreak Define pyk of disp ( asterisk ) asterisk as "disp ( "! ) "!" end define linebreak Define pyk of form ( asterisk ) asterisk as "form ( "! ) "!" end define linebreak Define pyk of glue' ( asterisk ) asterisk as "glue' ( "! ) "!" end define linebreak Define pyk of dbug' ( asterisk ) asterisk as "dbug' ( "! ) "!" end define linebreak Define pyk of diag' ( asterisk ) asterisk as "diag' ( "! ) "!" end define linebreak Define pyk of disp' ( asterisk ) asterisk as "disp' ( "! ) "!" end define linebreak Define pyk of form' ( asterisk ) asterisk as "form' ( "! ) "!" end define linebreak Define pyk of LocateProofLine ( asterisk , asterisk ) asterisk as "LocateProofLine ( "! , "! ) "!" end define linebreak Define pyk of check as "check" end define linebreak empty end protect ]]"
\end{flushleft}



\section{Priority table}

\begin {flushleft}
"[[ priority table preassociative priority check equal priority base equal priority proclaim asterisk as asterisk end proclaim equal priority empty equal priority preassociative asterisk greater than asterisk equal priority postassociative asterisk greater than asterisk equal priority priority asterisk equal asterisk equal priority priority asterisk end priority equal priority asterisk equal priority pyk equal priority Define asterisk of asterisk as asterisk end define equal priority math asterisk end math equal priority display math asterisk end math equal priority make math asterisk end math equal priority a equal priority b equal priority c equal priority d equal priority e equal priority f equal priority g equal priority h equal priority i equal priority j equal priority k equal priority l equal priority m equal priority n equal priority o equal priority p equal priority q equal priority r equal priority s equal priority t equal priority u equal priority x equal priority y equal priority z equal priority v equal priority w equal priority A equal priority B equal priority C equal priority D equal priority E equal priority F equal priority G equal priority H equal priority I equal priority J equal priority K equal priority L equal priority M equal priority N equal priority O equal priority P equal priority Q equal priority R equal priority S equal priority T equal priority U equal priority V equal priority W equal priority X equal priority Y equal priority Z equal priority true equal priority quote asterisk end quote equal priority optimized define asterisk of asterisk as asterisk end define equal priority tex equal priority tex name equal priority priority equal priority value equal priority macro equal priority render equal priority claim equal priority message equal priority unpack equal priority execute equal priority executables equal priority exampleaspect0 equal priority exampleaspect1 equal priority exampleaspect2 equal priority name asterisk end name equal priority macro name asterisk end name equal priority hiding name asterisk end name equal priority hide asterisk end hide equal priority array ( asterisk ) asterisk end array equal priority left equal priority center equal priority right equal priority %% equal priority ( asterisk ) equal priority < asterisk | asterisk := asterisk > equal priority bottom equal priority false equal priority define asterisk of asterisk as asterisk end define equal priority ... equal priority --- 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 Ten equal priority Base equal priority Xor ( asterisk , asterisk , asterisk ) equal priority Carry ( asterisk , asterisk , asterisk ) equal priority Plus ( asterisk , asterisk , asterisk ) equal priority Borrow ( asterisk , asterisk , asterisk ) equal priority Compare ( asterisk , asterisk , asterisk ) equal priority Minus ( asterisk , asterisk , asterisk ) equal priority BoolTag equal priority IntTag equal priority PairTag equal priority ExTag equal priority MapTag equal priority equal1 ( asterisk , asterisk ) equal priority TheInt ( asterisk , asterisk ) equal priority int ( asterisk ) equal priority plus1 ( asterisk , asterisk ) equal priority plus2 ( asterisk , asterisk , asterisk , asterisk ) equal priority minus1 ( asterisk ) equal priority minus2 ( asterisk , asterisk ) equal priority times1 ( asterisk , asterisk ) equal priority times2 ( asterisk , asterisk , asterisk , asterisk ) equal priority lt1 ( asterisk , asterisk ) equal priority lt2 ( asterisk , asterisk , asterisk , asterisk ) equal priority reverse ( asterisk ) equal priority revappend ( asterisk , asterisk ) equal priority nth ( asterisk , asterisk ) equal priority exception equal priority map ( asterisk ) equal priority Catch ( asterisk ) equal priority catch ( asterisk ) equal priority object ( asterisk ) equal priority Object ( asterisk , asterisk , asterisk ) equal priority destruct ( asterisk ) equal priority 0 equal priority 1 equal priority 2 equal priority 3 equal priority 4 equal priority 5 equal priority 6 equal priority 7 equal priority 8 equal priority 9 equal priority numeral ( asterisk ) equal priority num1 ( asterisk , asterisk , asterisk ) equal priority num2 ( asterisk , asterisk , asterisk ) equal priority evenp ( asterisk ) equal priority oddp ( asterisk ) equal priority half ( asterisk ) equal priority small ( asterisk ) equal priority double ( asterisk , asterisk ) equal priority lognot ( asterisk ) equal priority logior ( asterisk , asterisk ) equal priority logxor ( asterisk , asterisk ) equal priority logand ( asterisk , asterisk ) equal priority logeqv ( asterisk , asterisk ) equal priority lognand ( asterisk , asterisk ) equal priority lognor ( asterisk , asterisk ) equal priority logandc1 ( asterisk , asterisk ) equal priority logandc2 ( asterisk , asterisk ) equal priority logorc1 ( asterisk , asterisk ) equal priority logorc2 ( asterisk , asterisk ) equal priority logtest ( asterisk , asterisk ) equal priority ash ( asterisk , asterisk ) equal priority ash+ ( asterisk , asterisk ) equal priority ash- ( asterisk , asterisk ) equal priority logbitp ( asterisk , asterisk ) equal priority logcount ( asterisk ) equal priority logcount1 ( asterisk ) equal priority integer-length ( asterisk ) equal priority vector-mask equal priority vector-empty ( asterisk ) equal priority vector-head1 ( asterisk ) equal priority vector-tail1 ( asterisk ) equal priority vector-cons ( asterisk , asterisk ) equal priority vector ( asterisk ) equal priority vector-suffix ( asterisk , asterisk ) equal priority vector-prefix ( asterisk , asterisk ) equal priority vector-subseq ( asterisk , asterisk , asterisk ) equal priority vector-length ( asterisk ) equal priority vector-index ( asterisk , asterisk ) equal priority vector-head ( asterisk ) equal priority vector-tail ( asterisk ) equal priority vector2byte* ( asterisk ) equal priority vector2byte*1 ( asterisk , asterisk ) equal priority bt2byte* ( asterisk ) equal priority bt2byte*1 ( asterisk , asterisk ) equal priority bt2vector ( asterisk ) equal priority revbyte*2vector ( asterisk , asterisk ) equal priority vector-revappend ( asterisk , asterisk ) equal priority vt2byte* ( asterisk ) equal priority vt2byte*1 ( asterisk , asterisk ) equal priority vt2vector ( asterisk ) equal priority floor1 ( asterisk , asterisk ) equal priority ceiling1 ( asterisk , asterisk ) equal priority round1 ( asterisk , asterisk ) equal priority floor ( asterisk , asterisk ) equal priority ceiling ( asterisk , asterisk ) equal priority truncate ( asterisk , asterisk ) equal priority round ( asterisk , asterisk ) equal priority reverse quotient ( asterisk ) equal priority length ( asterisk ) equal priority length1 ( asterisk , asterisk ) equal priority list-prefix ( asterisk , asterisk ) equal priority list-suffix ( asterisk , asterisk ) equal priority lookup ( asterisk , asterisk , asterisk ) equal priority zip ( asterisk , asterisk ) equal priority array1 ( asterisk , asterisk , asterisk ) equal priority array2 ( asterisk , asterisk , asterisk , asterisk ) equal priority array3 ( asterisk , asterisk ) equal priority array4 ( asterisk , asterisk ) equal priority array5 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority eval ( asterisk , asterisk , asterisk ) equal priority eval1 ( asterisk , asterisk , asterisk , asterisk ) equal priority spy ( asterisk ) equal priority trace ( asterisk ) equal priority print ( asterisk ) equal priority timer ( asterisk ) equal priority test1 equal priority test2 ( asterisk ) equal priority test3 ( asterisk , asterisk ) equal priority test3* ( asterisk , asterisk ) equal priority ttst1 ( asterisk ) equal priority ftst1 ( asterisk ) equal priority etst1 ( asterisk ) equal priority ttst asterisk end test equal priority ftst asterisk end test equal priority etst asterisk ; asterisk end test equal priority texname asterisk end texname equal priority testfunc1 ( asterisk ) equal priority testfunc2 ( asterisk , asterisk ) equal priority testfunc3 equal priority testfunc4 equal priority testfunc5 ( asterisk ) equal priority testfunc6 ( asterisk ) equal priority testfunc7 ( asterisk ) equal priority testfunc8 ( asterisk , asterisk ) equal priority macro1 equal priority macro2 ( asterisk ) equal priority macro3 ( asterisk , asterisk , asterisk ) equal priority macro3* ( asterisk , asterisk , asterisk ) equal priority macro4 ( asterisk ) equal priority macrostate0 equal priority stateexpand ( asterisk , asterisk , asterisk ) equal priority stateexpand* ( asterisk , asterisk , asterisk ) equal priority substitute ( asterisk , asterisk , asterisk ) equal priority substitute* ( asterisk , asterisk , asterisk ) equal priority expand ( asterisk , asterisk ) equal priority protect asterisk end protect equal priority Macro define asterisk as asterisk end define equal priority Macrodefine ( asterisk ) equal priority macro define asterisk as asterisk end define equal priority macrodefine ( asterisk ) equal priority self equal priority makeself ( asterisk ) equal priority root protect asterisk end protect equal priority rootprotect ( asterisk ) equal priority render define asterisk as asterisk end define equal priority tex define asterisk as asterisk end define equal priority tex name define asterisk as asterisk end define equal priority value define asterisk as asterisk end define equal priority message define asterisk as asterisk end define equal priority priority table asterisk equal priority verifier asterisk end verifier equal priority unpacker asterisk end unpacker equal priority renderer asterisk end renderer equal priority expander asterisk end expander equal priority executer asterisk end executer equal priority executables asterisk end executables equal priority ragged right equal priority make macro expanded version ragged right equal priority <<>> equal priority << asterisk >> equal priority tuple1 ( asterisk ) equal priority tuple2 ( asterisk , asterisk ) equal priority eager define asterisk as asterisk end define equal priority eager1 ( asterisk ) equal priority eager2 ( asterisk , asterisk , asterisk ) equal priority eager message define asterisk as asterisk end define equal priority macrolet1 ( asterisk ) equal priority destructure equal priority destructure define asterisk as asterisk end define equal priority let1 ( asterisk ) equal priority let2 ( asterisk , asterisk , asterisk , asterisk ) equal priority let3 ( asterisk , asterisk , asterisk , asterisk ) equal priority make-var ( asterisk ) equal priority make-let ( asterisk , asterisk , asterisk ) equal priority make-prime ( asterisk ) equal priority make-head ( asterisk ) equal priority make-tail ( asterisk ) equal priority back asterisk quote asterisk end quote equal priority make-root ( asterisk , asterisk ) equal priority make-pair ( asterisk , asterisk , asterisk ) equal priority make-true ( asterisk ) equal priority make-quote ( asterisk , asterisk ) equal priority make-make-root ( asterisk , asterisk , asterisk ) equal priority backquote0 ( asterisk ) equal priority backquote1 ( asterisk , asterisk , asterisk ) equal priority backquote2 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority backquote2* ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority text asterisk : asterisk end text equal priority tex ( asterisk ) equal priority latex ( asterisk ) equal priority bibtex ( asterisk ) equal priority makeindex ( asterisk ) equal priority dvipdfm ( asterisk ) equal priority page ( asterisk , asterisk ) title asterisk bib asterisk main text asterisk appendix asterisk end page equal priority page1 ( asterisk ) equal priority tex-file ( asterisk , asterisk , asterisk ) equal priority tex-command ( asterisk , asterisk ) equal priority quit ( asterisk ) equal priority boot ( asterisk , asterisk , asterisk ) equal priority write ( asterisk ) equal priority read ( asterisk ) equal priority exec ( asterisk , asterisk ) equal priority int ( asterisk , asterisk ) equal priority extend ( asterisk ) equal priority extended ( asterisk ) equal priority Hello World equal priority Echo equal priority Echo1 ( asterisk ) equal priority Eecho equal priority Eecho1 ( asterisk ) equal priority alpha equal priority beta equal priority gamma equal priority delta equal priority epsilon equal priority varepsilon equal priority zeta equal priority eta equal priority theta equal priority vartheta equal priority iota equal priority kappa equal priority lambda equal priority mu equal priority nu equal priority xi equal priority pi equal priority varpi equal priority rho equal priority varrho equal priority sigma equal priority varsigma equal priority tau equal priority upsilon equal priority phi equal priority chi equal priority psi equal priority omega equal priority Gamma equal priority Delta equal priority Theta equal priority Lambda equal priority Xi equal priority Pi equal priority Sigma equal priority Upsilon equal priority Phi equal priority Psi equal priority Omega equal priority cla equal priority clb equal priority clc equal priority cld equal priority cle equal priority clf equal priority clg equal priority clh equal priority cli equal priority clj equal priority clk equal priority cll equal priority clm equal priority cln equal priority clo equal priority clp equal priority clq equal priority clr equal priority cls equal priority clt equal priority clu equal priority clv equal priority clw equal priority clx equal priority cly equal priority clz equal priority statement equal priority proof equal priority meta equal priority math equal priority tactic equal priority unitac equal priority locate equal priority statement define asterisk as asterisk end define equal priority proof define asterisk as asterisk end define equal priority meta define asterisk as asterisk end define equal priority math define asterisk as asterisk end define equal priority tactic define asterisk as asterisk end define equal priority unitac define asterisk as asterisk end define equal priority locate define asterisk as asterisk end define equal priority ensure math asterisk end math equal priority #a equal priority #b equal priority #c equal priority #d equal priority #e equal priority #f equal priority #g equal priority #h equal priority #i equal priority #j equal priority #k equal priority #l equal priority #m equal priority #n equal priority #o equal priority #p equal priority #q equal priority #r equal priority #s equal priority #t equal priority #u equal priority #v equal priority #w equal priority #x equal priority #y equal priority #z equal priority tacfresh ( asterisk ) equal priority unifresh ( asterisk , asterisk ) equal priority L00 equal priority L01 equal priority L02 equal priority L03 equal priority L04 equal priority L05 equal priority L06 equal priority L07 equal priority L08 equal priority L09 equal priority L10 equal priority L11 equal priority L12 equal priority L13 equal priority L14 equal priority L15 equal priority L16 equal priority L17 equal priority L18 equal priority L19 equal priority L20 equal priority L21 equal priority L22 equal priority L23 equal priority L24 equal priority L25 equal priority L26 equal priority L27 equal priority L28 equal priority L29 equal priority L30 equal priority L31 equal priority L32 equal priority L33 equal priority L34 equal priority L35 equal priority L36 equal priority L37 equal priority L38 equal priority L39 equal priority L40 equal priority L41 equal priority L42 equal priority L43 equal priority L44 equal priority L45 equal priority L46 equal priority L47 equal priority L48 equal priority L49 equal priority L50 equal priority L51 equal priority L52 equal priority L53 equal priority L54 equal priority L55 equal priority L56 equal priority L57 equal priority L58 equal priority L59 equal priority L60 equal priority L61 equal priority L62 equal priority L63 equal priority L64 equal priority L65 equal priority L66 equal priority L67 equal priority L68 equal priority L69 equal priority L70 equal priority L71 equal priority L72 equal priority L73 equal priority L74 equal priority L75 equal priority L76 equal priority L77 equal priority L78 equal priority L79 equal priority L80 equal priority L81 equal priority L82 equal priority L83 equal priority L84 equal priority L85 equal priority L86 equal priority L87 equal priority L88 equal priority L89 equal priority L90 equal priority L91 equal priority L92 equal priority L93 equal priority L94 equal priority L95 equal priority L96 equal priority L97 equal priority L98 equal priority L99 equal priority False equal priority p.A1 equal priority p.A2 equal priority p.A3 equal priority p.MP equal priority p.Prop equal priority p.IProp equal priority distinctvar ( asterisk , asterisk ) equal priority metaavoid1 ( asterisk , asterisk , asterisk ) equal priority metaavoid1* ( asterisk , asterisk , asterisk ) equal priority objectavoid1 ( asterisk , asterisk , asterisk , asterisk ) equal priority objectavoid1* ( asterisk , asterisk , asterisk , asterisk ) equal priority metafree ( asterisk , asterisk , asterisk , asterisk ) equal priority metafree* ( asterisk , asterisk , asterisk , asterisk ) equal priority objectfree ( asterisk , asterisk , asterisk , asterisk ) equal priority objectfree* ( asterisk , asterisk , asterisk , asterisk ) equal priority remove ( asterisk , asterisk ) equal priority metaavoid2* ( asterisk , asterisk , asterisk ) equal priority metasubst ( asterisk , asterisk , asterisk ) equal priority metasubst* ( asterisk , asterisk , asterisk ) equal priority metasubstc ( asterisk , asterisk , asterisk ) equal priority metasubstc1 ( asterisk , asterisk , asterisk , asterisk ) equal priority metasubstc1* ( asterisk , asterisk , asterisk , asterisk ) equal priority metasubstc2 ( asterisk , asterisk , asterisk , asterisk ) equal priority metasubstc2* ( asterisk , asterisk , asterisk , asterisk ) equal priority metasubstc3 ( asterisk , asterisk , asterisk , asterisk ) equal priority expand-All ( asterisk ) equal priority expand-All1 ( asterisk , asterisk , asterisk ) equal priority make-string ( asterisk , asterisk ) equal priority end diagnose equal priority Locate ( asterisk , asterisk , asterisk ) equal priority Locate1 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority error ( asterisk , asterisk ) equal priority mismatch ( asterisk , asterisk , asterisk ) equal priority mismatch* ( asterisk , asterisk , asterisk ) equal priority eval-Init ( asterisk , asterisk ) equal priority eval-Ponens ( asterisk , asterisk , asterisk ) equal priority eval-Probans ( asterisk , asterisk , asterisk ) equal priority eval-Verify ( asterisk , asterisk , asterisk ) equal priority eval-Curry ( asterisk , asterisk , asterisk ) equal priority eval-Uncurry ( asterisk , asterisk , asterisk ) equal priority eval-Deref ( asterisk , asterisk , asterisk ) equal priority eval-at ( asterisk , asterisk , asterisk ) equal priority eval-at1 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority eval-infer ( asterisk , asterisk , asterisk , asterisk ) equal priority eval-endorse ( asterisk , asterisk , asterisk , asterisk ) equal priority eval-ie ( asterisk , asterisk , asterisk , asterisk ) equal priority eval-all ( asterisk , asterisk , asterisk , asterisk ) equal priority eval-cut ( asterisk , asterisk , asterisk ) equal priority seqeval ( asterisk , asterisk ) equal priority Repeat equal priority prepare proof indentation equal priority claiming ( asterisk , asterisk ) equal priority proofcheck equal priority proofcheck1 ( asterisk ) equal priority proofcheck2 ( asterisk ) equal priority seqeval* ( asterisk , asterisk ) equal priority premisecheck* ( asterisk , asterisk ) equal priority checked ( asterisk , asterisk ) equal priority premisecheck ( asterisk , asterisk ) equal priority circularitycheck1 ( asterisk , asterisk , asterisk , asterisk ) equal priority circularitycheck2 ( asterisk , asterisk , asterisk , asterisk ) equal priority circularitycheck2* ( asterisk , asterisk , asterisk , asterisk ) equal priority lemma1 equal priority lemma2 equal priority lemma2a equal priority lemma2b equal priority lemma2c equal priority lemma2d equal priority lemma2e equal priority lemma2f equal priority lemma3 equal priority lemma4a equal priority lemma4b equal priority lemma4c equal priority lemma4d equal priority lemma4e equal priority lemma4f equal priority lemma4g equal priority int2string ( asterisk , asterisk ) equal priority int2string1 ( asterisk , asterisk ) equal priority val2term ( asterisk , asterisk ) equal priority card2term ( asterisk , asterisk ) equal priority univar ( asterisk , asterisk , asterisk ) equal priority pterm ( asterisk , asterisk ) equal priority pterm1 ( asterisk , asterisk , asterisk , asterisk ) equal priority pterm2 ( asterisk , asterisk , asterisk ) equal priority pterm2* ( asterisk , asterisk , asterisk ) equal priority inst ( asterisk , asterisk , asterisk ) equal priority inst* ( asterisk , asterisk , asterisk ) equal priority occur ( asterisk , asterisk , asterisk ) equal priority occur* ( asterisk , asterisk , asterisk ) equal priority unify ( asterisk , asterisk , asterisk ) equal priority unify* ( asterisk , asterisk , asterisk ) equal priority unify2 ( asterisk , asterisk , asterisk ) equal priority taceval ( asterisk , asterisk , asterisk ) equal priority taceval1 ( asterisk , asterisk , asterisk ) equal priority tacstate0 equal priority unitac0 equal priority tactic-push ( asterisk , asterisk , asterisk ) equal priority tactic-pop ( asterisk , asterisk ) equal priority tactic-Init ( asterisk ) equal priority tactic-Ponens ( asterisk ) equal priority tactic-Probans ( asterisk ) equal priority tactic-Verify ( asterisk ) equal priority tactic-Curry ( asterisk ) equal priority tactic-Uncurry ( asterisk ) equal priority tactic-Deref ( asterisk ) equal priority tactic-at ( asterisk ) equal priority tactic-at1 ( asterisk , asterisk , asterisk , asterisk ) equal priority tactic-at2 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority tactic-infer ( asterisk ) equal priority tactic-endorse ( asterisk ) equal priority tactic-ie ( asterisk ) equal priority tactic-all ( asterisk ) equal priority tactic-cut ( asterisk ) equal priority tactic-cut1 ( asterisk , asterisk , asterisk ) equal priority hook-arg equal priority hook-res equal priority hook-idx equal priority hook-uni equal priority hook-pre equal priority hook-cond equal priority hook-parm equal priority hook-unitac equal priority hook-rule equal priority hook-lemma equal priority hook-conclude equal priority unitac ( asterisk ) equal priority unitac1 ( asterisk , asterisk , asterisk ) equal priority unieval ( asterisk , asterisk , asterisk ) equal priority unitac-Init ( asterisk ) equal priority unitac-Conclude ( asterisk ) equal priority unitac-conclude ( asterisk ) equal priority unitac-conclude-std ( asterisk ) equal priority unitac-Ponens ( asterisk ) equal priority unitac-ponens ( asterisk ) equal priority unitac-Probans ( asterisk ) equal priority unitac-probans ( asterisk ) equal priority unitac-Verify ( asterisk ) equal priority unitac-verify ( asterisk ) equal priority unitac-Curry ( asterisk ) equal priority unitac-Uncurry ( asterisk ) equal priority unitac-Deref ( asterisk ) equal priority unitac-idest ( asterisk ) equal priority unitac-At ( asterisk ) equal priority unitac-at ( asterisk ) equal priority unitac-Infer ( asterisk ) equal priority unitac-infer ( asterisk ) equal priority unitac-Endorse ( asterisk ) equal priority unitac-endorse ( asterisk ) equal priority unitac-All ( asterisk ) equal priority unitac-all ( asterisk ) equal priority unitac-cut ( asterisk ) equal priority unitac-adapt ( asterisk , asterisk , asterisk ) equal priority unitac-rule ( asterisk ) equal priority unitac-rule-std ( asterisk ) equal priority unitac-theo ( asterisk , asterisk , asterisk ) equal priority unitac-rule0 ( asterisk , asterisk , asterisk ) equal priority unitac-rule-plus ( asterisk , asterisk , asterisk ) equal priority unitac-rule-stmt ( asterisk , asterisk , asterisk , asterisk ) equal priority unitac-rule1 ( asterisk , asterisk , asterisk ) equal priority unitac-rule2 ( asterisk , asterisk , asterisk ) equal priority unitac-search ( asterisk , asterisk , asterisk ) equal priority unitac-search1 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority unitac-rule3 ( asterisk , asterisk ) equal priority unitac-rule4 ( asterisk , asterisk ) equal priority unitac-rule5 ( asterisk , asterisk , asterisk , asterisk ) equal priority unitac-stack ( asterisk , asterisk , asterisk ) equal priority unitac-lemma ( asterisk ) equal priority unitac-lemma-std ( asterisk ) equal priority unitac-Rule ( asterisk ) equal priority seqcnt ( asterisk , asterisk ) equal priority tactic-conclude-cut ( asterisk ) equal priority tactic-premise-line ( asterisk ) equal priority tactic-condition-line ( asterisk ) equal priority tactic-block ( asterisk ) equal priority System S equal priority S.S1 equal priority S.S5 equal priority S.reflexivity end priority greater than preassociative priority +asterisk equal priority -asterisk equal priority 0asterisk equal priority 1asterisk equal priority 2asterisk equal priority 3asterisk equal priority 4asterisk equal priority 5asterisk equal priority 6asterisk equal priority 7asterisk equal priority 8asterisk equal priority 9asterisk end priority greater than preassociative priority asterisk factorial equal priority asterisk _ { asterisk } equal priority asterisk prime equal priority asterisk %0 equal priority asterisk %1 equal priority asterisk %2 equal priority asterisk %3 equal priority asterisk %4 equal priority asterisk %5 equal priority asterisk %6 equal priority asterisk %7 equal priority asterisk %8 equal priority asterisk %9 equal priority asterisk head equal priority asterisk tail equal priority asterisk raise equal priority asterisk catch equal priority asterisk catching maptag equal priority asterisk maptag equal priority asterisk untag equal priority asterisk boolp equal priority asterisk truep equal priority asterisk falsep equal priority asterisk intp equal priority asterisk pairp equal priority asterisk atom equal priority asterisk mapp equal priority asterisk objectp equal priority asterisk root equal priority asterisk Head equal priority asterisk Tail equal priority asterisk TheBool equal priority asterisk TheNat equal priority asterisk norm equal priority asterisk Tag equal priority asterisk BoolP equal priority asterisk IntP equal priority asterisk PairP equal priority asterisk ExP equal priority asterisk MapP equal priority asterisk ObjectP equal priority asterisk Sign equal priority asterisk Mag equal priority asterisk zeroth equal priority asterisk first equal priority asterisk second equal priority asterisk third equal priority asterisk fourth equal priority asterisk fifth equal priority asterisk sixth equal priority asterisk seventh equal priority asterisk eighth equal priority asterisk ninth equal priority asterisk ref equal priority asterisk idx equal priority asterisk debug equal priority asterisk [[ asterisk ]] equal priority asterisk [[ asterisk -> asterisk ]] equal priority asterisk [[ asterisk => asterisk ]] equal priority asterisk unquote equal priority asterisk# equal priority asterisk plist ( asterisk ) equal priority asterisk def ( asterisk , asterisk ) equal priority asterisk lhs ( asterisk , asterisk ) equal priority asterisk rhs ( asterisk , asterisk ) equal priority asterisk metadef ( asterisk ) equal priority asterisk metavar ( asterisk ) equal priority asterisk stmt-rhs ( asterisk ) equal priority asterisk proof-rhs ( asterisk ) equal priority asterisk tactic-rhs ( asterisk ) equal priority asterisk unitac-rhs ( asterisk ) equal priority asterisk locate-rhs ( asterisk ) equal priority asterisk mathdef ( asterisk ) equal priority asterisk valuedef ( asterisk ) equal priority asterisk objectvar ( asterisk ) equal priority asterisk objectlambda ( asterisk ) equal priority asterisk objectquote ( asterisk ) equal priority asterisk objectterm ( asterisk ) equal priority asterisk objectterm* ( asterisk ) equal priority asterisk metaterm ( asterisk ) equal priority asterisk metaterm* ( asterisk ) equal priority asterisk metaavoid ( asterisk ) asterisk equal priority asterisk metaavoid* ( asterisk ) asterisk equal priority asterisk objectavoid ( asterisk ) asterisk equal priority asterisk objectavoid* ( asterisk ) asterisk end priority greater than preassociative priority asterisk ' asterisk equal priority asterisk apply asterisk end priority greater than preassociative priority - asterisk equal priority + asterisk end priority greater than preassociative priority asterisk Times asterisk equal priority asterisk * asterisk end priority greater than preassociative priority asterisk Plus asterisk equal priority asterisk Minus asterisk equal priority asterisk + asterisk equal priority asterisk - asterisk equal priority asterisk set+ asterisk equal priority asterisk set- asterisk equal priority asterisk set-- asterisk equal priority asterisk union asterisk end priority greater than preassociative priority PlusTag asterisk equal priority MinusTag asterisk end priority greater than preassociative priority asterisk div asterisk equal priority asterisk mod asterisk end priority greater than postassociative priority asterisk LazyPair asterisk equal priority asterisk Pair asterisk equal priority asterisk NatPair asterisk equal priority asterisk :: asterisk end priority greater than postassociative priority asterisk ,, asterisk end priority greater than preassociative priority asterisk = asterisk equal priority asterisk != asterisk equal priority asterisk Equal asterisk equal priority asterisk LT asterisk equal priority asterisk < asterisk equal priority asterisk <= asterisk equal priority asterisk > asterisk equal priority asterisk >= asterisk equal priority asterisk r= asterisk equal priority asterisk t= asterisk equal priority asterisk t=* asterisk equal priority asterisk member asterisk equal priority asterisk subset asterisk equal priority asterisk set= asterisk equal priority asterisk sequent= asterisk end priority greater than preassociative priority Not asterisk equal priority .not. asterisk equal priority notnot asterisk equal priority p.not asterisk end priority greater than preassociative priority asterisk And asterisk equal priority asterisk .and. asterisk equal priority asterisk .then. asterisk equal priority asterisk &c asterisk end priority greater than preassociative priority asterisk Or asterisk equal priority asterisk .or. asterisk end priority greater than postassociative priority asterisk Iff asterisk equal priority asterisk p.imply asterisk end priority greater than preassociative priority asterisk Select asterisk else asterisk end select equal priority asterisk IN asterisk end priority greater than preassociative priority \ asterisk . asterisk equal priority If asterisk then asterisk else asterisk equal priority if asterisk then asterisk else asterisk equal priority newline asterisk equal priority LET asterisk BE asterisk equal priority let asterisk := asterisk in asterisk equal priority let asterisk = asterisk in asterisk equal priority metadeclare asterisk end priority greater than postassociative priority norm asterisk equal priority asterisk Guard asterisk equal priority asterisk is val : asterisk equal priority asterisk is bool : asterisk equal priority asterisk is int : asterisk equal priority asterisk is pair : asterisk equal priority asterisk is map : asterisk equal priority asterisk is object : asterisk end priority greater than preassociative priority asterisk reduce to asterisk equal priority asterisk == asterisk end priority greater than preassociative priority asterisk Init equal priority asterisk Ponens equal priority asterisk Probans equal priority asterisk Verify equal priority asterisk Curry equal priority asterisk Uncurry equal priority asterisk Deref equal priority asterisk At equal priority asterisk Infer equal priority asterisk Endorse equal priority asterisk All equal priority asterisk Conclude equal priority asterisk Rule end priority greater than preassociative priority asterisk at asterisk equal priority asterisk ponens asterisk equal priority asterisk probans asterisk equal priority asterisk verify asterisk equal priority asterisk p.mp asterisk end priority greater than postassociative priority asterisk infer asterisk equal priority asterisk endorse asterisk equal priority asterisk id est asterisk end priority greater than preassociative priority All asterisk : asterisk end priority greater than postassociative priority asterisk oplus asterisk end priority greater than preassociative priority asterisk conclude asterisk end priority greater than postassociative priority line asterisk : asterisk >> asterisk ; asterisk equal priority Line asterisk : asterisk >> asterisk ; asterisk equal priority line asterisk : asterisk >> asterisk ; equal priority line asterisk : asterisk >> asterisk qed equal priority line asterisk : Premise >> asterisk ; asterisk equal priority Line asterisk : Premise >> asterisk ; asterisk equal priority line asterisk : Condition >> asterisk ; asterisk equal priority Line asterisk : Condition >> asterisk ; asterisk equal priority line asterisk : Arbitrary >> asterisk ; asterisk equal priority line asterisk : Local >> asterisk = asterisk ; asterisk equal priority line asterisk : Block >> Begin ; asterisk line asterisk : Block >> End ; asterisk equal priority Line asterisk : Block >> Begin ; asterisk line asterisk : Block >> End ; asterisk end priority greater than postassociative priority asterisk ;; asterisk end priority greater than preassociative priority asterisk proves asterisk end priority greater than postassociative priority axiom asterisk : asterisk end axiom equal priority rule asterisk : asterisk end rule equal priority theory asterisk : asterisk end theory equal priority lemma asterisk : asterisk end lemma equal priority asterisk lemma asterisk : asterisk end lemma equal priority proof of asterisk : asterisk equal priority asterisk proof of asterisk : asterisk end priority greater than postassociative priority asterisk,asterisk equal priority asterisk[ asterisk ]asterisk equal priority asterisk[[ asterisk ]]asterisk equal priority asterisk[[[ asterisk ]]]asterisk equal priority dbug ( asterisk ) asterisk equal priority dbug* ( asterisk ) asterisk equal priority glue ( asterisk ) asterisk equal priority diag ( asterisk ) asterisk equal priority disp ( asterisk ) asterisk equal priority form ( asterisk ) asterisk equal priority glue' ( asterisk ) asterisk equal priority dbug' ( asterisk ) asterisk equal priority diag' ( asterisk ) asterisk equal priority disp' ( asterisk ) asterisk equal priority form' ( asterisk ) asterisk equal priority LocateProofLine ( asterisk , asterisk ) asterisk end priority greater than preassociative priority asterisk linebreak asterisk end priority greater than preassociative priority asterisk & asterisk end priority greater than preassociative priority asterisk \\ asterisk end priority greater than empty ]]"
\end {flushleft}



\end{document}
" end text ,, latex ( "chores" ) ,, latex ( "chores" ) ,, dvipdfm ( "chores" )

The pyk compiler, version 0.1.9 by Klaus Grue,
GRD-2007-07-12.UTC:20:11:58.175987 = MJD-54293.TAI:20:12:31.175987 = LGT-4690987951175987e-6