Logiweb(TM)

Logiweb expansion 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

"[ 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:

"[[[ define claim of check as test1 &c proofcheck end define ]]]"

\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:

"[[[ define macro of check as macro1 end define ]]]"

\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 "[[ define message of statement as "statement/kg" end define,define value of statement as norm "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 "[[ define message of proof as "proof/kg" end define,define value of proof as norm "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 "[[ define message of meta as "meta/kg" end define,define value of meta as norm "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 "[[ define message of math as "math/kg" end define,define value of math as norm "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 "[[ define message of tactic as "tactic/kg" end define,define value of tactic as norm "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 "[[ define message of unitac as "unitac/kg" end define,define value of unitac as norm "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 "[[ define message of locate as "locate/kg" end define,define value of locate as norm "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 "[[ define macro of statement define x as y end define as \ x . expand ( quote macro define statement define x as y end define as define statement of x as y end define end define end quote , x ) end define ]]".

\item "[[ define macro of proof define x as y end define as \ x . expand ( quote macro define proof define x as y end define as define proof of x as y end define end define end quote , x ) end define ]]".

\item "[[ define macro of meta define x as y end define as \ x . expand ( quote macro define meta define x as y end define as define meta of x as y end define end define end quote , x ) end define ]]".

\item "[[ define macro of math define x as y end define as \ x . expand ( quote macro define math define x as y end define as define math of x as y end define end define end quote , x ) end define ]]".

\item "[[ define macro of tactic define x as y end define as \ x . expand ( quote macro define tactic define x as y end define as define tactic of x as y end define end define end quote , x ) end define ]]".

\item "[[ define macro of unitac define x as y end define as \ x . expand ( quote macro define unitac define x as y end define as define unitac of x as y end define end define end quote , x ) end define ]]".

\item "[[ define macro of locate define x as y end define as \ x . expand ( quote 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 quote , x ) 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 ensure math define statement of L as #a infer #a end define end math end hide ]"

\noindent which is simply shorthand for "[[ hide define statement of L as #a infer #a end define end hide ]]". The lemma construct is defined thus: "[[ define macro of lemma x : y end lemma as \ x . expand ( quote macro define lemma x : y end lemma as ensure math statement define x as y end define end math end define end quote , x ) 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 ensure math define statement of T as p.MP oplus p.A1 oplus p.A2 oplus p.A3 end define end math end hide ]"

\noindent which is shorthand for "[[ hide define statement of T as p.MP oplus p.A1 oplus p.A2 oplus p.A3 end define end hide ]]". The theory construct is defined thus: "[[ define macro of theory x : y end theory as \ x . expand ( quote macro define theory x : y end theory as ensure math define statement of x as y end define end math end define end quote , x ) 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 ensure math define statement of p.A1 as All #a : All #b : A p.imply B p.imply A end define,define unitac of p.A1 as \ u . unitac-rule ( u ) end define end math end hide ]"

\noindent This is shorthand for "[[ hide define statement of p.A1 as All #a : All #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:

"[[[ define macro of axiom x : y end axiom as \ x . expand ( quote 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 end quote , x ) 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 : All #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:

"[[[ define macro of rule x : y end rule as \ x . expand ( quote 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 end quote , x ) 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:

"[[[ define macro of metadeclare x as \ x . expand ( quote macro define metadeclare x as meta define x as "var" end define end define end quote , x ) end define ]]]"

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

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:

"[[[ define meta of x# as "var" end define ]]]"

\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: "[[ define meta of tacfresh ( x ) as "var" end define ]]" and "[[ define meta of unifresh ( x , y ) as "var" end define ]]". 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 "[[ define value of x plist ( c ) as norm x is val : c is val : 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 "[[ define value of x def ( c , a ) as norm x is val : c is val : a is val : x plist ( c ) [[ a ]] end define ]]". Look up aspect "[[ a ]]" of symbol "[[ x ]]".

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

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

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

\item "[[ define value of x metavar ( c ) as norm x is val : c is val : x metadef ( c ) = "var" end define ]]". True if "[[ x ]]" is a meta variable.

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

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

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

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

\item "[[ define value of x locate-rhs ( c ) as norm x is val : c is val : 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 "[[ define meta of x infer y as "infer" end define ]]". States that provability of "[[ x ]]" implies provability of "[[ y ]]".

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

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

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

\item "[[ define meta of 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 ( check ) != 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 ( check ) = "var" ]]".

We shall say that a meta construct "[[ x ]]" is a \index{binder, meta}\indexintro{meta binder} iff "[[ x metadef ( check ) = "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 ( check ) = 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 "[[ check [[ 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 "[[ check [[ 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 ( check ) ]]" where we define "[[ x objectterm ( c ) ]]" in the following.

\begin{statements}

\item "[[ define value of x valuedef ( c ) as norm x is val : c is val : 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 "[[ define value of x mathdef ( c ) as norm x is val : c is val : x rhs ( c , math ) idx end define ]]". The math definition of "[[ x ]]". This is "[[ true ]]" for constructs with no math definition.

\item "[[ define value of x objectvar ( c ) as norm x is val : c is val : 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 "[[ define value of x objectlambda ( c ) as norm x is val : c is val : x metadef ( c ) = true .and. x valuedef ( c ) = 0 end define ]]". This is true if "[[ x ]]" is a lambda abstraction.

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

\item "[[ define value of x objectterm ( c ) as norm x is val : c is val : LET x metadef ( c ) BE asterisk IN LET asterisk BE d IN if d = "var" then true else if d != true then false else LET x valuedef ( c ) BE asterisk IN LET asterisk BE d IN if d = 0 then x first objectvar ( c ) .or. x first metavar ( c ) .and. x second objectterm ( c ) else if d = 1 then true else if d .and. x mathdef ( c ) then true else x tail objectterm* ( c ) end define ]]"

\item "[[ define value of x objectterm* ( c ) as norm x is val : c is val : 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 ( check ) ]]" where we define "[[ x metaterm ( c ) ]]" in the following.

\begin{statements}

\item "[[ define value of x metaterm ( c ) as norm x is val : c is val : LET x metadef ( c ) BE asterisk IN LET asterisk BE d IN if d = "var" then true else if d = "all" then x first metavar ( c ) .and. x second metaterm ( c ) else if d != true then x tail metaterm* ( c ) else x objectterm ( c ) end define ]]"

\item "[[ define value of x metaterm* ( c ) as norm x is val : c is val : 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 "[[ define value of x metaavoid ( c ) y as norm x is val : c is val : y is val : 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 "[[ define value of x metaavoid* ( c ) y as norm x is val : c is val : y is val : if y atom then true else 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 "[[ define value of metaavoid1 ( x , y , c ) as norm x is val : y is val : c is val : LET y metadef ( c ) BE asterisk IN LET asterisk BE d IN if d = "var" then .not. x t= y else if d = "all" then x t= y first .or. metaavoid1 ( x , y second , c ) else if d != true then metaavoid1* ( x , y tail , c ) else LET y valuedef ( c ) BE asterisk IN LET asterisk BE d IN if d = 1 then true else metaavoid1* ( x , y tail , c ) end define ]]"

\item "[[ define value of metaavoid1* ( x , y , c ) as norm x is val : y is val : c is val : 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 "[[ define value of distinctvar ( x , c ) as norm x is val : c is val : 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 "[[ define value of x objectavoid* ( c ) y as norm x is val : c is val : y is val : 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 "[[ define value of x objectavoid ( c ) y as norm x is val : c is val : y is val : x :: <<>> objectavoid* ( c ) y end define ]]". Same as above except that "[[ x ]]" is a term rather than a list of terms.

\item "[[ define value of objectavoid1 ( x , y , c , r ) as norm x is val : y is val : c is val : r is val : if x = <<>> then r else LET y metadef ( c ) BE asterisk IN LET asterisk BE d IN if d = "var" then r set+ y else LET y valuedef ( c ) BE asterisk IN LET asterisk BE d IN if d = true then if y member x then false raise else r else if d = 0 then objectavoid1 ( x set- y first , y second , c , r ) else if d = 1 then r else objectavoid1* ( x , y tail , c , r ) end define ]]"

\item "[[ define value of objectavoid1* ( x , y , c , r ) as norm x is val : y is val : c is val : r is val : 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 "[[ define value of metafree ( x , y , z , c ) as norm x is val : y is val : z is val : c is val : LET x metadef ( c ) BE asterisk IN LET asterisk BE d IN if d = "var" then true else if d = true then z objectterm ( c ) .or. y metaavoid ( c ) x else if d != "all" then metafree* ( x tail , y , z , c ) else if y t= x first then true else if y metaavoid ( c ) x second then true else 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 "[[ define value of metafree* ( x , y , z , c ) as norm x is val : y is val : z is val : c is val : 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 "[[ define value of objectfree ( x , y , z , c ) as norm x is val : y is val : z is val : c is val : if x metadef ( c ) != true then false else LET x valuedef ( c ) BE asterisk IN LET asterisk BE d IN if d = true then true else if d = 1 then true else if d != 0 then objectfree* ( x tail , y , z , c ) else if y t= x first then true else if y objectavoid ( c ) x second then true else 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 "[[ define value of objectfree* ( x , y , z , c ) as norm x is val : y is val : z is val : c is val : 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 "[[ define value of metasubst ( x , s , c ) as norm x is val : s is val : c is val : LET x metadef ( c ) BE asterisk IN LET asterisk BE d IN if d = "var" then lookup ( x , s , x ) else if d != "all" then x head :: metasubst* ( x tail , s , c ) else LET remove ( x first , s ) BE asterisk IN LET asterisk BE s IN x head :: x first :: metasubst ( x second , s , c ) :: <<>> end define ]]".

\item "[[ define value of metasubst* ( x , s , c ) as norm x is val : s is val : c is val : if x atom then true else 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 "[[ define value of metasubstc ( x , s , c ) as norm x is val : s is val : c is val : metasubstc1 ( x , s , true , c ) end define ]]"

\item "[[ define value of metasubstc1 ( x , s , b , c ) as norm x is val : s is val : b is val : c is val : LET x metadef ( c ) BE asterisk IN LET asterisk BE d IN if d = "var" then metasubstc3 ( x , s , b , c ) else if d then metasubstc2 ( x , s , b , c ) else if d != "all" then x head :: metasubstc1* ( x tail , s , b , c ) else LET remove ( x first , s ) BE asterisk IN LET asterisk BE s IN x head :: x first :: metasubstc1 ( x second , s , x first :: b , c ) :: <<>> end define ]]".

\item "[[ define value of metasubstc1* ( x , s , b , c ) as norm x is val : s is val : b is val : c is val : if x atom then true else metasubstc1 ( x head , s , b , c ) :: metasubstc1* ( x tail , s , b , c ) end define ]]"

\item "[[ define value of metasubstc2 ( x , s , b , c ) as norm x is val : s is val : b is val : c is val : LET x metadef ( c ) BE asterisk IN LET asterisk BE d IN if d then x head :: metasubstc2* ( x tail , s , b , c ) else LET lookup ( x , s , true ) BE asterisk IN LET asterisk BE v IN if v then x else LET v metadef ( c ) BE asterisk IN LET asterisk BE d IN if .not. d .and. d != "var" then error ( x , LocateProofLine ( x , c ) diag ( "Substitution of" ) disp ( x ) diag ( "with" ) disp ( v ) diag ( "produces non-meta-term" ) end diagnose ) else if metaavoid2* ( b , v , c ) then v else 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 "[[ define value of metasubstc2* ( x , s , b , c ) as norm x is val : s is val : b is val : c is val : if x atom then true else metasubstc2 ( x head , s , b , c ) :: metasubstc2* ( x tail , s , b , c ) end define ]]"

\item "[[ define value of metaavoid2* ( x , y , c ) as norm x is val : y is val : c is val : x .or. x head metaavoid ( c ) y .and. metaavoid2* ( x tail , y , c ) end define ]]"

\item "[[ define value of metasubstc3 ( x , s , b , c ) as norm x is val : s is val : b is val : c is val : LET lookup ( x , s , true ) BE asterisk IN LET asterisk BE v IN if v then x else if metaavoid2* ( b , v , c ) then v else 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 "[[ define value of remove ( x , s ) as norm x is val : s is val : if s atom then s else if x t= s head head then remove ( x , s tail ) else s head :: remove ( x , s tail ) end define ]]"

\end{statements}



\subsection{Quantifiers}

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

\begin{statements}

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

\item "[[ define value of expand-All ( x ) as norm x is val : LET x BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE u IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE v IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET stateexpand ( u , s , c ) BE asterisk IN LET asterisk BE u IN LET stateexpand ( v , s , c ) BE asterisk IN LET asterisk BE v IN expand-All1 ( t , u , v ) end define ]]"

\item "[[ define value of expand-All1 ( t , u , v ) as norm t is val : u is val : v is val : if .not. u r= quote x ,, y end quote then make-root ( t , quote All u unquote : v unquote end quote ) :: u :: v :: true else 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 "[[ define value of x member y as norm x is val : y is val : if y atom then false else x t= y head .or. x member y tail end define ]]". Membership of a set of terms.

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

\item "[[ define value of x set- y as norm x is val : y is val : if y member x then x set-- y else x end define ]]". Remove the term "[[ y ]]" from the set "[[ x ]]" of terms.

\item "[[ define value of x set-- y as norm x is val : y is val : if x atom then true else if x head t= y then x tail else x head :: x tail set-- y end define ]]"

\item "[[ define value of x subset y as norm x is val : y is val : if x atom then true else x head member y .and. x tail subset y end define ]]"

\item "[[ define value of x union y as norm x is val : y is val : if x atom then y else x tail union y set+ x head end define ]]"

\item "[[ define value of x set= y as norm x is val : y is val : 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 "[[ define value of x sequent= y as norm x is val : y is val : 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 "[[ define meta of x Init as "Init" end define ]]". Allows to build a sequent with "[[ x ]]" as both premise and result.

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

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

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

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

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

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

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

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

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

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

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

\item "[[ define meta of 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 "[[ define meta of 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 "[[ define meta of 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 "[[ define meta of 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 "[[ define meta of 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 "[[ define meta of x At as "At" end define ]]". Same as "[[ x at y ]]" but leaves it to unification to determine "[[ y ]]".

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

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

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

\item "[[ define meta of 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.

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



\subsection{Error message construct}

The "[[ define value of error ( x , y ) as norm x is val : y is val : 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 "[[ define value of mismatch ( x , y , c ) as norm x is val : y is val : c is val : LET x metadef ( c ) BE asterisk IN LET asterisk BE a IN if a = true then false else if a != y metadef ( c ) then true else mismatch* ( x tail , y tail , c ) end define ]]"



\item "[[ define value of mismatch* ( x , y , c ) as norm x is val : y is val : c is val : if x atom .and. y atom then false else if x atom .or. y atom then true else 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 "[[ define value of seqeval ( t , c ) as norm t is val : c is val : if t r= quote x Init end quote then eval-Init ( t first , c ) else if t r= quote x Ponens end quote then eval-Ponens ( seqeval ( t first , c ) , t first , c ) else if t r= quote x Probans end quote then eval-Probans ( seqeval ( t first , c ) , t first , c ) else if t r= quote x Verify end quote then eval-Verify ( seqeval ( t first , c ) , t first , c ) else if t r= quote x Curry end quote then eval-Curry ( seqeval ( t first , c ) , t first , c ) else if t r= quote x Uncurry end quote then eval-Uncurry ( seqeval ( t first , c ) , t first , c ) else if t r= quote x Deref end quote then eval-Deref ( seqeval ( t first , c ) , t first , c ) else if t r= quote x at y end quote then eval-at ( t , true , c ) else if t r= quote x infer y end quote then eval-infer ( t first , seqeval ( t second , c ) , t second , c ) else if t r= quote x endorse y end quote then eval-endorse ( t first , seqeval ( t second , c ) , t second , c ) else if t r= quote x id est y end quote then eval-ie ( seqeval ( t first , c ) , t second , t first , c ) else if t r= quote All x : y end quote then eval-all ( t first , seqeval ( t second , c ) , t second , c ) else if t r= quote x ;; y end quote then eval-cut ( seqeval ( t first , c ) , seqeval ( t second , c ) , c ) else 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 "[[ define value of eval-Init ( x , c ) as norm x is val : c is val : if x metaterm ( c ) then x :: <<>> :: <<>> :: x :: <<>> else error ( x , LocateProofLine ( x , c ) diag ( "Init-seqop used on non-meta term:" ) disp ( x ) end diagnose ) end define ]]"



\item "[[ define value of eval-Ponens ( x , d , c ) as norm x is val : d is val : c is val : LET x BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN if mismatch ( quote x infer y end quote , R , c ) then error ( d , LocateProofLine ( d , c ) diag ( "Ponens-seqop used on non-inference:" ) disp ( R ) end diagnose ) else LET R BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE P prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN P set+ P prime :: C :: R prime :: <<>> end define ]]"



\item "[[ define value of eval-Probans ( x , d , c ) as norm x is val : d is val : c is val : LET x BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN if mismatch ( quote x endorse y end quote , R , c ) then error ( d , LocateProofLine ( d , c ) diag ( "Probans-seqop used on non-endorsement:" ) disp ( R ) end diagnose ) else LET R BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN P :: C set+ C prime :: R prime :: <<>> end define ]]"



\item "[[ define value of eval-Verify ( x , d , c ) as norm x is val : d is val : c is val : LET x BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN if mismatch ( quote x endorse y end quote , R , c ) then error ( d , LocateProofLine ( d , c ) diag ( "Verify-seqop used on non-endorsement:" ) disp ( R ) end diagnose ) else LET R BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN if eval ( C prime , true , c ) apply c maptag untag catch = false :: true then P :: C :: R prime :: <<>> else error ( d , LocateProofLine ( d , c ) diag ( "Verify-seqop used on false condition:" ) disp ( C prime ) end diagnose ) end define ]]"



\item "[[ define value of eval-Curry ( x , d , c ) as norm x is val : d is val : c is val : LET x BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN if mismatch ( quote x oplus y infer z end quote , R , c ) then error ( d , LocateProofLine ( d , c ) diag ( "Curry-seqop used on unfit argument:" ) disp ( R ) end diagnose ) else LET R BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime prime IN LET asterisk prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime tail BE asterisk prime prime prime prime IN LET asterisk BE X IN LET asterisk prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime tail BE asterisk prime prime prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime prime prime IN LET asterisk prime prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime prime tail BE asterisk prime prime prime prime prime IN LET asterisk BE Y IN LET asterisk prime prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime prime tail BE asterisk prime prime prime prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE Z IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN P :: C :: make-root ( R , quote X unquote infer Y unquote infer Z unquote end quote ) :: X :: make-root ( R , quote Y unquote infer Z unquote end quote ) :: Y :: Z :: true :: true :: <<>> end define ]]"



\item "[[ define value of eval-Uncurry ( x , d , c ) as norm x is val : d is val : c is val : LET x BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN if mismatch ( quote x infer y infer z end quote , R , c ) then error ( d , LocateProofLine ( d , c ) diag ( "Uncurry-seqop used on unfit argument:" ) disp ( R ) end diagnose ) else LET R BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE X IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime prime IN LET asterisk prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime tail BE asterisk prime prime prime prime IN LET asterisk prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime tail BE asterisk prime prime prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime prime prime IN LET asterisk prime prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime prime tail BE asterisk prime prime prime prime prime IN LET asterisk BE Y IN LET asterisk prime prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime prime tail BE asterisk prime prime prime prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime prime prime prime IN LET asterisk prime prime prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime prime prime tail BE asterisk prime prime prime prime prime prime IN LET asterisk BE Z IN LET asterisk prime prime prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime prime prime tail BE asterisk prime prime prime prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN P :: C :: make-root ( R , quote X unquote oplus Y unquote infer Z unquote end quote ) :: make-root ( R , quote X unquote oplus Y unquote end quote ) :: X :: Y :: true :: Z :: true :: <<>> end define ]]"



\item "[[ define value of eval-Deref ( x , d , c ) as norm x is val : d is val : c is val : LET x BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET R stmt-rhs ( c ) BE asterisk IN LET asterisk BE R prime IN if R prime = true then error ( d , LocateProofLine ( d , c ) diag ( "Deref-seqop used on undefined statement:" ) disp ( R ) end diagnose ) else if R prime metaterm ( c ) then P :: C :: R prime :: <<>> else 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 "[[ define value of eval-at ( x , v , c ) as norm x is val : v is val : c is val : if .not. x r= quote x at y end quote then LET seqeval ( x , c ) BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN P :: C :: eval-at1 ( R , v , true , x , c ) :: <<>> else if x second metaterm ( c ) then eval-at ( x first , x second :: v , c ) else error ( x , LocateProofLine ( x , c ) diag ( "At-seqop used on non-meta-term:" ) disp ( x second ) end diagnose ) end define ]]"

\item "[[ define value of eval-at1 ( R , v , s , d , c ) as norm R is val : v is val : s is val : d is val : c is val : if v then metasubstc ( R , s , c ) else 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 eval-at1 ( R second , v tail , R first :: v head :: s , d , c ) end define ]]"



\item "[[ define value of eval-infer ( x , y , d , c ) as norm x is val : y is val : d is val : c is val : if .not. x metaterm ( c ) then error ( d , LocateProofLine ( d , c ) diag ( "Infer-seqop used on non-meta term:" ) disp ( x ) end diagnose ) else LET y BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN P set- x :: C :: make-root ( R , quote x unquote infer R unquote end quote ) :: x :: R :: true :: <<>> end define ]]"



\item "[[ define value of eval-endorse ( x , y , d , c ) as norm x is val : y is val : d is val : c is val : if .not. x metaterm ( c ) then error ( d , LocateProofLine ( d , c ) diag ( "Endorse-seqop used on non-meta term:" ) disp ( x ) end diagnose ) else LET y BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN P :: C set- x :: make-root ( R , quote x unquote endorse R unquote end quote ) :: x :: R :: true :: <<>> end define ]]"



\item "[[ define value of eval-ie ( x , y , d , c ) as norm x is val : y is val : d is val : c is val : LET x BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN if R t= y stmt-rhs ( c ) then P :: C :: y :: <<>> else 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 "[[ define value of eval-all ( x , y , d , c ) as norm x is val : y is val : d is val : c is val : LET y BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN if .not. x metaavoid* ( c ) P then 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 if .not. x metaavoid* ( c ) C then 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 P :: C :: make-root ( R , quote All x unquote : R unquote end quote ) :: x :: R :: true :: <<>> end define ]]"



\item "[[ define value of eval-cut ( x , y , c ) as norm x is val : y is val : c is val : LET x BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET y BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN 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 "[[ define locate of 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 "[[ define locate of 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 "[[ define locate of 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 "[[ define locate of 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 "[[ define locate of line asterisk : asterisk >> asterisk ; as "line" :: 1 end define ]]"

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

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

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

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

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

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

\end{statements}



\subsection{Error message generation}

\begin{statements}

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

\item "[[ define value of dbug ( x ) y as norm x is val : y is val : if y debug != true then y else make-root ( x , y ) :: dbug* ( x ) y tail end define ]]"

\item "[[ define value of dbug* ( x ) y as norm x is val : y is val : if y then true else dbug ( x ) y head :: dbug* ( x ) y tail end define ]]"

\item "[[ define value of glue ( x ) y as norm x is val : y is val : make-root ( true , name quote glue' ( x ) y end quote end name ) :: make-string ( true , x ) :: y :: <<>> end define ]]"

\item "[[ define value of diag ( x ) y as norm x is val : y is val : make-root ( true , name quote diag' ( x ) y end quote end name ) :: make-string ( true , x ) :: y :: <<>> end define ]]"

\item "[[ define value of disp ( x ) y as norm x is val : y is val : make-root ( true , name quote disp' ( x ) y end quote end name ) :: x :: y :: <<>> end define ]]"

\item "[[ define value of form ( x ) y as norm x is val : y is val : make-root ( true , name quote form' ( x ) y end quote end name ) :: x :: y :: <<>> end define ]]"

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

\end{statements}



\subsection{Error location}

\begin{statements}

\item "[[ define value of Locate ( t , s , c ) as norm t is val : s is val : c is val : LET reverse ( t debug head ) catch BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE d IN LET Locate1 ( d tail , c [[ d head ]] [[ "body" ]] , s , true , c ) catch BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE e IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE v IN 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 "[[ define value of Locate1 ( d , t , s , r , c ) as norm d is val : t is val : s is val : r is val : c is val : if t then r else LET t locate-rhs ( c ) BE asterisk IN LET asterisk BE v IN LET if v then true else eval ( v , true , c ) untag BE asterisk IN LET asterisk BE v IN LET if v head = s then t :: v tail else r BE asterisk IN LET asterisk BE r IN if d atom then r else Locate1 ( d tail , nth ( d head , t tail ) , s , r , c ) end define ]]"

\item "[[ define value of LocateProofLine ( v , c ) y as norm v is val : c is val : y is val : LET Locate ( v , "proof" , c ) BE asterisk IN LET asterisk BE p IN LET Locate ( v , "line" , c ) BE asterisk IN LET asterisk BE l IN if .not. p .and. .not. l then dbug ( v ) diag ( "Line" ) form ( nth ( l tail , l head ) ) diag ( "in proof of" ) form ( nth ( p tail , p head ) ) glue ( ":\newline " ) y else if .not. p then dbug ( v ) diag ( "In proof of" ) form ( nth ( p tail , p head ) ) glue ( ":\newline " ) y else 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 "[[ define value of claiming ( x , y ) as norm x is val : y is val : if .not. y r= quote u &c v end quote then x t= y else 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 "[[ define value of proofcheck as \ c . proofcheck1 ( c ) end define ]]".

Suited as conjunct in the claim of a page.

\item "[[ define claim of check as test1 &c proofcheck end define ]]".

Use both proofcheck and test1 as verifiers.

\item "[[ define value of proofcheck1 ( c ) as norm c is val : LET proofcheck2 ( c ) catch BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE e IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE v IN if v != true then v else if .not. e then true else 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 "[[ define value of proofcheck2 ( c ) as norm c is val : LET c [[ 0 ]] BE asterisk IN LET asterisk BE r IN LET seqeval* ( c [[ r ]] [[ "codex" ]] [[ r ]] , c ) BE asterisk IN LET asterisk BE a IN LET circularitycheck1 ( r , c , a , a ) BE asterisk IN LET asterisk BE x 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 "[[ define value of seqeval* ( a , c ) as norm a is val : c is val : if a = true then true else LET a BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE x IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE y IN if .not. x intp then seqeval* ( x , c ) :: seqeval* ( y , c ) else LET y [[ 0 ]] [[ proof ]] BE asterisk IN LET asterisk BE d IN if d = true then true else print ( d second ) .then. LET eval ( d third , true , c ) apply d maptag apply c maptag untag [[ hook-arg ]] catch BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE e IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE p IN if e .and. p then error ( d second , diag ( "Malformed proof of" ) form ( d second ) end diagnose ) else if e then p raise else LET seqeval ( p , c ) catch BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE e IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE S IN if e .and. S then error ( d second , diag ( "Malformed sequent proof of" ) form ( d second ) end diagnose ) else if e then S raise else LET S BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE P IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE C IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE R IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN if C != <<>> then error ( d second , diag ( "In proof of" ) form ( d second ) glue ( ":\newline " ) diag ( "Unchecked sidecondition:" ) disp ( C head ) end diagnose ) else LET y [[ 0 ]] [[ statement ]] BE asterisk IN LET asterisk BE l IN if l = true then error ( d second , diag ( "Proof of non-existent lemma:" ) disp ( d second ) end diagnose ) else if .not. l third t= R then 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 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 "[[ define value of premisecheck* ( P , c ) as norm P is val : c is val : 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 "[[ define value of checked ( r , c ) as norm r is val : c is val : LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ 0 ]] [[ 0 ]] [[ "claim" ]] third BE asterisk IN LET asterisk BE x IN if claiming ( quote proofcheck end quote , x ) then true else if .not. x then false else LET c [[ r ]] [[ "bibliography" ]] first BE asterisk IN LET asterisk BE r IN if r then false else LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ 0 ]] [[ 0 ]] [[ "claim" ]] third BE asterisk IN LET asterisk BE x IN claiming ( quote proofcheck end quote , x ) end define ]]". True if the page with reference "[[ r ]]" has been checked by "[[ proofcheck ]]".

\item "[[ define value of premisecheck ( P , c ) as norm P is val : c is val : LET P ref BE asterisk IN LET asterisk BE r IN LET P idx BE asterisk IN LET asterisk BE i IN if c [[ r ]] [[ "diagnose" ]] != true then error ( P , diag ( "Lemma" ) disp ( P ) diag ( "occurs on a page with a non-empty diagnose." ) diag ( "Avoid referencing that lemma." ) end diagnose ) else if .not. checked ( r , c ) then 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 if P proof-rhs ( c ) then 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 "[[ define value of circularitycheck1 ( r , c , a , q ) as norm r is val : c is val : a is val : q is val : if a = true then q else LET a BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE x IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE y IN 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 "[[ define value of circularitycheck2 ( r , c , i , q ) as norm r is val : c is val : i is val : q is val : LET q [[ i ]] BE asterisk IN LET asterisk BE v IN if v = 0 then LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ proof ]] second BE asterisk IN LET asterisk BE n IN error ( n , diag ( "Circular proof. The vicious circle includes lemma" ) disp ( n ) end diagnose ) else if v = 1 then q else circularitycheck2* ( r , c , v head , q [[ i -> 0 ]] ) [[ i -> 1 ]] end define ]]".

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

\item "[[ define value of circularitycheck2* ( r , c , l , q ) as norm r is val : c is val : l is val : q is val : if l atom then q else LET l BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE p IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE l IN LET circularitycheck2* ( r , c , l , q ) BE asterisk IN LET asterisk BE q IN 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 "[[ define statement of lemma1 as All #x : All #y : #x infer #y infer #x end define ]]".

Manually stated lemma for testing.

\item "[[ define proof of 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 "[[ define value of int2string ( t , v ) as norm t is val : v is val : if v > 0 then 0 :: int2string1 ( v , "" ) :: t debug :: <<>> else if v = 0 then 0 :: "0" :: t debug :: <<>> else 0 :: %% %2 %5 %6 * int2string1 ( - v , "" ) + logand ( "-" , %% %2 %5 %5 ) :: t debug :: <<>> end define ]]"

\item "[[ define value of int2string1 ( v , r ) as norm v is val : r is val : if v = 0 then r else LET logand ( "0" , %% %2 %5 %5 ) BE asterisk IN LET asterisk BE z IN LET floor ( v , %% %1 %0 ) BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE x IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE y IN int2string1 ( x , %% %2 %5 %6 * r + z + y ) end define ]]"

\item "[[ define value of val2term ( t , v ) as norm t is val : v is val : if v = true then make-root ( t , quote true end quote ) :: true else if v = false then make-root ( t , quote false end quote ) :: true else if v pairp then make-root ( t , quote val2term ( t , v head ) unquote :: val2term ( t , v tail ) unquote end quote ) :: val2term ( t , v head ) :: val2term ( t , v tail ) :: true else if v mapp then make-root ( t , quote map ( --- ) end quote ) :: make-root ( t , quote --- end quote ) :: true :: true else if v objectp then make-root ( t , quote object ( val2term ( t , destruct ( v ) ) unquote ) end quote ) :: val2term ( t , destruct ( v ) ) :: true else if v = 0 then make-root ( t , quote 0 end quote ) :: true else if v < 0 then make-root ( t , quote - card2term ( t , - v ) unquote end quote ) :: card2term ( t , - v ) :: true else card2term ( t , v ) end define ]]"

\item "[[ define value of card2term ( t , v ) as norm t is val : v is val : if v = 0 then make-root ( t , quote %% end quote ) :: true else if evenp ( v ) then make-root ( t , quote card2term ( t , half ( v ) ) unquote %0 end quote ) :: card2term ( t , half ( v ) ) :: true else make-root ( t , quote card2term ( t , half ( v ) ) unquote %1 end quote ) :: card2term ( t , half ( v ) ) :: true end define ]]".

\end{statements}



\subsection{Unification}

\begin{statements}

\item "[[ define value of univar ( t , v , i ) as norm t is val : v is val : i is val : make-root ( t , quote unifresh ( v unquote , int2string ( t , i ) unquote ) end quote ) :: v :: int2string ( t , i ) :: true end define ]]"

\item "[[ define value of pterm ( t , c ) as norm t is val : c is val : 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 "[[ define value of pterm1 ( t , s , n , c ) as norm t is val : s is val : n is val : c is val : LET t metadef ( c ) BE asterisk IN LET asterisk BE d IN if d != "all" then pterm2 ( t , s , c ) else LET univar ( t first , t first , n ) BE asterisk IN LET asterisk BE v IN LET pterm1 ( t second , t first :: v :: s , n + 1 , c ) BE asterisk IN LET asterisk BE t prime IN make-root ( t , quote All v unquote : t prime unquote end quote ) :: v :: t prime :: true end define ]]".

\item "[[ define value of pterm2 ( t , s , c ) as norm t is val : s is val : c is val : LET t metadef ( c ) BE asterisk IN LET asterisk BE d IN LET if d = "all" then t first :: t first :: s else s BE asterisk IN LET asterisk BE s IN if d != "var" then t head :: pterm2* ( t tail , s , c ) else LET lookup ( t , s , true ) BE asterisk IN LET asterisk BE n IN if n = true then t else n end define ]]"

\item "[[ define value of pterm2* ( t , s , c ) as norm t is val : s is val : c is val : if t atom then true else pterm2 ( t head , s , c ) :: pterm2* ( t tail , s , c ) end define ]]"

\item "[[ define value of inst ( t , d , a ) as norm t is val : d is val : a is val : if .not. t r= quote unifresh ( true , true ) end quote then t ref :: t idx :: d debug :: inst* ( t tail , d , a ) else LET a [[ t second idx ]] BE asterisk IN LET asterisk BE u IN if u != true then inst ( u , d , a ) else 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 "[[ define value of inst* ( t , d , a ) as norm t is val : d is val : a is val : if t atom then true else inst ( t head , d , a ) :: inst* ( t tail , d , a ) end define ]]".

\item "[[ define value of occur ( t , u , s ) as norm t is val : u is val : s is val : if u r= quote unifresh ( true , true ) end quote then t t= u .or. occur ( t , s [[ u second idx ]] , s ) else occur* ( t , u tail , s ) end define ]]".

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

\item "[[ define value of occur* ( t , u , s ) as norm t is val : u is val : s is val : if u atom then false else occur ( t , u head , s ) .or. occur* ( t , u tail , s ) end define ]]".

\item "[[ define value of unify ( t , u , s ) as norm t is val : u is val : s is val : if t r= quote unifresh ( true , true ) end quote then unify2 ( t , u , s ) else if u r= quote unifresh ( true , true ) end quote then unify2 ( u , t , s ) else if t r= u then unify* ( t tail , u tail , s ) else 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 "[[ define value of unify* ( t , u , s ) as norm t is val : u is val : s is val : if t atom then s else unify* ( t tail , u tail , unify ( t head , u head , s ) ) end define ]]".

\item "[[ define value of unify2 ( t , u , s ) as norm t is val : u is val : s is val : if t t= u then s else LET s [[ t second idx ]] BE asterisk IN LET asterisk BE t prime IN if t prime != true then unify ( t prime , u , s ) else 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 "[[ define value of hook-arg as norm "arg" end define ]]"

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

\item "[[ define value of hook-res as norm "con" end define ]]"

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

\item "[[ define value of hook-idx as norm "idx" end define ]]"

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

\item "[[ define value of hook-uni as norm "uni" end define ]]"

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

\item "[[ define value of hook-pre as norm "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 "[[ define value of hook-cond as norm "cond" end define ]]"

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

\item "[[ define value of hook-parm as norm "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 "[[ define value of taceval ( t , s , c ) as norm t is val : s is val : c is val : LET t tactic-rhs ( c ) BE asterisk IN LET asterisk BE d IN if .not. d then eval ( d , true , c ) apply t :: s :: c :: <<>> maptag untag else LET lookup ( t , s [[ hook-pre ]] , true ) BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE r IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE a IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN if .not. a then s [[ hook-res -> r ]] [[ hook-arg -> a ]] else error ( t , diag ( "Unknown tactic operator in root of argumentation:" ) disp ( t ) end diagnose ) end define ]]".

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

\item "[[ define value of tactic-push ( n , v , s ) as norm n is val : v is val : s is val : s [[ n -> v :: s [[ n ]] ]] end define ]]"

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

\item "[[ define value of tactic-pop ( n , s ) as norm n is val : s is val : 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 "[[ define value of taceval1 ( t , p , c ) as norm t is val : p is val : c is val : LET t tactic-rhs ( c ) BE asterisk IN LET asterisk BE d IN LET make-root ( t , quote t unquote infer p unquote end quote ) :: t :: p :: true BE asterisk IN LET asterisk BE t IN if d then taceval ( t , tacstate0 , c ) else 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 "[[ define macro of x lemma y : z end lemma as \ x . expand ( quote 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 end quote , x ) 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 "[[ define macro of proof of x : y as \ x . expand ( quote 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 end quote , x ) end define ]]".

A proof is the same as a proof definition.

\item "[[ define macro of x proof of y : z as \ x . expand ( quote 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 end quote , x ) 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 "[[ define macro of line l : a >> x ; as \ x . expand ( quote macro define line l : a >> x ; as a conclude x end define end quote , x ) end define ]]"

\item "[[ define macro of line l : a >> x qed as \ x . expand ( quote macro define line l : a >> x qed as a conclude x end define end quote , x ) end define ]]"

\item "[[ define macro of line l : Arbitrary >> x ; n as \ x . expand ( quote macro define line l : Arbitrary >> x ; n as All x : n end define end quote , x ) end define ]]"

\item "[[ define macro of line l : Local >> x = y ; n as \ x . expand ( quote macro define line l : Local >> x = y ; n as let x := y in n end define end quote , x ) end define ]]"

\end{statements}



\section{Tactic definitions of sequent operators}

\subsection{Init tactic}

\begin{statements}

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

\item "[[ define value of tactic-Init ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE x IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN s [[ hook-arg -> t ]] [[ hook-res -> x ]] end define ]]"

\end{statements}



\subsection{Ponens tactic}

\begin{statements}

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

\item "[[ define value of tactic-Ponens ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE x IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET taceval ( x , s , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote s [[ hook-arg ]] unquote Ponens end quote ) :: s [[ hook-arg ]] :: true BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN if mismatch ( quote x infer y end quote , r , c ) then error ( t , diag ( "Ponens tactic used on non-inference:" ) disp ( r ) end diagnose ) else s [[ hook-arg -> a ]] [[ hook-res -> r second ]] end define ]]"

\end{statements}



\subsection{Probans tactic}

\begin{statements}

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

\item "[[ define value of tactic-Probans ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE x IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET taceval ( x , s , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote s [[ hook-arg ]] unquote Probans end quote ) :: s [[ hook-arg ]] :: true BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN if mismatch ( quote x endorse y end quote , r , c ) then error ( t , diag ( "Probans tactic used on non-endorsement:" ) disp ( r ) end diagnose ) else s [[ hook-arg -> a ]] [[ hook-res -> r second ]] end define ]]"

\end{statements}



\subsection{Verify tactic}

\begin{statements}

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

\item "[[ define value of tactic-Verify ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE x IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET taceval ( x , s , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote s [[ hook-arg ]] unquote Verify end quote ) :: s [[ hook-arg ]] :: true BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN if mismatch ( quote x endorse y end quote , r , c ) then error ( t , diag ( "Verify tactic used on non-endorsement:" ) disp ( r ) end diagnose ) else s [[ hook-arg -> a ]] [[ hook-res -> r second ]] end define ]]"

\end{statements}



\subsection{Curry tactic}

\begin{statements}

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

\item "[[ define value of tactic-Curry ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE x IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET taceval ( x , s , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote s [[ hook-arg ]] unquote Curry end quote ) :: s [[ hook-arg ]] :: true BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN if mismatch ( quote x oplus y infer z end quote , r , c ) then error ( t , diag ( "Curry tactic used on unfit argument:" ) disp ( r ) end diagnose ) else LET make-root ( r , quote r first first unquote infer r first second unquote infer r second unquote end quote ) :: r first first :: make-root ( r , quote r first second unquote infer r second unquote end quote ) :: r first second :: r second :: true :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Uncurry tactic}

\begin{statements}

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

\item "[[ define value of tactic-Uncurry ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE x IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET taceval ( x , s , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote s [[ hook-arg ]] unquote Uncurry end quote ) :: s [[ hook-arg ]] :: true BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN if mismatch ( quote x infer y infer z end quote , r , c ) then error ( t , diag ( "Uncurry tactic used on unfit argument:" ) disp ( r ) end diagnose ) else LET make-root ( r , quote r first unquote oplus r second first unquote infer r second second unquote end quote ) :: make-root ( r , quote r first unquote oplus r second first unquote end quote ) :: r first :: r second first :: true :: r second second :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Deref tactic}

\begin{statements}

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

\item "[[ define value of tactic-Deref ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE x IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET taceval ( x , s , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote s [[ hook-arg ]] unquote Deref end quote ) :: s [[ hook-arg ]] :: true BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET r stmt-rhs ( c ) BE asterisk IN LET asterisk BE r prime IN if r prime = true then error ( t , diag ( "Deref tactic used on undefined statement:" ) disp ( r ) end diagnose ) else 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 "[[ define tactic of x at y as \ u . tactic-at ( u ) end define ]]".

\item "[[ define value of tactic-at ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN tactic-at1 ( t , s , true , c ) end define ]]"

\item "[[ define value of tactic-at1 ( t , s , v , c ) as norm t is val : s is val : v is val : c is val : if mismatch ( quote x at y end quote , t , c ) then tactic-at2 ( t , taceval ( t , s , c ) , v , true , c ) else LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE x IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE y IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET tactic-push ( hook-parm , y , s ) BE asterisk IN LET asterisk BE s IN tactic-at1 ( x , s , y :: v , c ) end define ]]"

\item "[[ define value of tactic-at2 ( t , s , v , s prime , c ) as norm t is val : s is val : v is val : s prime is val : c is val : if v then s [[ hook-res -> metasubst ( s [[ hook-res ]] , s prime , c ) ]] else LET v BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE y IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE v IN LET make-root ( t , quote s [[ hook-arg ]] unquote at y unquote end quote ) :: s [[ hook-arg ]] :: y :: true BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN if mismatch ( quote All x : y end quote , r , c ) then error ( t , diag ( "At tactic used on non-quantifier:" ) disp ( r ) end diagnose ) else LET s [[ hook-arg -> a ]] [[ hook-res -> r second ]] BE asterisk IN LET asterisk BE s IN 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 "[[ define tactic of x infer y as \ u . tactic-infer ( u ) end define ]]".

\item "[[ define value of tactic-infer ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE x IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE y IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET tactic-push ( hook-pre , true :: x :: make-root ( x , quote x unquote Init end quote ) :: x :: true :: <<>> , s ) BE asterisk IN LET asterisk BE s IN LET taceval ( y , s , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote x unquote infer s [[ hook-arg ]] unquote end quote ) :: x :: s [[ hook-arg ]] :: true BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote x unquote infer s [[ hook-res ]] unquote end quote ) :: x :: s [[ hook-res ]] :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Endorse tactic}

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

\begin{statements}

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

\item "[[ define value of tactic-endorse ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE x IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE y IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET taceval ( y , tactic-push ( hook-cond , true :: x :: <<>> , s ) , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote x unquote endorse s [[ hook-arg ]] unquote end quote ) :: x :: s [[ hook-arg ]] :: true BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote x unquote endorse s [[ hook-res ]] unquote end quote ) :: x :: s [[ hook-res ]] :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Id est tactic}

\begin{statements}

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

\item "[[ define value of tactic-ie ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE x IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE y IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET taceval ( x , s , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote s [[ hook-arg ]] unquote id est y unquote end quote ) :: s [[ hook-arg ]] :: y :: true BE asterisk IN LET asterisk BE a IN s [[ hook-arg -> a ]] [[ hook-res -> y ]] end define ]]"

\end{statements}



\subsection{All tactic}

Pop instantiations from the ``parameters'' stack.

\begin{statements}

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

\item "[[ define value of tactic-all ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE x IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE y IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET taceval ( y , tactic-pop ( hook-parm , s ) , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote All x unquote : s [[ hook-arg ]] unquote end quote ) :: x :: s [[ hook-arg ]] :: true BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote All x unquote : s [[ hook-res ]] unquote end quote ) :: x :: s [[ hook-res ]] :: true BE asterisk IN LET asterisk BE r IN 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 "[[ define tactic of x ;; y as \ u . tactic-cut ( u ) end define ]]".

\item "[[ define value of tactic-cut ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE x IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE y IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET taceval ( x , s , c ) BE asterisk IN LET asterisk BE s prime IN LET s prime [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET s prime [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET tactic-push ( hook-pre , true :: r :: make-root ( r , quote r unquote Init end quote ) :: r :: true :: <<>> , s ) BE asterisk IN LET asterisk BE s IN LET taceval ( y , s , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote a unquote ;; s [[ hook-arg ]] unquote end quote ) :: a :: s [[ hook-arg ]] :: true BE asterisk IN LET asterisk BE a IN s [[ hook-arg -> a ]] end define ]]"

\end{statements}



\section{Unification tactic}

\subsection{Main definitions}

\begin{statements}

\item "[[ define tactic of 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 "[[ define value of unitac ( x ) as norm x is val : LET x BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unitac1 ( t , s , c ) catch BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE e IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE v IN if .not. e then v else if .not. v then error ( t , LocateProofLine ( t , c ) v ) else error ( t , LocateProofLine ( t , c ) diag ( "During unification: Uncaught exception" ) 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 "[[ define value of unitac1 ( t , s , c ) as norm t is val : s is val : c is val : LET s [[ hook-idx -> 1 ]] [[ hook-uni -> true ]] BE asterisk IN LET asterisk BE s IN LET unieval ( t , s , c ) BE asterisk IN LET asterisk BE s IN LET inst ( s [[ hook-arg ]] , t , s [[ hook-uni ]] ) BE asterisk IN LET asterisk BE t IN LET taceval ( t , s , c ) catch BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE e IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE v IN if .not. e then v else if .not. v then v raise else error ( t , diag ( "Post unification tactic evalutation: Uncaught exception" ) 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 "[[ define value of unitac-adapt ( t , s , c ) as norm t is val : s is val : c is val : if t = "var" then s else LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET r metadef ( c ) BE asterisk IN LET asterisk BE d IN if d = "var" then s else if d = t then s else if d = "infer" then unitac-adapt ( t , s [[ hook-arg -> make-root ( a , quote a unquote Ponens end quote ) :: a :: true ]] [[ hook-res -> r second ]] , c ) else if d = "endorse" then unitac-adapt ( t , s [[ hook-arg -> make-root ( a , quote a unquote Verify end quote ) :: a :: true ]] [[ hook-res -> r second ]] , c ) else if d = "all" then LET s [[ hook-idx ]] BE asterisk IN LET asterisk BE i IN LET s [[ hook-idx -> i + 1 ]] BE asterisk IN LET asterisk BE s IN LET univar ( a , r first , i ) BE asterisk IN LET asterisk BE v IN LET metasubst ( r second , r first :: v :: <<>> , c ) BE asterisk IN LET asterisk BE r prime IN unitac-adapt ( t , s [[ hook-arg -> make-root ( a , quote a unquote at v unquote end quote ) :: a :: v :: true ]] [[ hook-res -> r prime ]] , c ) else if t then s else error ( a , diag ( "Cannot convert" ) disp ( r ) 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 "[[ define value of unieval ( t , s , c ) as norm t is val : s is val : c is val : LET t unitac-rhs ( c ) BE asterisk IN LET asterisk BE d IN if d then LET lookup ( t , s [[ hook-pre ]] , true ) BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE r IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE a IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN if .not. a then s [[ hook-arg -> a ]] [[ hook-res -> r ]] else error ( t , diag ( "Unknown unitac operator in root of argumentation:" ) disp ( t ) end diagnose ) else LET eval ( d , true , c ) apply t :: s :: c :: <<>> maptag untag catch BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE e IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE s IN if .not. e then s else if .not. s then s raise else error ( t , 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 "[[ define unitac of x Init as \ u . unitac-Init ( u ) end define ]]"

\item "[[ define value of unitac-Init ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN 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 "[[ define unitac of x Ponens as \ u . unitac-Ponens ( u ) end define ]]"

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

\item "[[ define value of unitac-Ponens ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET unitac-adapt ( "infer" , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> make-root ( t , quote a unquote Ponens end quote ) :: a :: true ]] [[ 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 "[[ define value of unitac-ponens ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET unitac-adapt ( "infer" , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET unieval ( t second , s , c ) BE asterisk IN LET asterisk BE s IN LET unitac-adapt ( r first metadef ( c ) , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a prime IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r prime IN LET s [[ hook-uni ]] BE asterisk IN LET asterisk BE u IN LET unify ( r first , r prime , u ) BE asterisk IN LET asterisk BE u IN LET s [[ hook-uni -> u ]] BE asterisk IN LET asterisk BE s IN s [[ hook-arg -> make-root ( t , quote a prime unquote ;; a unquote Ponens end quote ) :: a prime :: make-root ( t , quote a unquote Ponens end quote ) :: a :: true :: true ]] [[ 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 "[[ define unitac of x Probans as \ u . unitac-Probans ( u ) end define ]]"

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

\item "[[ define value of unitac-Probans ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET unitac-adapt ( "endorse" , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> make-root ( t , quote a unquote Probans end quote ) :: a :: true ]] [[ 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 "[[ define value of unitac-probans ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET unitac-adapt ( "endorse" , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET s [[ hook-uni ]] BE asterisk IN LET asterisk BE u IN LET lookup ( t second , s [[ hook-cond ]] , t second :: <<>> ) BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE p IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET unify ( r first , p , u ) BE asterisk IN LET asterisk BE u IN LET s [[ hook-uni -> u ]] BE asterisk IN LET asterisk BE s IN s [[ hook-arg -> make-root ( t , quote a unquote Probans end quote ) :: a :: true ]] [[ 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 "[[ define unitac of x Verify as \ u . unitac-Verify ( u ) end define ]]"

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

\item "[[ define value of unitac-Verify ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET unitac-adapt ( "endorse" , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> make-root ( t , quote a unquote Verify end quote ) :: a :: true ]] [[ 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 "[[ define value of unitac-verify ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET unitac-adapt ( "endorse" , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET s [[ hook-uni ]] BE asterisk IN LET asterisk BE u IN LET unify ( r first , t second , u ) BE asterisk IN LET asterisk BE u IN LET s [[ hook-uni -> u ]] BE asterisk IN LET asterisk BE s IN s [[ hook-arg -> make-root ( t , quote a unquote Verify end quote ) :: a :: true ]] [[ 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 "[[ define unitac of x Curry as \ u . unitac-Curry ( u ) end define ]]"

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

\item "[[ define value of unitac-Curry ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET unitac-adapt ( "infer" , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN if .not. r first r= quote x oplus y end quote then error ( r , diag ( "Unsuited for currying:" ) disp ( r ) end diagnose ) else LET make-root ( r , quote r first first infer r first second infer r second end quote ) :: make-root ( r , quote r first first end quote ) :: make-root ( r , quote r first end quote ) :: make-root ( r , quote r end quote ) :: true :: true :: true :: make-root ( r , quote r first second infer r second end quote ) :: make-root ( r , quote r first second end quote ) :: make-root ( r , quote r first end quote ) :: make-root ( r , quote r end quote ) :: true :: true :: true :: make-root ( r , quote r second end quote ) :: make-root ( r , quote r end quote ) :: true :: true :: true :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> make-root ( t , quote a unquote Curry end quote ) :: a :: true ]] [[ 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 "[[ define value of unitac-Uncurry ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET unitac-adapt ( "infer" , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN if .not. r second r= quote x infer y end quote then error ( r , diag ( "Unsuited for uncurrying:" ) disp ( r ) end diagnose ) else LET make-root ( r , quote r first oplus r second first infer r second second end quote ) :: make-root ( r , quote r first oplus r second first end quote ) :: make-root ( r , quote r first end quote ) :: make-root ( r , quote r end quote ) :: true :: true :: make-root ( r , quote r second first end quote ) :: make-root ( r , quote r second end quote ) :: make-root ( r , quote r end quote ) :: true :: true :: true :: true :: make-root ( r , quote r second second end quote ) :: make-root ( r , quote r second end quote ) :: make-root ( r , quote r end quote ) :: true :: true :: true :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> make-root ( t , quote a unquote Uncurry end quote ) :: a :: true ]] [[ 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 "[[ define unitac of x At as \ u . unitac-At ( u ) end define ]]"

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

\item "[[ define value of unitac-At ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET unitac-adapt ( "all" , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET s [[ hook-idx ]] BE asterisk IN LET asterisk BE i IN LET s [[ hook-idx -> i + 1 ]] BE asterisk IN LET asterisk BE s IN LET univar ( a , r first , i ) BE asterisk IN LET asterisk BE v IN LET make-root ( t , quote a unquote at v unquote end quote ) :: a :: v :: true BE asterisk IN LET asterisk BE a IN LET metasubst ( r second , r first :: v :: <<>> , c ) BE asterisk IN LET asterisk BE r IN 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 "[[ define value of unitac-at ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET unitac-adapt ( "all" , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET s [[ hook-idx ]] BE asterisk IN LET asterisk BE i IN LET s [[ hook-idx -> i + 1 ]] BE asterisk IN LET asterisk BE s IN LET univar ( a , r first , i ) BE asterisk IN LET asterisk BE v IN LET make-root ( t , quote a unquote at v unquote end quote ) :: a :: v :: true BE asterisk IN LET asterisk BE a IN LET metasubst ( r second , r first :: v :: <<>> , c ) BE asterisk IN LET asterisk BE r IN LET s [[ hook-uni ]] BE asterisk IN LET asterisk BE u IN LET unify ( t second , v , u ) BE asterisk IN LET asterisk BE u IN LET s [[ hook-uni -> u ]] BE asterisk IN LET asterisk BE s IN 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 "[[ define unitac of x Deref as \ u . unitac-Deref ( u ) end define ]]"

\item "[[ define value of unitac-Deref ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET unitac-adapt ( true , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET r stmt-rhs ( c ) BE asterisk IN LET asterisk BE l IN if l then s else LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote a unquote Deref end quote ) :: a :: true BE asterisk IN LET asterisk BE a IN 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 "[[ define unitac of x id est y as \ u . unitac-idest ( u ) end define ]]"

\item "[[ define value of unitac-idest ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET t second stmt-rhs ( c ) BE asterisk IN LET asterisk BE l IN LET unitac-adapt ( l metadef ( c ) , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET s [[ hook-uni ]] BE asterisk IN LET asterisk BE u IN LET unify ( r , l , u ) BE asterisk IN LET asterisk BE u IN LET s [[ hook-uni -> u ]] BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote a unquote id est t second unquote end quote ) :: a :: t second :: true BE asterisk IN LET asterisk BE a IN 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 "[[ define unitac of x Infer as \ u . unitac-Infer ( u ) end define ]]"

\item "[[ define value of unitac-Infer ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-idx ]] BE asterisk IN LET asterisk BE i IN LET s [[ hook-idx -> i + 1 ]] BE asterisk IN LET asterisk BE s IN LET univar ( t , quote cla end quote , i ) BE asterisk IN LET asterisk BE v IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote v unquote infer r unquote end quote ) :: v :: r :: true BE asterisk IN LET asterisk BE r IN LET make-root ( t , quote v unquote infer a unquote end quote ) :: v :: a :: true BE asterisk IN LET asterisk BE a IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

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

\item "[[ define value of unitac-infer ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t second , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote t first unquote infer r unquote end quote ) :: t first :: r :: true BE asterisk IN LET asterisk BE r IN LET make-root ( t , quote t first unquote infer a unquote end quote ) :: t first :: a :: true BE asterisk IN LET asterisk BE a IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Endorse}

\begin{statements}

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

\item "[[ define value of unitac-Endorse ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-idx ]] BE asterisk IN LET asterisk BE i IN LET s [[ hook-idx -> i + 1 ]] BE asterisk IN LET asterisk BE s IN LET univar ( t , quote cla end quote , i ) BE asterisk IN LET asterisk BE v IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote v unquote endorse r unquote end quote ) :: v :: r :: true BE asterisk IN LET asterisk BE r IN LET make-root ( t , quote v unquote endorse a unquote end quote ) :: v :: a :: true BE asterisk IN LET asterisk BE a IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

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

\item "[[ define value of unitac-endorse ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t second , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote t first unquote endorse r unquote end quote ) :: t first :: r :: true BE asterisk IN LET asterisk BE r IN LET make-root ( t , quote t first unquote endorse a unquote end quote ) :: t first :: a :: true BE asterisk IN LET asterisk BE a IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{All}

\begin{statements}

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

\item "[[ define value of unitac-All ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-idx ]] BE asterisk IN LET asterisk BE i IN LET s [[ hook-idx -> i + 1 ]] BE asterisk IN LET asterisk BE s IN LET univar ( t , quote cla end quote , i ) BE asterisk IN LET asterisk BE v IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote All v unquote : r unquote end quote ) :: v :: r :: true BE asterisk IN LET asterisk BE r IN LET make-root ( t , quote All v unquote : a unquote end quote ) :: v :: a :: true BE asterisk IN LET asterisk BE a IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

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

\item "[[ define value of unitac-all ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t second , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote All t first unquote : r unquote end quote ) :: t first :: r :: true BE asterisk IN LET asterisk BE r IN LET make-root ( t , quote All t first unquote : a unquote end quote ) :: t first :: a :: true BE asterisk IN LET asterisk BE a IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Cut}

\begin{statements}

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

\item "[[ define value of unitac-cut ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a prime IN LET unieval ( t second , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote a prime unquote ;; a unquote end quote ) :: a prime :: a :: true BE asterisk IN LET asterisk BE a IN 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 "[[ define unitac of x Conclude as \ u . unitac-Conclude ( u ) end define ]]"

\item "[[ define value of unitac-Conclude ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN 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 "[[ define value of hook-unitac as norm "unitac" end define ]]"

\item "[[ define value of tacstate0 as norm 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 "[[ define value of hook-lemma as norm "lemma" end define ]]"

\item "[[ define value of hook-rule as norm "rule" end define ]]"

\item "[[ define value of hook-conclude as norm "conclude" end define ]]"

\item "[[ define value of unitac0 as norm 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 "[[ define unitac of x conclude y as \ u . unitac-conclude ( u ) end define ]]"

\item "[[ define value of unitac-conclude ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET s [[ hook-unitac ]] [[ hook-conclude ]] BE asterisk IN LET asterisk BE d IN eval ( d , true , c ) apply t :: s :: c :: <<>> maptag untag end define ]]"

\item "[[ define value of unitac-conclude-std ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unieval ( t first , s , c ) BE asterisk IN LET asterisk BE s IN LET unitac-adapt ( t second metadef ( c ) , s , c ) BE asterisk IN LET asterisk BE s IN LET unify ( s [[ hook-res ]] , t second , s [[ hook-uni ]] ) BE asterisk IN LET asterisk BE u IN 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 : All #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 "[[ define unitac of r Rule as \ u . unitac-Rule ( u ) end define ]]"

\item "[[ define value of unitac-Rule ( x ) as norm x is val : LET x BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t first BE asterisk IN LET asterisk BE r IN LET unitac-theo ( r , s , c ) BE asterisk IN LET asterisk BE a IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"



\item "[[ define value of unitac-rule ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET s [[ hook-unitac ]] [[ hook-rule ]] BE asterisk IN LET asterisk BE d IN eval ( d , true , c ) apply t :: s :: c :: <<>> maptag untag end define ]]"

\item "[[ define value of unitac-rule-std ( x ) as norm x is val : LET x BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t stmt-rhs ( c ) BE asterisk IN LET asterisk BE r IN LET unitac-theo ( t , s , c ) BE asterisk IN LET asterisk BE a IN LET make-root ( r , quote a unquote Deref end quote ) :: a :: true BE asterisk IN LET asterisk BE a IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\item "[[ define value of unitac-theo ( t , s , c ) as norm t is val : s is val : c is val : LET reverse ( s [[ hook-pre ]] ) BE asterisk IN LET asterisk BE p IN 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 "[[ define value of unitac-rule0 ( r , P , c ) as norm r is val : P is val : c is val : LET unitac-rule1 ( r , P , c ) BE asterisk IN LET asterisk BE p IN if .not. p then p else if r metadef ( c ) = "plus" then unitac-rule-plus ( r , P , c ) else LET r stmt-rhs ( c ) BE asterisk IN LET asterisk BE d IN if .not. d then unitac-rule-stmt ( d , r , P , c ) else error ( r , diag ( "No locally assumed theory includes the following rule:" ) disp ( r ) 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 "[[ define value of unitac-rule-plus ( R , P , c ) as norm R is val : P is val : c is val : LET R BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE r IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE r prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unitac-rule0 ( r , P , c ) BE asterisk IN LET asterisk BE p IN if p then true else LET unitac-rule0 ( r prime , P , c ) BE asterisk IN LET asterisk BE p prime IN if p prime then true else make-root ( 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 ) :: p :: make-root ( R , quote p prime unquote ;; r unquote oplus r prime unquote infer r unquote oplus r prime unquote Init Curry Ponens Ponens end quote ) :: p prime :: make-root ( R , quote r unquote oplus r prime unquote infer r unquote oplus r prime unquote Init Curry Ponens Ponens end quote ) :: make-root ( R , quote r unquote oplus r prime unquote infer r unquote oplus r prime unquote Init Curry Ponens end quote ) :: make-root ( R , quote r unquote oplus r prime unquote infer r unquote oplus r prime unquote Init Curry end quote ) :: make-root ( R , quote r unquote oplus r prime unquote infer r unquote oplus r prime unquote Init end quote ) :: make-root ( R , quote r unquote oplus r prime unquote end quote ) :: r :: r prime :: true :: make-root ( R , quote r unquote oplus r prime unquote Init end quote ) :: make-root ( R , quote r unquote oplus r prime unquote end quote ) :: r :: r prime :: true :: true :: true :: true :: true :: true :: true :: true 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 "[[ define value of unitac-rule-stmt ( d , r , P , c ) as norm d is val : r is val : P is val : c is val : LET unitac-rule0 ( d , P , c ) BE asterisk IN LET asterisk BE p IN if p then true else make-root ( r , quote p unquote ;; d unquote Init id est r unquote end quote ) :: p :: make-root ( r , quote d unquote Init id est r unquote end quote ) :: make-root ( r , quote d unquote Init end quote ) :: d :: true :: r :: true :: true end define ]]"

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

\item "[[ define value of unitac-rule1 ( r , P , c ) as norm r is val : P is val : c is val : if P atom then true else unitac-rule2 ( r , P head first , c ) .and. 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 "[[ define value of unitac-rule2 ( r , T , c ) as norm r is val : T is val : c is val : LET unitac-search ( r , T , c ) BE asterisk IN LET asterisk BE p IN if p then true else 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 "[[ define value of unitac-search ( r , T , c ) as norm r is val : T is val : c is val : 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 "[[ define value of unitac-search1 ( r , T , p , a , c ) as norm r is val : T is val : p is val : a is val : c is val : if r t= T then reverse ( a ) :: p raise else LET T stmt-rhs ( c ) BE asterisk IN LET asterisk BE T prime IN if .not. T prime then unitac-search1 ( r , T prime , reverse ( a ) :: p , T prime :: <<>> , c ) else if T metadef ( c ) != "plus" then true else unitac-search1 ( r , T first , p , "head" :: a , c ) .and. 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 "[[ define value of unitac-rule3 ( r , p ) as norm r is val : p is val : LET unitac-rule4 ( r , p head ) BE asterisk IN LET asterisk BE q IN if p tail then q else LET unitac-rule3 ( r , p tail ) BE asterisk IN LET asterisk BE p IN make-root ( r , quote p unquote Deref ;; q unquote end quote ) :: make-root ( r , quote p unquote Deref end quote ) :: p :: true :: q :: true end define ]]"



\item "[[ define value of unitac-rule4 ( r , a ) as norm r is val : a is val : LET unitac-rule5 ( r , a head , a tail , true ) BE asterisk IN LET asterisk BE p IN make-root ( r , quote p unquote Ponens end quote ) :: p :: true 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 "[[ define value of unitac-rule5 ( r , T , a , s ) as norm r is val : T is val : a is val : s is val : if a atom then LET unitac-stack ( r , s , make-root ( r , quote T unquote Init end quote ) :: T :: true ) BE asterisk IN LET asterisk BE p IN make-root ( r , quote T unquote infer p unquote end quote ) :: T :: p :: true else LET a BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE e IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE a IN if e = "head" then make-root ( r , quote unitac-rule5 ( r , T first , a , T second :: s ) unquote Uncurry end quote ) :: unitac-rule5 ( r , T first , a , T second :: s ) :: true else make-root ( r , quote T first unquote infer unitac-rule5 ( r , T second , a , s ) unquote Uncurry end quote ) :: make-root ( r , quote T first unquote infer unitac-rule5 ( r , T second , a , s ) unquote end quote ) :: T first :: unitac-rule5 ( r , T second , a , s ) :: true :: true 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 "[[ define value of unitac-stack ( r , s , t ) as norm r is val : s is val : t is val : if s atom then t else LET s BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE p IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE s IN LET unitac-stack ( r , s , t ) BE asterisk IN LET asterisk BE t IN make-root ( r , quote p unquote infer t unquote end quote ) :: p :: t :: true end define ]]".

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

\end{statements}



\subsection{Lemmas}

\begin{statements}

\item "[[ define value of unitac-lemma ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET s [[ hook-unitac ]] [[ hook-lemma ]] BE asterisk IN LET asterisk BE d IN eval ( d , true , c ) apply t :: s :: c :: <<>> maptag untag end define ]]"

\item "[[ define value of unitac-lemma-std ( x ) as norm x is val : LET x BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t stmt-rhs ( c ) BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE T IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE r IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET unitac-theo ( T , s , c ) BE asterisk IN LET asterisk BE a prime IN LET make-root ( t , quote a prime unquote ;; t unquote Init Deref Ponens end quote ) :: a prime :: make-root ( t , quote t unquote Init Deref Ponens end quote ) :: make-root ( t , quote t unquote Init Deref end quote ) :: make-root ( t , quote t unquote Init end quote ) :: t :: true :: true :: true :: true BE asterisk IN LET asterisk BE a IN 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 "[[ define macro of line l : a >> x ; n as \ x . expand ( quote macro define line l : a >> x ; n as Line l : a >> x ; n end define end quote , x ) end define ]]"

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

\item "[[ define value of tactic-conclude-cut ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE l IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE a IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime prime IN LET asterisk prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime tail BE asterisk prime prime prime prime IN LET asterisk BE x IN LET asterisk prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime tail BE asterisk prime prime prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime prime prime IN LET asterisk prime prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime prime tail BE asterisk prime prime prime prime prime IN LET asterisk BE n IN LET asterisk prime prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime prime tail BE asterisk prime prime prime prime prime IN LET taceval ( make-root ( t , quote a unquote conclude x unquote end quote ) :: a :: x :: true , s , c ) BE asterisk IN LET asterisk BE s prime IN LET s prime [[ hook-arg ]] BE asterisk IN LET asterisk BE a prime IN LET s prime [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET tactic-push ( hook-pre , l :: r :: make-root ( r , quote r unquote Init end quote ) :: r :: true :: <<>> , s ) BE asterisk IN LET asterisk BE s IN LET taceval ( n , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN s [[ hook-arg -> make-root ( t , quote a prime unquote ;; a unquote end quote ) :: a prime :: a :: true ]] end define ]]"

\end{statements}



\subsection{Premise line}

\begin{statements}

\item "[[ define macro of line l : Premise >> x ; n as \ x . expand ( quote macro define line l : Premise >> x ; n as Line l : Premise >> x ; n end define end quote , x ) end define ]]"

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

\item "[[ define value of tactic-premise-line ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE l IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE x IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime prime IN LET asterisk prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime tail BE asterisk prime prime prime prime IN LET asterisk BE n IN LET asterisk prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime tail BE asterisk prime prime prime prime IN LET taceval ( n , tactic-push ( hook-pre , l :: x :: make-root ( x , quote x unquote Init end quote ) :: x :: true :: <<>> , s ) , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote x unquote infer s [[ hook-arg ]] unquote end quote ) :: x :: s [[ hook-arg ]] :: true BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote x unquote infer s [[ hook-res ]] unquote end quote ) :: x :: s [[ hook-res ]] :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Condition line}

\begin{statements}

\item "[[ define macro of line l : Condition >> x ; n as \ x . expand ( quote macro define line l : Condition >> x ; n as Line l : Condition >> x ; n end define end quote , x ) end define ]]"

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

\item "[[ define value of tactic-condition-line ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE l IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE x IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime prime IN LET asterisk prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime tail BE asterisk prime prime prime prime IN LET asterisk BE n IN LET asterisk prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime tail BE asterisk prime prime prime prime IN LET taceval ( n , tactic-push ( hook-cond , l :: x :: <<>> , s ) , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote x unquote endorse s [[ hook-arg ]] unquote end quote ) :: x :: s [[ hook-arg ]] :: true BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote x unquote endorse s [[ hook-res ]] unquote end quote ) :: x :: s [[ hook-res ]] :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{Blocks}

\begin{statements}

\item "[[ define macro of line l : Block >> Begin ; x line k : Block >> End ; n as \ x . expand ( quote 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 end quote , x ) end define ]]"

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

\item "[[ define value of tactic-block ( u ) as norm u is val : LET u BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE t IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE s IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE c IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET t BE asterisk IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET asterisk BE l IN LET asterisk prime prime head BE asterisk IN LET asterisk prime prime tail BE asterisk prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET asterisk BE x IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime prime IN LET asterisk prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime tail BE asterisk prime prime prime prime IN LET asterisk BE k IN LET asterisk prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime tail BE asterisk prime prime prime prime IN LET if asterisk atom then asterisk else asterisk head :: if asterisk atom then asterisk else asterisk tail :: true BE asterisk prime prime prime prime prime IN LET asterisk prime prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime prime tail BE asterisk prime prime prime prime prime IN LET asterisk BE n IN LET asterisk prime prime prime prime prime head BE asterisk IN LET asterisk prime prime prime prime prime tail BE asterisk prime prime prime prime prime IN LET taceval ( x , s , c ) BE asterisk IN LET asterisk BE s prime IN LET s prime [[ hook-arg ]] BE asterisk IN LET asterisk BE a prime IN LET s prime [[ hook-res ]] BE asterisk IN LET asterisk BE r IN LET tactic-push ( hook-pre , k :: r :: make-root ( r , quote r unquote Init end quote ) :: r :: true :: <<>> , s ) BE asterisk IN LET asterisk BE s IN LET taceval ( n , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN s [[ hook-arg -> make-root ( t , quote a prime unquote ;; a unquote end quote ) :: a prime :: a :: true ]] 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 ]]").

"[ ensure math define statement of p.A1 as All #x : All #y : #x p.imply #y p.imply #x end define,define unitac of p.A1 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of p.A2 as All #x : All #y : All #z : #x p.imply #y p.imply #z p.imply #x p.imply #y p.imply #x p.imply #z end define,define unitac of p.A2 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of p.A3 as All #x : All #y : p.not #y p.imply p.not #x p.imply p.not #y p.imply #x p.imply #y end define,define unitac of p.A3 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of p.MP as All #x : All #y : #x p.imply #y infer #x infer #y end define,define unitac of p.MP as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of p.IProp as p.A1 oplus p.A2 oplus p.MP end define end math ]"

"[ ensure math define statement of p.Prop as p.IProp oplus p.A3 end define end math ]"

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

"[[[ define macro of x p.mp y as \ x . expand ( quote macro define x p.mp y as p.MP ponens x ponens y Conclude end define end quote , x ) 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}:



"[ ensure math define statement of lemma2 as p.Prop infer All #x : #x p.imply #x end define,define unitac of lemma2 as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma2 as \ p . \ c . taceval1 ( quote p.Prop end quote , quote All #x : Line L02 : p.A2 >> #x p.imply #y p.imply #x p.imply #x p.imply #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 : p.MP ponens L02 ponens L03 Conclude >> #x p.imply #y p.imply #x p.imply #x p.imply #x ; Line L05 : p.A1 >> #x p.imply #y p.imply #x ; p.MP ponens L04 ponens L05 Conclude conclude #x p.imply #x end quote , c ) end define end math ]"

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

"[ ensure math define statement of lemma2a as p.Prop infer All #x : #x p.imply #x end define,define unitac of lemma2a as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma2a as \ p . \ c . taceval1 ( quote p.Prop end quote , quote All #x : Line L04 : p.MP ponens p.A2 ponens p.A1 Conclude >> #x p.imply #y p.imply #x p.imply #x p.imply #x ; Line L05 : p.A1 >> #x p.imply #y p.imply #x ; p.MP ponens L04 ponens L05 Conclude conclude #x p.imply #x end quote , c ) end define end math ]"

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

"[ ensure math define statement of lemma2b as p.Prop infer All #x : #x p.imply #x end define,define unitac of lemma2b as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma2b as \ p . \ c . taceval1 ( quote p.Prop end quote , quote All #x : Line L05 : p.A1 >> #x p.imply #y p.imply #x ; p.MP ponens p.MP ponens p.A2 ponens p.A1 Conclude ponens L05 Conclude conclude #x p.imply #x end quote , c ) end define end math ]"

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

"[ ensure math define statement of lemma2c as p.Prop infer All #x : #x p.imply #x end define,define unitac of lemma2c as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma2c as \ p . \ c . taceval1 ( quote p.Prop end quote , quote All #x : p.MP ponens p.MP ponens p.A2 ponens p.A1 Conclude ponens p.A1 At at #y Conclude conclude #x p.imply #x end quote , c ) end define end math ]"

\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:

"[ ensure math define statement of lemma2d as p.Prop infer All #x : #x p.imply #x end define,define unitac of lemma2d as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma2d as \ p . \ c . taceval1 ( quote p.Prop end quote , quote All #x : p.MP ponens p.MP ponens p.A2 ponens p.A1 Conclude ponens p.A1 At at #y Conclude conclude All #x : #x p.imply #x end quote , c ) end define end math ]"

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

"[ ensure math define statement of lemma2e as p.Prop infer All #x : #x p.imply #x end define,define unitac of lemma2e as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma2e as \ p . \ c . taceval1 ( quote p.Prop end quote , quote p.MP ponens p.MP ponens p.A2 ponens p.A1 Conclude ponens p.A1 At at #y Conclude All conclude All #x : #x p.imply #x end quote , c ) end define end math ]"

\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:

"[ ensure math define statement of lemma2f as p.IProp oplus p.A3 infer All #x : #x p.imply #x end define,define unitac of lemma2f as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma2f as \ p . \ c . taceval1 ( quote p.IProp oplus p.A3 end quote , quote All #x : p.MP ponens p.MP ponens p.A2 ponens p.A1 Conclude ponens p.A1 At at #y Conclude conclude #x p.imply #x end quote , c ) end define end math ]"



\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.

"[ ensure math define statement of lemma3 as p.Prop infer All #x : #x infer #x end define,define unitac of lemma3 as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma3 as \ p . \ c . taceval1 ( quote p.Prop end quote , quote Line L01 : Block >> Begin ; All #x : Line L03 : Premise >> #x ; L03 conclude #x line L05 : Block >> End ; L05 ponens L05 conclude All #x : #x infer #x end quote , c ) end define end math ]"



\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.

"[ ensure math define statement of System S as S.S1 oplus S.S5 end define end math ]"

"[ ensure math define statement of S.S1 as All #x : All #y : All #z : #x = #y infer #x = #z infer #y = #z end define,define unitac of S.S1 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of S.S5 as All #x : #x + 0 = #x end define,define unitac of S.S5 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of S.reflexivity as System S infer All #x : #x = #x end define,define unitac of S.reflexivity as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of S.reflexivity as \ p . \ c . taceval1 ( quote System S end quote , quote All #x : Line L02 : S.S5 >> #x + 0 = #x ; S.S1 ponens L02 ponens L02 conclude #x = #x end quote , c ) end define end math ]"



\subsection{Rules}



"[ ensure math define statement of lemma4a as p.Prop infer p.IProp end define,define unitac of lemma4a as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma4a as \ p . \ c . taceval1 ( quote p.Prop end quote , quote p.IProp Rule conclude p.IProp end quote , c ) end define end math ]"



"[ ensure math define statement of lemma4b as p.Prop infer p.A1 end define,define unitac of lemma4b as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma4b as \ p . \ c . taceval1 ( quote p.Prop end quote , quote p.A1 Rule conclude p.A1 end quote , c ) end define end math ]"



"[ ensure math define statement of lemma4c as p.Prop infer p.A2 end define,define unitac of lemma4c as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma4c as \ p . \ c . taceval1 ( quote p.Prop end quote , quote p.A2 Rule conclude p.A2 end quote , c ) end define end math ]"



"[ ensure math define statement of lemma4d as p.Prop infer p.A3 end define,define unitac of lemma4d as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma4d as \ p . \ c . taceval1 ( quote p.Prop end quote , quote p.A3 Rule conclude p.A3 end quote , c ) end define end math ]"



"[ ensure math define statement of lemma4e as p.IProp oplus p.A3 infer p.Prop end define,define unitac of lemma4e as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma4e as \ p . \ c . taceval1 ( quote p.IProp oplus p.A3 end quote , quote p.Prop Rule conclude p.Prop end quote , c ) end define end math ]"



"[ ensure math define statement of lemma4f as p.IProp infer p.A3 infer p.Prop end define,define unitac of lemma4f as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma4f as \ p . \ c . taceval1 ( quote p.IProp end quote , quote Line L01 : Premise >> p.A3 ; p.Prop Rule conclude p.Prop end quote , c ) end define end math ]"



"[ ensure math define statement of lemma4g as p.IProp infer p.A3 infer x p.imply x end define,define unitac of lemma4g as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma4g as \ p . \ c . taceval1 ( quote p.IProp end quote , quote Line L01 : Premise >> p.A3 ; lemma2 conclude x p.imply x end quote , c ) end define end math ]"



\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 "[[ Define tex of alpha as "
\alpha " end define ]]"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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



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



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



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



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



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



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

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

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

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

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

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

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

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

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

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

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

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



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

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

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

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

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

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

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

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

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



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



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



\item "[[ Define tex of 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 "[[ Define tex name of line x : y >> z ; u as "
L "[ x ]"
\colon "[ y ]"
\gg "[ z ]"
; "[ u ]"" end define ]]"

\item "[[ Define tex of 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 "[[ Define tex name of line x : y >> z ; as "
L "[ x ]"
\colon "[ y ]"
\gg "[ z ]"
;" end define ]]"

\item "[[ Define tex of 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 "[[ Define tex name of line x : y >> z qed as "
L "[ x ]"
\colon "[ y ]"
\gg "[ z ]"
\Box" end define ]]"

\item "[[ Define tex of 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 "[[ Define tex name of line x : Premise >> z ; u as "
L "[ x ]"
\colon Premise
\gg "[ z ]"
; "[ u ]"" end define ]]"

\item "[[ Define tex of 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 "[[ Define tex name of line x : Condition >> z ; u as "
L "[ x ]"
\colon Condition
\gg "[ z ]"
; "[ u ]"" end define ]]"

\item "[[ Define tex of 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 "[[ Define tex name of line x : Arbitrary >> z ; u as "
L "[ x ]"
\colon Arbitrary
\gg "[ z ]"
; "[ u ]"" end define ]]"

\item "[[ Define tex of 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 "[[ Define tex name of line x : Local >> y = z ; u as "
L "[ x ]"
\colon Local
\gg "[ y ]" \mathrel{\ddot{=}} "[ z ]"
; "[ u ]"" end define ]]"

\item "[[ Define tex of 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 "[[ Define tex name of 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 "[[ Define tex of prepare proof indentation as "
\ifx\indentation\undefined
\newlength{\indentation}\setlength{\indentation}{0em}
\fi" end define ]]"

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



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



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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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



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

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

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

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

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

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

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

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

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

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



\end{statements}



\section{Pyk definitions}

\begin{flushleft}
"[[ 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{flushleft}



\section{Priority table}

\begin {flushleft}
"[[ define priority of check as 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 define ]]"
\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