Logiweb(TM)

Logiweb expansion of Peano in pyk

Up Help

text "page.html" : "<head>
<title>
Peano arithmetic
</title>
</head>

<body>
<h2>
Peano arithmetic
</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 = {Peano arithmetic - 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=Peano arithmetic}
\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{Peano arithmetic}
\author{Klaus Grue}
\maketitle
\tableofcontents

"[ ragged right ]"
"[ prepare proof indentation ]"



\section{Preliminaries}

\subsection{Quantifiers}

The following macro definition allows to write e.g.\ "[[ f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . u ]]" instead of "[[ f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . u ]]".

\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 f.allfunc \ u unquote . v unquote end quote ) :: make-root ( t , quote \ u unquote . v unquote end quote ) :: u :: v :: true :: true else expand-all1 ( t , u first , expand-all1 ( t , u second , v ) ) end define ]]"

\end{statements}



\subsection{First and second argument of quantifier}

\begin{statements}

\item "[[ define value of x First as norm x is val : x first first end define ]]"

\item "[[ define value of x Second as norm x is val : x first second end define ]]"

\end{statements}



\subsection{Avoidance}

The side condition "[[ \ c . quote x end quote objectavoid ( c ) quote y end quote ]]" expresses that "[[ x ]]" does not occur free in "[[ y ]]". This side condition is useful to express Mendelsons axioms A5 \cite{Mendelson}. We shall also use it in connection with an inference of instantiation defined later.

\begin{statements}

\item "[[ define macro of x avoid y as \ x . expand ( quote macro define x avoid y as \ c . quote x end quote objectavoid ( c ) quote y end quote end define end quote , x ) end define ]]". This macro quotes its arguments and pass them on to objectavoid which performs the actual computation. During proof checking, "[[ c ]]" is instantiated to the cache of the page on which the proof occurs.

\end{statements}



\subsection{Instantiation}

The side condition "[[ \ c . sub0 ( quote a end quote , quote b end quote , quote x end quote , quote t end quote , c ) ]]" expresses that "[[ a ]]" is equal to the result of replacing "[[ x ]]" by "[[ t ]]" in "[[ b ]]". This side condition is useful for expressing the axiom of induction in which one has to replace the induction variable "[[ x ]]" by "[[ 0 ]]" and "[[ x suc ]]". The side condition requires "[[ x ]]" to be an object variable. The side condition is also useful for expressing axiom A4 (instantiation).

\begin{statements}

\item "[[ define macro of sub ( a , b , x , t ) as \ x . expand ( quote macro define sub ( a , b , x , t ) as \ c . sub0 ( quote a end quote , quote b end quote , quote x end quote , quote t end quote , c ) end define end quote , x ) end define ]]". This macro quotes its arguments and pass them on to sub0 which performs the actual computation. During proof checking, "[[ c ]]" is instantiated to the cache of the page on which the proof occurs.

\item "[[ define value of sub0 ( a , b , x , t , c ) as norm a is val : b is val : x is val : t is val : c is val : x objectvar ( c ) .and. sub1 ( a , b , x , t , c ) end define ]]". Check that "[[ x ]]" is an object variable and invoke sub1.

\item "[[ define value of sub1 ( a , b , x , t , c ) as norm a is val : b is val : x is val : t is val : c is val : if b r= quote f.allfunc \ u . v end quote .and. b First t= x then a t= b else if b t= x then a t= t else a r= b .and. sub* ( a tail , b tail , x , t , c ) end define ]]"

\item "[[ define value of sub* ( a , b , x , t , c ) as norm a is val : b is val : x is val : t is val : c is val : a atom .or. sub1 ( a head , b head , x , t , c ) .and. sub* ( a tail , b tail , x , t , c ) end define ]]"

\end{statements}



\subsection{Substitution}

The function "[[ f.subst ( x , s , c ) ]]" defined in the following performs the substitution "[[ s ]]" on "[[ x ]]" without renaming.

\begin{statements}

\item "[[ define value of f.subst ( x , s , c ) as norm x is val : s is val : c is val : LET lookup ( x , s , true ) BE asterisk IN LET asterisk BE d IN if .not. d then d else LET x valuedef ( c ) BE asterisk IN LET asterisk BE d IN if d = 1 then x else if d != 0 then x head :: f.subst* ( x tail , s , c ) else x head :: x first :: f.subst ( x second , remove ( x first , s ) , c ) :: <<>> end define ]]"

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

\end{statements}



\subsection{Parallel instantiation}

\begin{statements}

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

"[[ \ c . inst0 ( quote x end quote , quote y end quote , c ) ]]" is suited as a side condition. The side condition is true if "[[ y ]]" is an instantiation of "[[ x ]]". Multiple instantiation is legal and is done in parallel. Only universal quantifiers which occur in the root can be instantiated. Universal quantifiers which occur in the the root of "[[ x ]]" but which are not instantiated because they also appear in the root of "[[ y ]]" may instead be alpha-converted.



\item "[[ define value of inst0 ( x , y , c ) as norm x is val : y is val : c is val : .not. inst1 ( x , y , c ) catch head end define ]]"

Check that "[[ y ]]" is an instance of "[[ x ]]". Return true if it is and false otherwise.



\item "[[ define value of inst1 ( x , y , c ) as norm x is val : y is val : c is val : LET inst-strip ( x , true , 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 x IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE u IN LET inst-strip ( y , true , 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 y IN LET asterisk prime head BE asterisk IN LET asterisk prime tail BE asterisk prime IN LET asterisk BE v IN LET inst-zip ( u , v ) BE asterisk IN LET asterisk BE s IN inst2 ( x , y , s , true , c ) end define ]]"

Remove universal quantifiers from the root of "[[ x ]]" and "[[ y ]]". Accumulate the bound variables in reverse order in "[[ u ]]" and "[[ v ]]". Then zip "[[ u ]]" and "[[ v ]]" in a way which allows "[[ u ]]" to be longer than "[[ v ]]". In that way, variables which occur both in "[[ u ]]" and "[[ v ]]" are effectively alpha-renamed.



\item "[[ define value of inst-strip ( x , v , c ) as norm x is val : v is val : c is val : if .not. x metadef ( c ) then x :: v else if .not. x valuedef ( c ) then x :: v else if x mathdef ( c ) != "all" then x :: v else if x tail then exception else LET x first BE asterisk IN LET asterisk BE x IN if .not. x metadef ( c ) then exception else if x valuedef ( c ) != 0 then exception else inst-strip ( x second , x first :: v , c ) end define ]]"

Remove universal quantifiers from the root of "[[ x ]]". Accumulate the bound variables in "[[ v ]]".



\item "[[ define value of inst-zip ( x , y ) as norm x is val : y is val : if x then if y then true else exception else x head :: y head :: inst-zip ( x tail , y tail ) end define ]]"

Zip "[[ x ]]" and "[[ y ]]" where "[[ x ]]" is allowed to be longer than "[[ y ]]".



\item "[[ define value of inst2 ( x , y , s , b , c ) as norm x is val : y is val : s is val : b is val : c is val : LET lookup ( x , s , false ) BE asterisk IN LET asterisk BE d IN if d then x :: y :: s else if d pairp then if inst3 ( d , b , c ) then s else exception else if .not. x r= y then exception else if .not. x metadef ( c ) then exception else LET x valuedef ( c ) BE asterisk IN LET asterisk BE d IN if d = 1 then if x first = y first then s else exception else if d != 0 then inst2* ( x tail , y tail , s , b , c ) else LET x first BE asterisk IN LET asterisk BE v IN if .not. v = y first then exception else if .not. x objectvar ( c ) then exception else LET remove ( v , s ) BE asterisk IN LET asterisk BE s IN inst2 ( x second , y second , s , b set+ v , c ) end define ]]"

Check that "[[ y ]]" is the result of performing the substitution "[[ s ]]" on "[[ x ]]". The set "[[ b ]]" contains all locally bound variables. The function enriches "[[ s ]]" whenever it meets a variable for which it is not yet known how the variable is instantiated. The function returns the enriched "[[ s ]]" or signals an error.



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

Elementwise application of "[[ inst2 ( x , y , s , b , c ) ]]" to lists "[[ x ]]" and "[[ y ]]".



\item "[[ define value of inst3 ( x , b , c ) as norm x is val : b is val : c is val : if .not. x metadef ( c ) then false else if .not. x mathdef ( c ) then inst3* ( x tail , b , c ) else LET x valuedef ( c ) BE asterisk IN LET asterisk BE d IN if d then .not. x member b else if d = 1 then true else if d != 0 then inst3* ( x tail , b , c ) else inst3 ( x second , b set- x first , c ) end define ]]"

Check that "[[ x ]]" is suited for insertion, i.e. that the free variable of "[[ x ]]" do not occur in "[[ b ]]".



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

Elementwise application of "[[ inst3 ( x , b , c ) ]]" to the list "[[ x ]]".

\end{statements}



\subsection{Definition}

The side condition "[[ \ c . def0 ( quote a end quote , quote b end quote , c ) ]]" allows to formulate a rule of definition which allows to replace definiens by definiendum and vice versa.

\begin{statements}

\item "[[ define macro of def ( a , b ) as \ x . expand ( quote macro define def ( a , b ) as \ c . def0 ( quote a end quote , quote b end quote , c ) end define end quote , x ) end define ]]".

This macro quotes its arguments and pass them on to def0 which performs the actual computation. During proof checking, "[[ c ]]" is instantiated to the cache of the page on which the proof occurs.

\item "[[ define value of def0 ( a , b , c ) as norm a is val : b is val : c is val : def1 ( a , b , c ) .or. def2 ( a , b , c ) .or. def2 ( b , a , c ) end define ]]".

Test that "[[ a ]]" and "[[ b ]]" are equal modulo application of definitions.

\item "[[ define value of def0* ( a , b , c ) as norm a is val : b is val : c is val : a atom .or. def0 ( a head , b head , c ) .and. def0* ( a tail , b tail , c ) end define ]]"

Coordinatewise application of def0 to the lists "[[ a ]]" and "[[ b ]]".

\item "[[ define value of def1 ( a , b , c ) as norm a is val : b is val : c is val : LET a metadef ( c ) BE asterisk IN LET asterisk BE v IN if v = "var" then a t= b else if .not. v then false else LET a valuedef ( c ) BE asterisk IN LET asterisk BE v IN if v = 0 then a first t= b first .and. def0 ( a second , b second , c ) else if v = 1 then a first = b first else a r= b .and. def0* ( a tail , b tail , c ) end define ]]".

def1 is true if "[[ a ]]" and "[[ b ]]" are equal modulo definitions applied to subterms of "[[ a ]]" and "[[ b ]]".

\item "[[ define value of def2 ( a , b , c ) as norm a is val : b is val : c is val : a metadef ( c ) = true .and. a valuedef ( c ) = true .and. LET a def ( c , math ) BE asterisk IN LET asterisk BE v IN if v .or. v third ref = 0 .or. .not. checked-def ( a ref , c ) then false else LET zip ( v second tail , a tail ) BE asterisk IN LET asterisk BE s IN def3 ( v third , b , s , c ) end define ]]"

Test that "[[ b ]]" is equal to "[[ a ]]" according to the definition of "[[ a ]]".

\item "[[ define value of def3 ( a , b , s , c ) as norm a is val : b is val : s is val : c is val : if .not. a metadef ( c ) then false else LET a valuedef ( c ) BE asterisk IN LET asterisk BE v IN if v = 0 then b valuedef ( c ) = 0 .and. def3 ( a second , b second , a first :: b first :: s , c ) else if v = 1 then false else LET a mathdef ( c ) BE asterisk IN LET asterisk BE w IN if v .and. w .or. w ref = 0 then b t= lookup ( a , s , true ) else a r= b .and. def3* ( a tail , b tail , s , c ) end define ]]".

True if the right hand side "[[ a ]]" is identical to "[[ b ]]" after instantiating a as specified by the association list "[[ s ]]".

\item "[[ define value of def3* ( a , b , s , c ) as norm a is val : b is val : s is val : c is val : a atom .or. def3 ( a head , b head , s , c ) .and. def3* ( a tail , b tail , s , c ) end define ]]"

Coordinatewise application of def3 to the lists "[[ a ]]" and "[[ b ]]".

\end{statements}



\subsection{Soundness of definitions}

\begin{statements}

\item "[[ define claim of Peano as test1 &c defcheck &c proofcheck end define ]]"

When using the present page as bed page, all tests are executed ("[[ test1 ]]"), all proofs are checked ("[[ proofcheck ]]"), and the soundness of all definitions are checked ("[[ defcheck ]]").

\item "[[ define value of defcheck as \ c . defcheck1 ( c ) end define ]]"

The "[[ defcheck ]]" conjunct passes the cache "[[ c ]]" on to "[[ defcheck1 ( c ) ]]".

\item "[[ define value of checked-def ( 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 claiming ( quote defcheck end quote , x ) end define ]]"

True if the soundness of definitions on the page with reference "[[ r ]]" has been checked.

\item "[[ define value of defcheck1 ( c ) as norm c is val : LET c [[ 0 ]] BE asterisk IN LET asterisk BE r IN LET c [[ r ]] [[ "codex" ]] [[ r ]] BE asterisk IN LET asterisk BE a IN LET defcheck2 ( a , 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 definition soundness checker: unprocessed exception" end quote end name end define ]]"

Look up the array "[[ a ]]" of all local definitions on the page being checked. Pass it to "[[ defcheck2 ( a , c ) ]]"

\item "[[ define value of defcheck2 ( a , c ) as norm a is val : c is val : if a = true then true else if .not. a head intp then defcheck2 ( a head , c ) .and. defcheck2 ( a tail , c ) else LET a tail [[ 0 ]] [[ math ]] BE asterisk IN LET asterisk BE v IN if v .or. v third ref = 0 then true else if valid-def ( v third , v second tail , v second :: <<>> , c ) then true else error ( v second , diag ( "Definition soundness check of" ) form ( v second ) diag ( "failed." ) diag ( "Error could be in any, transitively used definition" ) diag ( "or could be that the definition is circular." ) end diagnose ) end define ]]"

Find all definitions "[[ v ]]". If "[[ v ]]" is "[[ true ]]" then the corresponding construct is undefined which is ok. If "[[ v third ref = 0 ]]" then the right hand side is a string indicating that this is a predefined construct of some sort which is ok. Otherwise, call valid-def. Calling valid-def for each definition is not optimal since non-circularity is checked every time.

\item "[[ define value of valid-def ( a , b , s , c ) as norm a is val : b is val : s is val : c is val : if .not. a metadef ( c ) then false else LET a valuedef ( c ) BE asterisk IN LET asterisk BE v IN if v = 0 then valid-def ( a second , a first :: b , s , c ) else if v = 1 then false else if .not. v then valid-def* ( a tail , b , s , c ) else LET a def ( c , math ) BE asterisk IN LET asterisk BE v IN if v then a member b else if .not. valid-def* ( a tail , b , s , c ) then false else if v third ref = 0 then true else if v second ref != c [[ 0 ]] then claiming ( v second ref , c ) else if v second member s then false else valid-def ( v third , v second tail , v second :: s , c ) end define ]]".

"[[ valid-def ( a , b , s , c ) ]]" tests that "[[ a ]]" is a valid right hand side of a definition. "[[ b ]]" is the list of bound variables (parameters plus variables bound by lambdas). "[[ s ]]" is a stack of left hand sides used for spotting circular definitions. "[[ c ]]" is the cache.

\item "[[ define value of valid-def* ( a , b , s , c ) as norm a is val : b is val : s is val : c is val : a atom .or. valid-def ( a head , b , s , c ) .and. valid-def* ( a tail , b , s , c ) end define ]]".

Conjunction of valid-def applied to all elements of the list "[[ a ]]".



\end{statements}



\subsection{Connectives and function letters}

The sidecondition above and the inference rule of definition stated later allows to define new concepts from previously defined concepts. Definitions whose right hand side is a string introduce a new construct.

In Propositional calculus we take implication "[[ x imply y ]]" and falsehood "[[ ff ]]" as elementary and then define a number of logical connectives on basis of that:

\begin{statements}

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

\item "[[ define math of ff as "ff" end define ]]".

\item "[[ define math of not x as x imply ff end define ]]"

\item "[[ define math of tt as ff imply ff end define ]]"

\item "[[ define math of x or y as not x imply y end define ]]"

\item "[[ define math of x and y as not x imply not y end define ]]"

\item "[[ define math of x when y as y imply x end define ]]"

\item "[[ define math of x iff y as x imply y and y imply x end define ]]"

\end{statements}

In first order logic we take the universal quantifier as elementary. We have defined "[[ f.allfunc \ x . y ]]" to macro expand to "[[ f.allfunc \ x . y ]]" so it is the unary "[[ f.allfunc x ]]" construct which represents the universal quantifier.

\begin{statements}

\item "[[ define math of f.allfunc x as "all" end define ]]".

\end{statements}

In Peano arithmetic we use the function letters "[[ 0 ]]", "[[ x + y ]]", "[[ x * y ]]", and "[[ x suc ]]" and the relation sign "[[ x = y ]]". All of these except the successor function "[[ x suc ]]" are value defined on the \href{\lgwrelay 64/\lgwBaseBlockBaseSixtyFour /2/body/tex/chores.pdf}{base} page. We also give a value definition of the successor function:

\begin{statements}

\item "[[ define value of x suc as norm x is val : x + 1 end define ]]"

\end{statements}



\section{Theories}

\subsection{Propositional calculus}

The following rules define the propositional calculus "[[ Prop ]]". The axioms "[[ A1 ]]", "[[ A2 ]]", and "[[ A3 ]]" and the inference rule "[[ MP ]]" are taken from Mendelson \cite{Mendelson}.

The "[[ Def ]]" rule is the inference of definition. Due to the inference of definition, we may use e.g.\ "[[ x and y ]]", "[[ x or y ]]", and "[[ x iff y ]]" even though those connectives are not mentioned in the axioms.

Even "[[ not x ]]" is defined: "[[ not x ]]" is defined to mean "[[ x imply ff ]]" where "[[ ff ]]" is falsehood.

Apart from "[[ Def ]]" and the definition of "[[ not x ]]", "[[ Prop ]]" below is defined as in \cite{Mendelson}.

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

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

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

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

"[ ensure math define statement of Def as All #x : All #y : \ c . def0 ( quote #x end quote , quote #y end quote , c ) endorse #x infer #y end define,define unitac of Def as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of Prop as A1 oplus A2 oplus A3 oplus MP oplus Def end define end math ]"



\subsection{First order logic}

First order logic "[[ FOL ]]" is "[[ Prop ]]" extended with "[[ A4 ]]", "[[ AP4 ]]", "[[ A5 ]]", and "[[ Gen ]]". "[[ Gen ]]" is generalization, "[[ A4 ]]" is the opposite, and "[[ A5 ]]" is needed for the theorem of deduction.

"[[ AP4 ]]" is a parallel version of "[[ A4 ]]" which allows to instantiate several quantifiers at the same time. As an example, "[[ f.allfunc \ x . f.allfunc \ y . x + y = y + x imply y + x = x + y ]]" is correct according to "[[ AP4 ]]" because "[[ y + x = x + y ]]" arises from "[[ x + y = y + x ]]" by simultaneous replacement of "[[ x ]]" with "[[ y ]]" and "[[ y ]]" with "[[ x ]]". The verification time of the present paper has been reduce by a factor of five by having parallel object instantiation ("[[ AP4 ]]") and by having parallel meta instantiation (parallel "[[ x at y ]]"). Both "[[ A4 ]]" and "[[ AP4 ]]" has been included in "[[ FOL ]]" even though any one of them is sufficient.

Apart from "[[ AP4 ]]" and the definition of "[[ not x ]]", "[[ FOL ]]" below is defined as in \cite{Mendelson}.

"[ ensure math define statement of A4 as All #t : All #x : All #a : All #b : \ c . sub0 ( quote #b end quote , quote #a end quote , quote #x end quote , quote #t end quote , c ) endorse f.allfunc \ #x . #a imply #b end define,define unitac of A4 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of AP4 as All #a : All #b : \ c . inst0 ( quote #a end quote , quote #b end quote , c ) endorse #a imply #b end define,define unitac of AP4 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of A5 as All #x : All #a : All #b : \ c . quote #x end quote objectavoid ( c ) quote #a end quote endorse f.allfunc \ #x . #a imply #b imply #a imply f.allfunc \ #x . #b end define,define unitac of A5 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of Gen as All #u : All #x : #x infer f.allfunc \ #u . #x end define,define unitac of Gen as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of FOL as Prop oplus A4 oplus AP4 oplus A5 oplus Gen end define end math ]"



\subsection{Peano Arithmetic}

Peano arithmetic "[[ PA ]]" is "[[ FOL ]]" extended with "[[ S1 ]]" to "[[ S9 ]]" taken from \cite{Mendelson}.

"[ ensure math define statement of S1 as f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . x = y imply x = z imply y = z end define,define unitac of S1 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of S2 as f.allfunc \ x . f.allfunc \ y . x = y imply x suc = y suc end define,define unitac of S2 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of S3 as f.allfunc \ x . not 0 = x suc end define,define unitac of S3 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of S4 as f.allfunc \ x . x suc = y suc imply x = y end define,define unitac of S4 as \ u . unitac-rule ( u ) end define end math ]"

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

"[ ensure math define statement of S6 as f.allfunc \ x . f.allfunc \ y . x + y suc = x + y suc end define,define unitac of S6 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of S7 as f.allfunc \ x . x * 0 = 0 end define,define unitac of S7 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of S8 as f.allfunc \ x . f.allfunc \ y . x * y suc = x * y + x end define,define unitac of S8 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of S9 as All #x : All #a : All #z : All #i : \ c . sub0 ( quote #z end quote , quote #a end quote , quote #x end quote , quote 0 end quote , c ) endorse \ c . sub0 ( quote #i end quote , quote #a end quote , quote #x end quote , quote #x suc end quote , c ) endorse #z imply f.allfunc \ #x . #a imply #i imply #a end define,define unitac of S9 as \ u . unitac-rule ( u ) end define end math ]"

"[ ensure math define statement of PA as FOL oplus S1 oplus S2 oplus S3 oplus S4 oplus S5 oplus S6 oplus S7 oplus S8 oplus S9 end define end math ]"



\section{Deduction}

\subsection{Auxiliary lemmas}

We now prove a number of auxiliary lemmas which are needed by the deduction tactic. Later, we define that "[[ Prop ]]", "[[ FOL ]]", and "[[ PA ]]" proofs are tactic expanded by the deduction tactic. We cannot prove the lemmas below using the deduction tactic since the deduction tactic does not work before the lemmas below are proved. For that reason, we disable the deduction tactic in the proofs below by assuming "[[ Prop ]]" and "[[ FOL ]]" as premises rather than stating them in the header of the proof.

Lemma "[[ Mend1.8 ]]" below is Lemma 1.8 in Mendelson: Introduction to Mathematical Logic \cite{Mendelson}. In general, the numbering used in \cite{Mendelson} has been kept. Some of the proofs also come from \cite{Mendelson}. The present text deviates slightly from \cite{Mendelson} in that the present text takes implication "[[ x imply y ]]" and falsehood "[[ ff ]]" as primitive whereas \cite{Mendelson} takes implication "[[ x imply y ]]" and negation "[[ not x ]]" as primitive. All proofs in \cite{Mendelson} carry over to the present framework without change since the axioms and inference rules are taken from \cite{Mendelson}. But the present text can take advantage of an additional feature, namely that "[[ not x ]]" is defined to denote "[[ x imply ff ]]".



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

"[ ensure math define proof of Mend1.8 as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #x : Line L03 : A2 >> #x imply #y imply #x imply #x imply #x imply #y imply #x imply #x imply #x ; Line L04 : A1 >> #x imply #y imply #x imply #x ; Line L05 : MP ponens L03 ponens L04 >> #x imply #y imply #x imply #x imply #x ; Line L06 : A1 >> #x imply #y imply #x ; MP ponens L05 ponens L06 conclude #x imply #x end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of A1' as Prop infer All #h : All #a : #a infer #h imply #a end define,define unitac of A1' as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of A1' as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #a : Line L03 : Premise >> #a ; MP ponens A1 ponens L03 conclude #h imply #a end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of A2' as Prop infer All #h : All #a : All #b : #h imply #a imply #b infer #h imply #a infer #h imply #b end define,define unitac of A2' as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of A2' as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #a : All #b : Line L03 : Premise >> #h imply #a imply #b ; Line L04 : Premise >> #h imply #a ; MP ponens MP ponens A2 ponens L03 ponens L04 conclude #h imply #b end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of Mend1.47b as Prop infer All #a : All #b : All #c : #a imply #b infer #b imply #c infer #a imply #c end define,define unitac of Mend1.47b as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of Mend1.47b as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #a : All #b : All #c : Line L03 : Premise >> #a imply #b ; Line L04 : Premise >> #b imply #c ; Line L05 : A1' ponens L04 >> #a imply #b imply #c ; A2' ponens L05 ponens L03 conclude #a imply #c end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of Mend1.47c as Prop infer All #a : All #b : All #c : #a imply #b imply #c infer #b imply #a imply #c end define,define unitac of Mend1.47c as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of Mend1.47c as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #a : All #b : All #c : Line L03 : Premise >> #a imply #b imply #c ; Line L04 : MP ponens A2 ponens L03 >> #a imply #b imply #a imply #c ; Line L05 : A1' ponens L04 >> #b imply #a imply #b imply #a imply #c ; Line L06 : MP ponens A2 ponens L05 >> #b imply #a imply #b imply #b imply #a imply #c ; MP ponens L06 ponens A1 Conclude conclude #b imply #a imply #c end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of Mend1.47d as Prop infer All #a : All #b : not #a imply not #b imply #b imply #a end define,define unitac of Mend1.47d as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of Mend1.47d as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #a : All #b : Line L03 : A3 >> not #a imply not #b imply not #a imply #b imply #a ; Line L04 : Mend1.47c ponens L03 >> not #a imply #b imply not #a imply not #b imply #a ; Line L05 : A1 >> #b imply not #a imply #b ; Line L06 : Mend1.47b ponens L05 ponens L04 >> #b imply not #a imply not #b imply #a ; Mend1.47c ponens L06 conclude not #a imply not #b imply #b imply #a end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of Mend1.11b as Prop infer All #a : #a imply not not #a end define,define unitac of Mend1.11b as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of Mend1.11b as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #a : Line L03 : Mend1.8 >> #a imply ff imply #a imply ff ; Line L04 : Mend1.47c ponens L03 >> #a imply #a imply ff imply ff ; Line L05 : Def ponens L04 >> #a imply not #a imply ff ; Def ponens L05 conclude #a imply not not #a end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of Mend1.48d as Prop infer All #h : All #x : #h and #x imply #h end define,define unitac of Mend1.48d as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of Mend1.48d as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #x : Line L03 : Mend1.8 >> ff imply ff ; Line L04 : Def ponens L03 >> not ff ; Line L05 : A1' ponens L04 >> not not #x imply not ff ; Line L06 : MP ponens Mend1.47d ponens L05 >> ff imply not #x ; Line L07 : A1' ponens L06 >> #h imply ff imply not #x ; Line L08 : MP ponens A2 ponens L07 >> #h imply ff imply #h imply not #x ; Line L09 : Def ponens L08 >> not #h imply #h imply not #x ; Line L10 : Mend1.11b >> #h imply not #x imply not not #h imply not #x ; Line L11 : Mend1.47b ponens L09 ponens L10 >> not #h imply not not #h imply not #x ; Line L12 : MP ponens Mend1.47d ponens L11 >> not #h imply not #x imply #h ; Def ponens L12 conclude #h and #x imply #h end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of Mend1.48e as Prop infer All #h : All #x : #h and #x imply #x end define,define unitac of Mend1.48e as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of Mend1.48e as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #x : Line L03 : A1 >> not #x imply #h imply not #x ; Line L04 : Mend1.11b >> #h imply not #x imply not not #h imply not #x ; Line L05 : Mend1.47b ponens L03 ponens L04 >> not #x imply not not #h imply not #x ; Line L06 : MP ponens Mend1.47d ponens L05 >> not #h imply not #x imply #x ; Def ponens L06 conclude #h and #x imply #x end quote , tacstate0 , c ) end define end math ]"



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

"[ ensure math define proof of Lnexthyp as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #x : All #y : Line L03 : Premise >> #h imply #y ; Line L04 : Mend1.48d >> #h and #x imply #h ; Mend1.47b ponens L04 ponens L03 conclude #h and #x imply #y end quote , tacstate0 , c ) end define end math ]"



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

"[ ensure math define proof of Lcurry as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #x : All #y : Line L03 : Premise >> #h and #x imply #y ; Line L04 : Def ponens L03 >> not #h imply not #x imply #y ; Line L05 : Mend1.11b >> #y imply not not #y ; Line L06 : Mend1.47b ponens L04 ponens L05 >> not #h imply not #x imply not not #y ; Line L07 : MP ponens Mend1.47d ponens L06 >> not #y imply #h imply not #x ; Line L08 : Mend1.47c ponens L07 >> #h imply not #y imply not #x ; Line L09 : Mend1.47d >> not #y imply not #x imply #x imply #y ; Mend1.47b ponens L08 ponens L09 conclude #h imply #x imply #y end quote , tacstate0 , c ) end define end math ]"



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

"[ ensure math define proof of LTruth as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; Line L02 : Mend1.8 >> ff imply ff ; Def ponens L02 conclude tt end quote , tacstate0 , c ) end define end math ]"



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

"[ ensure math define proof of LElimHyp as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #x : Line L03 : Premise >> tt imply #x ; Line L04 : LTruth >> tt ; MP ponens L03 ponens L04 conclude #x end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of LA4' as FOL infer All #h : All #t : All #x : All #a : All #b : \ c . sub0 ( quote #b end quote , quote #a end quote , quote #x end quote , quote #t end quote , c ) endorse #h imply f.allfunc \ #x . #a infer #h imply #b end define,define unitac of LA4' as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of LA4' as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; All #h : All #t : All #x : All #a : All #b : Line L03 : Condition >> \ c . sub0 ( quote #b end quote , quote #a end quote , quote #x end quote , quote #t end quote , c ) ; Line L04 : Premise >> #h imply f.allfunc \ #x . #a ; Line L05 : A4 probans L03 >> f.allfunc \ #x . #a imply #b ; Mend1.47b ponens L04 ponens L05 conclude #h imply #b end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of LAP4' as FOL infer All #h : All #a : All #b : \ c . inst0 ( quote #a end quote , quote #b end quote , c ) endorse #h imply #a infer #h imply #b end define,define unitac of LAP4' as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of LAP4' as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; All #h : All #a : All #b : Line L03 : Condition >> \ c . inst0 ( quote #a end quote , quote #b end quote , c ) ; Line L04 : Premise >> #h imply #a ; Line L05 : AP4 probans L03 >> #a imply #b ; Mend1.47b ponens L04 ponens L05 conclude #h imply #b end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of MP' as Prop infer All #h : All #a : All #b : #h imply #a imply #b infer #h imply #a infer #h imply #b end define,define unitac of MP' as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of MP' as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #a : All #b : Line L03 : Premise >> #h imply #a imply #b ; Line L04 : Premise >> #h imply #a ; Line L05 : A2 >> #h imply #a imply #b imply #h imply #a imply #h imply #b ; Line L06 : MP ponens L05 ponens L03 >> #h imply #a imply #h imply #b ; MP ponens L06 ponens L04 conclude #h imply #b end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of Gen1 as FOL infer All #h : All #x : All #a : \ c . quote #x end quote objectavoid ( c ) quote #h end quote endorse #h imply #a infer #h imply f.allfunc \ #x . #a end define,define unitac of Gen1 as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of Gen1 as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; All #h : All #x : All #a : Line L03 : Condition >> \ c . quote #x end quote objectavoid ( c ) quote #h end quote ; Line L04 : Premise >> #h imply #a ; Line L05 : Gen ponens L04 >> f.allfunc \ #x . #h imply #a ; Line L06 : A5 probans L03 >> f.allfunc \ #x . #h imply #a imply #h imply f.allfunc \ #x . #a ; MP ponens L06 ponens L05 conclude #h imply f.allfunc \ #x . #a end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of Gen2 as FOL infer All #h : All #x : All #y : All #a : \ c . quote #x end quote objectavoid ( c ) quote #h end quote endorse \ c . quote #y end quote objectavoid ( c ) quote #h end quote endorse #h imply #a infer #h imply f.allfunc \ #x . f.allfunc \ #y . #a end define,define unitac of Gen2 as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of Gen2 as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; All #h : All #x : All #y : All #a : Line L03 : Condition >> \ c . quote #x end quote objectavoid ( c ) quote #h end quote ; Line L04 : Condition >> \ c . quote #y end quote objectavoid ( c ) quote #h end quote ; Line L05 : Premise >> #h imply #a ; Line L06 : Gen1 probans L04 ponens L05 >> #h imply f.allfunc \ #y . #a ; Gen1 probans L03 ponens L06 conclude #h imply f.allfunc \ #x . f.allfunc \ #y . #a end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of Gen3 as FOL infer All #h : All #x : All #y : All #z : All #a : \ c . quote #x end quote objectavoid ( c ) quote #h end quote endorse \ c . quote #y end quote objectavoid ( c ) quote #h end quote endorse \ c . quote #z end quote objectavoid ( c ) quote #h end quote endorse #h imply #a infer #h imply f.allfunc \ #x . f.allfunc \ #y . f.allfunc \ #z . #a end define,define unitac of Gen3 as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of Gen3 as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; All #h : All #x : All #y : All #z : All #a : Line L03 : Condition >> \ c . quote #x end quote objectavoid ( c ) quote #h end quote ; Line L04 : Condition >> \ c . quote #y end quote objectavoid ( c ) quote #h end quote ; Line L05 : Condition >> \ c . quote #z end quote objectavoid ( c ) quote #h end quote ; Line L06 : Premise >> #h imply #a ; Line L07 : Gen2 probans L04 probans L05 ponens L06 >> #h imply f.allfunc \ #y . f.allfunc \ #z . #a ; Gen1 probans L03 ponens L07 conclude #h imply f.allfunc \ #x . f.allfunc \ #y . f.allfunc \ #z . #a end quote , tacstate0 , c ) end define end math ]"



"[ ensure math define statement of Induction as PA infer All #x : All #h : All #a : All #z : All #i : \ c . sub0 ( quote #z end quote , quote #a end quote , quote #x end quote , quote 0 end quote , c ) endorse \ c . sub0 ( quote #i end quote , quote #a end quote , quote #x end quote , quote #x suc end quote , c ) endorse \ c . quote #x end quote objectavoid ( c ) quote #h end quote endorse #h imply #z infer #h imply #a imply #i infer #h imply #a end define,define unitac of Induction as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of Induction as \ p . \ c . taceval ( quote Line L01 : Premise >> PA ; All #x : All #h : All #a : All #z : All #i : Line L03 : Condition >> \ c . sub0 ( quote #z end quote , quote #a end quote , quote #x end quote , quote 0 end quote , c ) ; Line L04 : Condition >> \ c . sub0 ( quote #i end quote , quote #a end quote , quote #x end quote , quote #x suc end quote , c ) ; Line L05 : Condition >> \ c . quote #x end quote objectavoid ( c ) quote #h end quote ; Line L06 : Premise >> #h imply #z ; Line L07 : Premise >> #h imply #a imply #i ; Line L08 : Gen1 probans L05 ponens L07 >> #h imply f.allfunc \ #x . #a imply #i ; Line L09 : S9 probans L03 probans L04 >> #z imply f.allfunc \ #x . #a imply #i imply #a ; Line L10 : A1' ponens L09 >> #h imply #z imply f.allfunc \ #x . #a imply #i imply #a ; Line L11 : A2' ponens L10 ponens L06 >> #h imply f.allfunc \ #x . #a imply #i imply #a ; A2' ponens L11 ponens L08 conclude #h imply #a end quote , tacstate0 , c ) end define end math ]"



\subsection{Hooks for the tactic state}

\begin{statements}

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

Hypothesis hook. Contains the ``working hypothesis'' which is the conjunction of all assumed hypotheses (or "[[ true ]]" if no hypotheses are assumed).

\end{statements}



\subsection{Tactic state for hypothetical reasoning}

During hypothetical reasoning, "[[ unitac-hyp ]]" is installed at the "[[ hook-unitac ]]" hook of the tactic state. The effect is that occurrences of "[[ x conclude y ]]" are changed to "[[ x conclude hyp imply y ]]" where "[[ hyp ]]" is the current hypothesis. References to lemmas and rules are modified likewise. Modification only affects proof lines, lemmas, and rules which conclude on object term. Proof lines, lemmas, and rules which conclude a meta term are unaffected.

\begin{statements}

\item "[[ define value of is-meta-term ( t , c ) as norm t is val : c is val : LET t metadef ( c ) BE asterisk IN LET asterisk BE d IN if d != true .and. d != "var" then true else .not. t stmt-rhs ( c ) end define ]]"

True if "[[ t ]]" is a meta-term (i.e.\ no object term) or if "[[ t ]]" is statement defined to denote some other term.

\item "[[ define value of unitac-hyp as norm true [[ hook-lemma -> quote \ u . unitac-lemma-hyp ( u ) end quote ]] [[ hook-rule -> quote \ u . unitac-rule-hyp ( u ) end quote ]] [[ hook-conclude -> quote \ u . unitac-conclude-hyp ( u ) end quote ]] end define ]]"

Structure containing modified lemma, rule, and conclude tactics.

\item "[[ define value of unitac-lemma-hyp ( 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 if is-meta-term ( r , c ) then unitac-lemma-std ( x ) else LET s [[ hook-hyp ]] BE asterisk IN LET asterisk BE h 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 LET make-root ( a , quote a unquote ;; A1' Init Deref Ponens at h unquote at r unquote Ponens end quote ) :: a :: make-root ( a , quote A1' Init Deref Ponens at h unquote at r unquote Ponens end quote ) :: make-root ( a , quote A1' Init Deref Ponens at h unquote at r unquote end quote ) :: make-root ( a , quote A1' Init Deref Ponens at h unquote end quote ) :: make-root ( a , quote A1' Init Deref Ponens end quote ) :: make-root ( a , quote A1' Init Deref end quote ) :: make-root ( a , quote A1' Init end quote ) :: make-root ( a , quote A1' end quote ) :: true :: true :: true :: true :: h :: true :: r :: true :: true :: true BE asterisk IN LET asterisk BE a IN LET make-root ( r , quote h unquote imply r unquote end quote ) :: h :: r :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]".

Modified lemma tactic. Calls unmodified tactic for meta terms.



\item "[[ define value of unitac-rule-hyp ( 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 if is-meta-term ( r , c ) then unitac-rule-std ( x ) else LET s [[ hook-hyp ]] BE asterisk IN LET asterisk BE h 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 LET make-root ( a , quote a unquote ;; A1' Init Deref Ponens at h unquote at r unquote Ponens end quote ) :: a :: make-root ( a , quote A1' Init Deref Ponens at h unquote at r unquote Ponens end quote ) :: make-root ( a , quote A1' Init Deref Ponens at h unquote at r unquote end quote ) :: make-root ( a , quote A1' Init Deref Ponens at h unquote end quote ) :: make-root ( a , quote A1' Init Deref Ponens end quote ) :: make-root ( a , quote A1' Init Deref end quote ) :: make-root ( a , quote A1' Init end quote ) :: make-root ( a , quote A1' end quote ) :: true :: true :: true :: true :: h :: true :: r :: true :: true :: true BE asterisk IN LET asterisk BE a IN LET make-root ( r , quote h unquote imply r unquote end quote ) :: h :: r :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

Modified rule tactic. Calls unmodified tactic for meta terms.



\item "[[ define value of unitac-conclude-hyp ( 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 q 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 is-meta-term ( r , c ) then unitac-conclude-std ( x ) else LET s [[ hook-hyp ]] BE asterisk IN LET asterisk BE h IN LET unieval ( q , s , c ) BE asterisk IN LET asterisk BE s IN LET f.unitac-adapt ( r mathdef ( c ) , s , c ) BE asterisk IN LET asterisk BE s IN LET make-root ( r , quote h unquote imply r unquote end quote ) :: h :: r :: true BE asterisk IN LET asterisk BE r IN LET unify ( s [[ hook-res ]] , r , s [[ hook-uni ]] ) BE asterisk IN LET asterisk BE u IN s [[ hook-uni -> u ]] [[ hook-res -> r ]] end define ]]"

Modified conclude tactic. Calls unmodified tactic for meta terms.

\end{statements}



\subsection{Stating hypotheses}

The following constructs allow to add a hypothesis to the working hypothesis of a proof.

\begin{statements}

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

The definition above ensures that errors in hypothesis lines are properly located (somewhat academic since hypothesis lines cannot be in error).

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

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

The tactic definition above adds "[[ x ]]" to the working hypothesis and tactic evaluates "[[ n ]]".

\item "[[ define value of tactic-hyp ( 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-hyp ]] BE asterisk IN LET asterisk BE h IN if h then tactic-first-hyp ( t , s , c ) else tactic-next-hyp ( h , t , s , c ) end define ]]"

When more hypotheses are assumed, the first hypothesis is treated differently from the next ones.

\end{statements}



\subsection{Stating a dummy hypothesis}

The following constructs allow to state "[[ tt ]]" as a hypothesis and removes "[[ tt ]]" again afterwards. The construct has no effect when the hypothesis is non-empty. The constructs below are useful in connection with constructs like "[[ x mp y ]]", "[[ x Mp ]]", "[[ x f.at y ]]", and "[[ x f.At ]]" which require the hypothesis to be non-empty.

\begin{statements}

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

\item "[[ define locate of tactic-ded ( l , n ) as "line" :: 2 end define ]]"

The definition above ensures that errors in dummy hypothesis lines are properly located (somewhat academic since hypothesis lines cannot be in error).

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

\item "[[ define tactic of Line l : Deduction ; n as \ u . tactic-dummyhyp ( u ) end define ]]"

\item "[[ define tactic of tactic-ded ( l , n ) as \ u . tactic-dummyhyp ( u ) end define ]]"

The tactic definition above adds "[[ tt ]]" to the working hypothesis, tactic evaluates "[[ n ]]", and removes "[[ tt ]]" again.

\item "[[ define value of tactic-dummyhyp ( 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 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 n 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-hyp ]] BE asterisk IN LET asterisk BE h IN if .not. h then taceval ( n , s , c ) else LET tactic-first-hyp ( true :: true :: quote tt end quote :: n :: <<>> , s , c ) BE asterisk IN LET asterisk BE s IN LET s [[ hook-res ]] second BE asterisk IN LET asterisk BE r IN LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN LET make-root ( a , quote a unquote ;; LElimHyp Init Deref Ponens at r unquote Ponens end quote ) :: a :: make-root ( a , quote LElimHyp Init Deref Ponens at r unquote Ponens end quote ) :: make-root ( a , quote LElimHyp Init Deref Ponens at r unquote end quote ) :: make-root ( a , quote LElimHyp Init Deref Ponens end quote ) :: make-root ( a , quote LElimHyp Init Deref end quote ) :: make-root ( a , quote LElimHyp Init end quote ) :: make-root ( a , quote LElimHyp end quote ) :: true :: true :: true :: true :: r :: true :: true :: true BE asterisk IN LET asterisk BE a IN s [[ hook-arg -> a ]] [[ hook-res -> r second ]] end define ]]"

\end{statements}



\subsection{Handling the first hypthesis}

\begin{statements}

\item "[[ define value of tactic-first-hyp ( t , s , c ) as norm t is val : s is val : c is val : LET quote x conclude y end quote 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 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 i 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 head BE asterisk IN LET asterisk prime tail BE asterisk 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 s [[ hook-hyp -> x ]] BE asterisk IN LET asterisk BE s IN LET s [[ hook-unitac -> unitac-hyp ]] BE asterisk IN LET asterisk BE s IN LET s [[ hook-pre -> add-first-hyp* ( x , s [[ hook-pre ]] , c ) ]] BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote x unquote imply x unquote end quote ) :: x :: x :: true BE asterisk IN LET asterisk BE x prime IN LET tactic-push ( hook-pre , l :: x prime :: make-root ( x prime , quote x prime unquote Init end quote ) :: x prime :: true :: <<>> , s ) BE asterisk IN LET asterisk BE s IN LET taceval ( n , s , c ) BE asterisk IN LET asterisk BE s IN s [[ hook-arg -> make-root ( t , quote Mend1.8 Init Deref Ponens at x unquote ;; s [[ hook-arg ]] unquote end quote ) :: make-root ( t , quote Mend1.8 Init Deref Ponens at x unquote end quote ) :: make-root ( t , quote Mend1.8 Init Deref Ponens end quote ) :: make-root ( t , quote Mend1.8 Init Deref end quote ) :: make-root ( t , quote Mend1.8 Init end quote ) :: make-root ( t , quote Mend1.8 end quote ) :: true :: true :: true :: true :: x :: true :: s [[ hook-arg ]] :: true ]] end define ]]"

The definition above first ensures that "[[ x conclude y ]]" adds the working hypothesis to "[[ y ]]". Then it sets the working hypothesis to "[[ x ]]". Then it adds "[[ x ]]" to all previously proved proof lines. Then it associates the label "[[ l ]]" with the conclusion "[[ x imply x ]]". Then it tactic evaluates the remainder of the proof. Finally it adds a proof of "[[ x imply x ]]".

\item "[[ define value of add-first-hyp* ( h , p , c ) as norm h is val : p is val : c is val : if p then true else add-first-hyp ( h , p head , c ) :: add-first-hyp* ( h , p tail , c ) end define ]]"

\item "[[ define value of add-first-hyp ( h , p , c ) as norm h is val : p is val : c is val : LET p 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 l 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 a IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN if is-meta-term ( r , c ) then p else LET make-root ( a , quote A1' Init Deref Ponens at h unquote at r unquote ;; a unquote end quote ) :: make-root ( a , quote A1' Init Deref Ponens at h unquote at r unquote end quote ) :: make-root ( a , quote A1' Init Deref Ponens at h unquote end quote ) :: make-root ( a , quote A1' Init Deref Ponens end quote ) :: make-root ( a , quote A1' Init Deref end quote ) :: make-root ( a , quote A1' Init end quote ) :: make-root ( a , quote A1' end quote ) :: true :: true :: true :: true :: h :: true :: r :: true :: a :: true BE asterisk IN LET asterisk BE a IN LET make-root ( r , quote h unquote imply r unquote end quote ) :: h :: r :: true BE asterisk IN LET asterisk BE r IN l :: r :: a :: <<>> end define ]]"



\subsection{Handling additional hyptheses}

\item "[[ define value of tactic-next-hyp ( h , t , s , c ) as norm h is val : t is val : s is val : c is val : 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 make-root ( t , quote h unquote and x unquote end quote ) :: h :: x :: true BE asterisk IN LET asterisk BE h prime IN LET s [[ hook-hyp -> h prime ]] BE asterisk IN LET asterisk BE s IN LET s [[ hook-pre -> add-next-hyp* ( x , s [[ hook-pre ]] , c ) ]] BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote h prime unquote imply x unquote end quote ) :: h prime :: x :: true BE asterisk IN LET asterisk BE x prime IN LET tactic-push ( hook-pre , l :: x prime :: make-root ( x prime , quote x prime unquote Init end quote ) :: x prime :: 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 LET s [[ hook-res ]] BE asterisk IN LET asterisk BE r IN if .not. r r= quote x imply y end quote .or. .not. r first r= quote x and y end quote then error ( x , LocateProofLine ( x , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r ) end diagnose ) else LET make-root ( t , quote Mend1.48e Init Deref Ponens at h unquote at x unquote end quote ) :: make-root ( t , quote Mend1.48e Init Deref Ponens at h unquote end quote ) :: make-root ( t , quote Mend1.48e Init Deref Ponens end quote ) :: make-root ( t , quote Mend1.48e Init Deref end quote ) :: make-root ( t , quote Mend1.48e Init end quote ) :: make-root ( t , quote Mend1.48e end quote ) :: true :: true :: true :: true :: h :: true :: x :: true BE asterisk IN LET asterisk BE a prime IN LET make-root ( t , quote Lcurry Init Deref Ponens at r first first unquote at r first second unquote at r second unquote Ponens end quote ) :: make-root ( t , quote Lcurry Init Deref Ponens at r first first unquote at r first second unquote at r second unquote end quote ) :: make-root ( t , quote Lcurry Init Deref Ponens at r first first unquote at r first second unquote end quote ) :: make-root ( t , quote Lcurry Init Deref Ponens at r first first unquote end quote ) :: make-root ( t , quote Lcurry Init Deref Ponens end quote ) :: make-root ( t , quote Lcurry Init Deref end quote ) :: make-root ( t , quote Lcurry Init end quote ) :: make-root ( t , quote Lcurry end quote ) :: true :: true :: true :: true :: r first first :: true :: r first second :: true :: r second :: true :: true BE asterisk IN LET asterisk BE a prime prime IN LET make-root ( t , quote r first first unquote imply r first second unquote imply r second unquote end quote ) :: r first first :: make-root ( t , quote r first second unquote imply r second unquote end quote ) :: r first second :: r second :: true :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> make-root ( t , quote a prime unquote ;; s [[ hook-arg ]] unquote ;; a prime prime unquote end quote ) :: a prime :: make-root ( t , quote s [[ hook-arg ]] unquote ;; a prime prime unquote end quote ) :: s [[ hook-arg ]] :: a prime prime :: true :: true ]] [[ hook-res -> r ]] end define ]]"

The definitions above adds the hypothesis to the working hypothesis. Then it adds "[[ x ]]" to all previously proved proof lines. Then it adds "[[ x ]]" to all previously proved proof lines. Then it associates the label "[[ l ]]" with the conclusion "[[ h and x imply x ]]". Then it tactic evaluates the remainder of the proof. Finally it adds a proof of "[[ h and x imply x ]]" and Curries the result from "[[ h and x imply b ]]" to "[[ h imply x imply b ]]" where "[[ h ]]" was the working hypothesis before the hypothesis "[[ x ]]" was added.

\item "[[ define value of add-next-hyp* ( x , p , c ) as norm x is val : p is val : c is val : if p then true else add-next-hyp ( x , p head , c ) :: add-next-hyp* ( x , p tail , c ) end define ]]"

\item "[[ define value of add-next-hyp ( x , p , c ) as norm x is val : p is val : c is val : LET p 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 l 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 a IN LET asterisk prime prime prime head BE asterisk IN LET asterisk prime prime prime tail BE asterisk prime prime prime IN if is-meta-term ( t , c ) then p 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 h 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 make-root ( a , quote a unquote ;; Lnexthyp Init Deref Ponens at h unquote at x unquote at r unquote Ponens end quote ) :: a :: make-root ( a , quote Lnexthyp Init Deref Ponens at h unquote at x unquote at r unquote Ponens end quote ) :: make-root ( a , quote Lnexthyp Init Deref Ponens at h unquote at x unquote at r unquote end quote ) :: make-root ( a , quote Lnexthyp Init Deref Ponens at h unquote at x unquote end quote ) :: make-root ( a , quote Lnexthyp Init Deref Ponens at h unquote end quote ) :: make-root ( a , quote Lnexthyp Init Deref Ponens end quote ) :: make-root ( a , quote Lnexthyp Init Deref end quote ) :: make-root ( a , quote Lnexthyp Init end quote ) :: make-root ( a , quote Lnexthyp end quote ) :: true :: true :: true :: true :: h :: true :: x :: true :: r :: true :: true :: true BE asterisk IN LET asterisk BE a IN LET make-root ( r , quote h unquote and x unquote imply r unquote end quote ) :: make-root ( r , quote h unquote and x unquote end quote ) :: h :: x :: true :: r :: true BE asterisk IN LET asterisk BE r IN l :: r :: a :: <<>> end define ]]"

\end{statements}



\subsection{Adaption}

\begin{statements}

\item "[[ define value of f.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-res ]] BE asterisk IN LET asterisk BE r IN LET r metadef ( c ) BE asterisk IN LET asterisk BE d IN if .not. d then s else if .not. r r= quote x imply y end quote then error ( r , LocateProofLine ( r , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r ) end diagnose ) else LET r first BE asterisk IN LET asterisk BE h IN LET r second BE asterisk IN LET asterisk BE r IN if .not. r metadef ( c ) then s else LET r mathdef ( c ) BE asterisk IN LET asterisk BE d IN if d = t then s else LET s [[ hook-arg ]] BE asterisk IN LET asterisk BE a IN if d = "all" then f.unitac-adapt-all ( t , h , a , r , r , s [[ hook-idx ]] , true , s , c ) else if d = "imply" then LET r first BE asterisk IN LET asterisk BE x IN LET r second BE asterisk IN LET asterisk BE y IN LET make-root ( t , quote a unquote ;; h unquote imply x unquote Init ;; MP' Init Deref Ponens at h unquote at x unquote at y unquote Ponens Ponens end quote ) :: a :: make-root ( t , quote h unquote imply x unquote Init ;; MP' Init Deref Ponens at h unquote at x unquote at y unquote Ponens Ponens end quote ) :: make-root ( t , quote h unquote imply x unquote Init end quote ) :: make-root ( t , quote h unquote imply x unquote end quote ) :: h :: x :: true :: true :: make-root ( t , quote MP' Init Deref Ponens at h unquote at x unquote at y unquote Ponens Ponens end quote ) :: make-root ( t , quote MP' Init Deref Ponens at h unquote at x unquote at y unquote Ponens end quote ) :: make-root ( t , quote MP' Init Deref Ponens at h unquote at x unquote at y unquote end quote ) :: make-root ( t , quote MP' Init Deref Ponens at h unquote at x unquote end quote ) :: make-root ( t , quote MP' Init Deref Ponens at h unquote end quote ) :: make-root ( t , quote MP' Init Deref Ponens end quote ) :: make-root ( t , quote MP' Init Deref end quote ) :: make-root ( t , quote MP' Init end quote ) :: make-root ( t , quote MP' end quote ) :: true :: true :: true :: true :: h :: true :: x :: true :: y :: true :: true :: true :: true :: true BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote h unquote imply y unquote end quote ) :: h :: y :: true BE asterisk IN LET asterisk BE r IN f.unitac-adapt ( t , s [[ hook-arg -> a ]] [[ hook-res -> r ]] , 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 mp and at operations to the argumentation inside "[[ s ]]" until the root of the conclusion is of type "[[ t ]]". As examples, "[[ t ]]" could be ``imply'', ``all'', ``var'', or "[[ true ]]". In the latter case, a maximum of mp and at operations are added. When "[[ t ]]" is ``var'', a minimum of operators are added (meaning that "[[ s ]]" is returned unchanged).

\item "[[ define value of f.unitac-adapt-all ( t , h , a , R , r , i , b , s , c ) as norm t is val : h is val : a is val : R is val : r is val : i is val : b is val : s is val : c is val : if r mathdef ( c ) = "all" then LET r First BE asterisk IN LET asterisk BE u IN LET r Second BE asterisk IN LET asterisk BE r IN LET univar ( a , u , i ) BE asterisk IN LET asterisk BE v IN LET u :: v :: b BE asterisk IN LET asterisk BE b IN f.unitac-adapt-all ( t , h , a , R , r , i + 1 , b , s , c ) else LET s [[ hook-idx -> i ]] BE asterisk IN LET asterisk BE s IN LET f.subst ( r , b , c ) BE asterisk IN LET asterisk BE r prime IN LET make-root ( a , quote a unquote ;; LAP4' Init Deref Ponens at h unquote at R unquote at r prime unquote Verify Ponens end quote ) :: a :: make-root ( a , quote LAP4' Init Deref Ponens at h unquote at R unquote at r prime unquote Verify Ponens end quote ) :: make-root ( a , quote LAP4' Init Deref Ponens at h unquote at R unquote at r prime unquote Verify end quote ) :: make-root ( a , quote LAP4' Init Deref Ponens at h unquote at R unquote at r prime unquote end quote ) :: make-root ( a , quote LAP4' Init Deref Ponens at h unquote at R unquote end quote ) :: make-root ( a , quote LAP4' Init Deref Ponens at h unquote end quote ) :: make-root ( a , quote LAP4' Init Deref Ponens end quote ) :: make-root ( a , quote LAP4' Init Deref end quote ) :: make-root ( a , quote LAP4' Init end quote ) :: make-root ( a , quote LAP4' end quote ) :: true :: true :: true :: true :: h :: true :: R :: true :: r prime :: true :: true :: true :: true BE asterisk IN LET asterisk BE a IN LET make-root ( r prime , quote h unquote imply r prime unquote end quote ) :: h :: r prime :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

Add at operations to the argumentation inside "[[ s ]]" until the root of the conclusion differs from ``all''. In a call to the functions, "[[ t ]]" indicates what to adapt to, "[[ h ]]" is the hypothesis, "[[ a ]]" is the argumentation, "[[ r ]]" is the result of the argumentation, "[[ R ]]" is the original result which is passed down unchanged, "[[ i ]]" is an index for generating fresh variables, "[[ b ]]" is a substitution, "[[ s ]]" is a tactic state, and "[[ c ]]" is a cache.

\end{statements}



\subsection{Ponens}

\begin{statements}

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

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

\item "[[ define value of f.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 f.unitac-adapt ( "imply" , 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 r= quote x imply y end quote then error ( t , LocateProofLine ( t , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r ) end diagnose ) else LET r first BE asterisk IN LET asterisk BE h IN LET r second BE asterisk IN LET asterisk BE r IN LET r first BE asterisk IN LET asterisk BE x IN LET r second BE asterisk IN LET asterisk BE y IN LET unieval ( t second , 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 if .not. r prime r= quote x imply y end quote then error ( t , LocateProofLine ( t , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r prime ) end diagnose ) else LET r prime second BE asterisk IN LET asterisk BE r prime IN LET s [[ hook-uni ]] BE asterisk IN LET asterisk BE u IN LET unify ( x , r prime , u ) BE asterisk IN LET asterisk BE u IN LET s [[ hook-uni -> u ]] BE asterisk IN LET asterisk BE s IN LET make-root ( t , quote a unquote ;; a prime unquote ;; MP' Init Deref Ponens at h unquote at x unquote at y unquote Ponens Ponens end quote ) :: a :: make-root ( t , quote a prime unquote ;; MP' Init Deref Ponens at h unquote at x unquote at y unquote Ponens Ponens end quote ) :: a prime :: make-root ( t , quote MP' Init Deref Ponens at h unquote at x unquote at y unquote Ponens Ponens end quote ) :: make-root ( t , quote MP' Init Deref Ponens at h unquote at x unquote at y unquote Ponens end quote ) :: make-root ( t , quote MP' Init Deref Ponens at h unquote at x unquote at y unquote end quote ) :: make-root ( t , quote MP' Init Deref Ponens at h unquote at x unquote end quote ) :: make-root ( t , quote MP' Init Deref Ponens at h unquote end quote ) :: make-root ( t , quote MP' Init Deref Ponens end quote ) :: make-root ( t , quote MP' Init Deref end quote ) :: make-root ( t , quote MP' Init end quote ) :: make-root ( t , quote MP' end quote ) :: true :: true :: true :: true :: h :: true :: x :: true :: y :: true :: true :: true :: true :: true BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote h unquote imply y unquote end quote ) :: h :: y :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

If the argumentation has form "[[ a mp a prime ]]" then convert "[[ a ]]" into something whose result has form "[[ h imply x imply y ]]". Convert "[[ a prime ]]" into something whose result has form "[[ h imply x prime ]]". Unify "[[ x ]]" with "[[ x prime ]]" and return argumentation "[[ a ;; a prime ;; A2 at --- ]]" and conclusion "[[ h imply y ]]".

\item "[[ define value of f.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 f.unitac-adapt ( "imply" , 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 r= quote x imply y end quote then error ( t , LocateProofLine ( t , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r ) end diagnose ) else LET r first BE asterisk IN LET asterisk BE h IN LET r second BE asterisk IN LET asterisk BE r IN LET r first BE asterisk IN LET asterisk BE x IN LET r second BE asterisk IN LET asterisk BE y IN LET make-root ( t , quote a unquote ;; h unquote imply x unquote Init ;; MP' Init Deref Ponens at h unquote at x unquote at y unquote Ponens Ponens end quote ) :: a :: make-root ( t , quote h unquote imply x unquote Init ;; MP' Init Deref Ponens at h unquote at x unquote at y unquote Ponens Ponens end quote ) :: make-root ( t , quote h unquote imply x unquote Init end quote ) :: make-root ( t , quote h unquote imply x unquote end quote ) :: h :: x :: true :: true :: make-root ( t , quote MP' Init Deref Ponens at h unquote at x unquote at y unquote Ponens Ponens end quote ) :: make-root ( t , quote MP' Init Deref Ponens at h unquote at x unquote at y unquote Ponens end quote ) :: make-root ( t , quote MP' Init Deref Ponens at h unquote at x unquote at y unquote end quote ) :: make-root ( t , quote MP' Init Deref Ponens at h unquote at x unquote end quote ) :: make-root ( t , quote MP' Init Deref Ponens at h unquote end quote ) :: make-root ( t , quote MP' Init Deref Ponens end quote ) :: make-root ( t , quote MP' Init Deref end quote ) :: make-root ( t , quote MP' Init end quote ) :: make-root ( t , quote MP' end quote ) :: true :: true :: true :: true :: h :: true :: x :: true :: y :: true :: true :: true :: true :: true BE asterisk IN LET asterisk BE a IN LET make-root ( t , quote h unquote imply y unquote end quote ) :: h :: y :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

\end{statements}



\subsection{At}

\begin{statements}

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

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

\item "[[ define value of f.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 f.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 if .not. r r= quote x imply y end quote then error ( t , LocateProofLine ( t , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r ) end diagnose ) else LET r first BE asterisk IN LET asterisk BE h IN LET r second BE asterisk IN LET asterisk BE r IN LET r First BE asterisk IN LET asterisk BE x IN LET r Second BE asterisk IN LET asterisk BE y 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 , x , i ) BE asterisk IN LET asterisk BE v IN LET f.subst ( y , x :: v :: <<>> , c ) BE asterisk IN LET asterisk BE r prime IN LET make-root ( t , quote a unquote ;; LAP4' Init Deref Ponens at h unquote at r unquote at r prime unquote Verify Ponens end quote ) :: a :: make-root ( t , quote LAP4' Init Deref Ponens at h unquote at r unquote at r prime unquote Verify Ponens end quote ) :: make-root ( t , quote LAP4' Init Deref Ponens at h unquote at r unquote at r prime unquote Verify end quote ) :: make-root ( t , quote LAP4' Init Deref Ponens at h unquote at r unquote at r prime unquote end quote ) :: make-root ( t , quote LAP4' Init Deref Ponens at h unquote at r unquote end quote ) :: make-root ( t , quote LAP4' Init Deref Ponens at h unquote end quote ) :: make-root ( t , quote LAP4' Init Deref Ponens end quote ) :: make-root ( t , quote LAP4' Init Deref end quote ) :: make-root ( t , quote LAP4' Init end quote ) :: make-root ( t , quote LAP4' end quote ) :: true :: true :: true :: true :: h :: true :: r :: true :: r prime :: true :: true :: true :: true BE asterisk IN LET asterisk BE a IN LET make-root ( r , quote h unquote imply r prime unquote end quote ) :: h :: r prime :: true BE asterisk IN LET asterisk BE r IN s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]"

If the argumentation has form "[[ a f.At ]]" then convert "[[ a ]]" into something whose conclusion is expected to be of form "[[ h imply f.allfunc \ x . y ]]". Then replace "[[ x ]]" by a fresh variable "[[ v ]]" in "[[ y ]]" and return conclusion "[[ h imply y ]]" and a suitable argumentation.

\item "[[ define value of f.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 f.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 if .not. r r= quote x imply y end quote then error ( t , LocateProofLine ( t , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r ) end diagnose ) else LET r first BE asterisk IN LET asterisk BE h IN LET r second BE asterisk IN LET asterisk BE r IN LET r First BE asterisk IN LET asterisk BE x IN LET r Second BE asterisk IN LET asterisk BE y 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 , x , i ) BE asterisk IN LET asterisk BE v IN LET f.subst ( y , x :: v :: <<>> , c ) BE asterisk IN LET asterisk BE r prime IN LET make-root ( t , quote a unquote ;; LAP4' Init Deref Ponens at h unquote at r unquote at r prime unquote Verify Ponens end quote ) :: a :: make-root ( t , quote LAP4' Init Deref Ponens at h unquote at r unquote at r prime unquote Verify Ponens end quote ) :: make-root ( t , quote LAP4' Init Deref Ponens at h unquote at r unquote at r prime unquote Verify end quote ) :: make-root ( t , quote LAP4' Init Deref Ponens at h unquote at r unquote at r prime unquote end quote ) :: make-root ( t , quote LAP4' Init Deref Ponens at h unquote at r unquote end quote ) :: make-root ( t , quote LAP4' Init Deref Ponens at h unquote end quote ) :: make-root ( t , quote LAP4' Init Deref Ponens end quote ) :: make-root ( t , quote LAP4' Init Deref end quote ) :: make-root ( t , quote LAP4' Init end quote ) :: make-root ( t , quote LAP4' end quote ) :: true :: true :: true :: true :: h :: true :: r :: true :: r prime :: true :: true :: true :: true BE asterisk IN LET asterisk BE a IN LET make-root ( r , quote h unquote imply r prime unquote end quote ) :: h :: r prime :: true 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 meta variable "[[ v ]]" in "[[ y ]]", unify "[[ v ]]" with "[[ a prime ]]", and return argumentation "[[ a at v ]]" and conclusion "[[ y ]]".

\end{statements}



\subsection{Deduction tactic}

We now state that "[[ Prop ]]", "[[ FOL ]]", and "[[ PA ]]" proofs may use deduction:

\begin{statements}

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

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

\item "[[ define tactic of PA as \ u . tactic-FOL ( u ) end define ]]".

\item "[[ define value of tactic-Prop ( 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 make-root ( t , quote x unquote infer Prop Rule conclude Prop ;; tactic-ded ( true , y unquote ) end quote ) :: x :: make-root ( t , quote Prop Rule conclude Prop ;; tactic-ded ( true , y unquote ) end quote ) :: make-root ( t , quote Prop Rule conclude Prop end quote ) :: make-root ( t , quote Prop Rule end quote ) :: make-root ( t , quote Prop end quote ) :: true :: true :: make-root ( t , quote Prop end quote ) :: true :: true :: make-root ( t , quote tactic-ded ( true , y unquote ) end quote ) :: make-root ( t , quote true end quote ) :: true :: y :: true :: true :: true BE asterisk IN LET asterisk BE t IN taceval ( t , s , c ) end define ]]"

\item "[[ define value of tactic-FOL ( 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 make-root ( t , quote x unquote infer Prop Rule conclude Prop ;; FOL Rule conclude FOL ;; tactic-ded ( true , y unquote ) end quote ) :: x :: make-root ( t , quote Prop Rule conclude Prop ;; FOL Rule conclude FOL ;; tactic-ded ( true , y unquote ) end quote ) :: make-root ( t , quote Prop Rule conclude Prop end quote ) :: make-root ( t , quote Prop Rule end quote ) :: make-root ( t , quote Prop end quote ) :: true :: true :: make-root ( t , quote Prop end quote ) :: true :: true :: make-root ( t , quote FOL Rule conclude FOL ;; tactic-ded ( true , y unquote ) end quote ) :: make-root ( t , quote FOL Rule conclude FOL end quote ) :: make-root ( t , quote FOL Rule end quote ) :: make-root ( t , quote FOL end quote ) :: true :: true :: make-root ( t , quote FOL end quote ) :: true :: true :: make-root ( t , quote tactic-ded ( true , y unquote ) end quote ) :: make-root ( t , quote true end quote ) :: true :: y :: true :: true :: true :: true BE asterisk IN LET asterisk BE t IN LET taceval ( t , s , c ) BE asterisk IN LET asterisk BE r IN r end define ]]"

\end{statements}



\subsection{Test proofs}

Elementary two level deduction. Import of L03 into inner deduction.

"[ ensure math define statement of lemma-x as FOL infer x imply y imply x end define,define unitac of lemma-x as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma-x as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; Line L02 : Prop Rule >> Prop ; Line L03 : Hypothesis >> x ; Line L04 : Hypothesis >> y ; L03 conclude x end quote , tacstate0 , c ) end define end math ]"



\noindent Import of lemma.

"[ ensure math define statement of lemma-y as FOL infer h imply x imply y imply x end define,define unitac of lemma-y as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma-y as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; Line L02 : Prop Rule >> Prop ; Line L03 : Hypothesis >> h ; lemma-x conclude x imply y imply x end quote , tacstate0 , c ) end define end math ]"



\noindent Import or rule.

"[ ensure math define statement of lemma-z as PA infer h imply i imply x + 0 = x end define,define unitac of lemma-z as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma-z as \ p . \ c . taceval ( quote Line L01 : Premise >> PA ; Line L02 : FOL Rule >> FOL ; Line L03 : Prop Rule >> Prop ; Line L04 : Hypothesis >> h ; Line L05 : Hypothesis >> i ; S5 conclude x + 0 = x end quote , tacstate0 , c ) end define end math ]"



\noindent Proof that contains a dummy hypothesis (Line L04) so that "[[ x mp y ]]" works.

"[ ensure math define statement of lemma-u as PA infer x = x end define,define unitac of lemma-u as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma-u as \ p . \ c . taceval ( quote Line L01 : Premise >> PA ; Line L02 : FOL Rule >> FOL ; Line L03 : Prop Rule >> Prop ; Line L04 : Deduction ; Line L05 : S5 >> x + 0 = x ; S1 mp L05 mp L05 conclude x = x end quote , tacstate0 , c ) end define end math ]"



\noindent Fully specified instantiation.

"[ ensure math define statement of lemma-v as PA infer h imply i imply x + 0 = x end define,define unitac of lemma-v as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma-v as \ p . \ c . taceval ( quote Line L01 : Premise >> PA ; Line L02 : FOL Rule >> FOL ; Line L03 : Prop Rule >> Prop ; Line L04 : Hypothesis >> h ; Line L05 : Hypothesis >> i ; S5 f.at x conclude x + 0 = x end quote , tacstate0 , c ) end define end math ]"



\noindent Partially specified instantiation.

"[ ensure math define statement of lemma-w as PA infer h imply i imply x + 0 = x end define,define unitac of lemma-w as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of lemma-w as \ p . \ c . taceval ( quote Line L01 : Premise >> PA ; Line L02 : FOL Rule >> FOL ; Line L03 : Prop Rule >> Prop ; Line L04 : Hypothesis >> h ; Line L05 : Hypothesis >> i ; S5 f.At conclude x + 0 = x end quote , tacstate0 , c ) end define end math ]"



\subsection{A proof of "[[ x + y = y + x ]]"}

"[ ensure math define statement of 3.2a as PA infer f.allfunc \ x . x = x end define,define unitac of 3.2a as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of 3.2a as \ p . \ c . taceval1 ( quote PA end quote , quote Line L01 : S5 >> x + 0 = x ; Line L02 : S1 mp L01 mp L01 >> x = x ; Gen1 ponens L02 conclude f.allfunc \ x . x = x end quote , c ) end define end math ]"



"[ ensure math define statement of 3.2b as PA infer f.allfunc \ x . f.allfunc \ y . x = y imply y = x end define,define unitac of 3.2b as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of 3.2b as \ p . \ c . taceval1 ( quote PA end quote , quote Line L00 : Block >> Begin ; Line L01 : Hypothesis >> x = y ; Line L02 : 3.2a >> x = x ; S1 mp L01 mp L02 conclude y = x line L04 : Block >> End ; Gen2 ponens L04 conclude f.allfunc \ x . f.allfunc \ y . x = y imply y = x end quote , c ) end define end math ]"



"[ ensure math define statement of 3.2c as PA infer f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . x = y imply y = z imply x = z end define,define unitac of 3.2c as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of 3.2c as \ p . \ c . taceval1 ( quote PA end quote , quote Line L01 : Block >> Begin ; Line L02 : Hypothesis >> x = y ; Line L03 : Hypothesis >> y = z ; Line L04 : 3.2b mp L02 >> y = x ; S1 mp L04 mp L03 conclude x = z line L06 : Block >> End ; Gen3 ponens L06 conclude f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . x = y imply y = z imply x = z end quote , c ) end define end math ]"



"[ ensure math define statement of 3.2d as PA infer f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . x = z imply y = z imply x = y end define,define unitac of 3.2d as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of 3.2d as \ p . \ c . taceval1 ( quote PA end quote , quote Line L00 : Block >> Begin ; Line L01 : Hypothesis >> x = z ; Line L02 : Hypothesis >> y = z ; Line L03 : 3.2b mp L02 >> z = y ; 3.2c mp L01 mp L03 conclude x = y line L05 : Block >> End ; Gen3 ponens L05 conclude f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . x = z imply y = z imply x = y end quote , c ) end define end math ]"



"[ ensure math define statement of 3.2e as PA infer f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . x = y imply x + z = y + z end define,define unitac of 3.2e as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of 3.2e as \ p . \ c . taceval1 ( quote PA end quote , quote Line L01 : Block >> Begin ; Line L02 : Hypothesis >> x = y ; Line L03 : S5 >> x + 0 = x ; Line L04 : 3.2c mp L03 mp L02 >> x + 0 = y ; Line L05 : S5 >> y + 0 = y ; 3.2d mp L04 mp L05 conclude x + 0 = y + 0 line L07 : Block >> End ; Line L08 : Block >> Begin ; Line L09 : Hypothesis >> x = y imply x + z = y + z ; Line L10 : Hypothesis >> x = y ; Line L11 : MP' ponens L09 ponens L10 >> x + z = y + z ; Line L12 : S2 mp L11 >> x + z suc = y + z suc ; Line L13 : S6 >> x + z suc = x + z suc ; Line L14 : 3.2c mp L13 mp L12 >> x + z suc = y + z suc ; Line L15 : S6 >> y + z suc = y + z suc ; 3.2d mp L14 mp L15 conclude x + z suc = y + z suc line L17 : Block >> End ; Line L18 : Induction at z ponens L07 ponens L17 >> x = y imply x + z = y + z ; Gen3 ponens L18 conclude f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . x = y imply x + z = y + z end quote , c ) end define end math ]"



"[ ensure math define statement of 3.2f as PA infer f.allfunc \ x . x = 0 + x end define,define unitac of 3.2f as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of 3.2f as \ p . \ c . taceval1 ( quote PA end quote , quote Line L01 : S5 >> 0 + 0 = 0 ; Line L02 : 3.2b mp L01 >> 0 = 0 + 0 ; Line L03 : Block >> Begin ; Line L04 : Hypothesis >> x = 0 + x ; Line L05 : S2 mp L04 >> x suc = 0 + x suc ; Line L06 : S6 >> 0 + x suc = 0 + x suc ; 3.2d mp L05 mp L06 conclude x suc = 0 + x suc line L08 : Block >> End ; Line L09 : Induction at x ponens L02 ponens L08 >> x = 0 + x ; Gen1 ponens L09 conclude f.allfunc \ x . x = 0 + x end quote , c ) end define end math ]"



"[ ensure math define statement of 3.2g as PA infer f.allfunc \ x . f.allfunc \ y . x suc + y = x + y suc end define,define unitac of 3.2g as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of 3.2g as \ p . \ c . taceval1 ( quote PA end quote , quote Line L01 : S5 >> x suc + 0 = x suc ; Line L02 : S5 >> x + 0 = x ; Line L03 : S2 mp L02 >> x + 0 suc = x suc ; Line L04 : 3.2d mp L01 mp L03 >> x suc + 0 = x + 0 suc ; Line L05 : Block >> Begin ; Line L06 : Hypothesis >> x suc + y = x + y suc ; Line L07 : S2 mp L06 >> x suc + y suc = x + y suc suc ; Line L08 : S6 >> x suc + y suc = x suc + y suc ; Line L09 : 3.2c mp L08 mp L07 >> x suc + y suc = x + y suc suc ; Line L10 : S6 >> x + y suc = x + y suc ; Line L11 : S2 mp L10 >> x + y suc suc = x + y suc suc ; 3.2d mp L09 mp L11 conclude x suc + y suc = x + y suc suc line L13 : Block >> End ; Line L14 : Induction at y ponens L04 ponens L13 >> x suc + y = x + y suc ; Gen2 ponens L14 conclude f.allfunc \ x . f.allfunc \ y . x suc + y = x + y suc end quote , c ) end define end math ]"



"[ ensure math define statement of 3.2h as PA infer f.allfunc \ x . f.allfunc \ y . x + y = y + x end define,define unitac of 3.2h as \ u . unitac-lemma ( u ) end define end math ]"

"[ ensure math define proof of 3.2h as \ p . \ c . taceval1 ( quote PA end quote , quote Line L01 : S5 >> x + 0 = x ; Line L02 : 3.2f >> x = 0 + x ; Line L03 : 3.2c mp L01 mp L02 >> x + 0 = 0 + x ; Line L04 : Block >> Begin ; Line L05 : Hypothesis >> x + y = y + x ; Line L06 : S2 mp L05 >> x + y suc = y + x suc ; Line L07 : S6 >> x + y suc = x + y suc ; Line L08 : 3.2c mp L07 mp L06 >> x + y suc = y + x suc ; Line L09 : 3.2g >> y suc + x = y + x suc ; 3.2d mp L08 mp L09 conclude x + y suc = y suc + x line L11 : Block >> End ; Line L12 : Induction at y ponens L03 ponens L11 >> x + y = y + x ; Gen2 ponens L12 conclude f.allfunc \ x . f.allfunc \ y . x + y = y + 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=Peano arithmetic - 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{Peano arithmetic - chores}
\author{Klaus Grue}
\maketitle
\tableofcontents



\section{\TeX\ definitions}

\begin{statements}

\item "[[ Define tex of line x : Hypothesis >> z ; u as "
\newline%
\makebox[0.1\textwidth]{}%
\parbox[b]{0.4\textwidth}{\raggedright%
\makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}%
$Hypothesis {} \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 : Hypothesis >> z ; u as "
L "[ x ]"
\colon Hypothesis
\gg "[ z ]"
; "[ u ]"" end define ]]"

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

\item "[[ Define tex name of line x : Deduction ; u as "
L "[ x ]"
\colon Deduction
; "[ u ]"" end define ]]"



\item "[[ Define tex of sub ( a , b , x , t ) as ""[ a ]"
\sim \langle "[ b ]"
\, | \, "[ x ]"
\, := "[ t ]"
\rangle" end define ]]"

\item "[[ Define tex of tt as "
\mathtt{\mathbf{T}}" end define ]]"

\item "[[ Define tex of ff as "
\mathtt{\mathbf{F}}" end define ]]"



\item "[[ Define tex of x First as ""[ x ]"
{}^{\underline{1}}" end define ]]"

\item "[[ Define tex of x Second as ""[ x ]"
{}^{\underline{2}}" end define ]]"

\item "[[ Define tex of x suc as ""[ x ]"
{}'" end define ]]"



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



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



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



\item "[[ Define tex of all x : y as "
\forall "[ x ]"
\colon \linebreak[0] "[ y ]"" end define ]]"

\item "[[ Define tex of exist x : y as "
\exists "[ x ]"
\colon \linebreak[0] "[ y ]"" end define ]]"



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

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

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



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



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

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



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

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

\end{statements}



\section{Pyk definitions}

\begin{flushleft}
"[[ 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 is-meta-term ( asterisk , asterisk ) as "is-meta-term ( "! , "! )" end define linebreak Define pyk of unitac-hyp as "unitac-hyp" end define linebreak Define pyk of unitac-lemma-hyp ( asterisk ) as "unitac-lemma-hyp ( "! )" end define linebreak Define pyk of unitac-rule-hyp ( asterisk ) as "unitac-rule-hyp ( "! )" end define linebreak Define pyk of unitac-conclude-hyp ( asterisk ) as "unitac-conclude-hyp ( "! )" end define linebreak Define pyk of tactic-hyp ( asterisk ) as "tactic-hyp ( "! )" end define linebreak Define pyk of tactic-dummyhyp ( asterisk ) as "tactic-dummyhyp ( "! )" end define linebreak Define pyk of tactic-ded ( asterisk , asterisk ) as "tactic-ded ( "! , "! )" end define linebreak Define pyk of tactic-first-hyp ( asterisk , asterisk , asterisk ) as "tactic-first-hyp ( "! , "! , "! )" end define linebreak Define pyk of add-first-hyp* ( asterisk , asterisk , asterisk ) as "add-first-hyp* ( "! , "! , "! )" end define linebreak Define pyk of add-first-hyp ( asterisk , asterisk , asterisk ) as "add-first-hyp ( "! , "! , "! )" end define linebreak Define pyk of tactic-next-hyp ( asterisk , asterisk , asterisk , asterisk ) as "tactic-next-hyp ( "! , "! , "! , "! )" end define linebreak Define pyk of add-next-hyp* ( asterisk , asterisk , asterisk ) as "add-next-hyp* ( "! , "! , "! )" end define linebreak Define pyk of add-next-hyp ( asterisk , asterisk , asterisk ) as "add-next-hyp ( "! , "! , "! )" end define linebreak Define pyk of f.unitac-adapt ( asterisk , asterisk , asterisk ) as "f.unitac-adapt ( "! , "! , "! )" end define linebreak Define pyk of f.unitac-adapt-all ( asterisk , asterisk , asterisk , asterisk , asterisk , asterisk , asterisk , asterisk , asterisk ) as "f.unitac-adapt-all ( "! , "! , "! , "! , "! , "! , "! , "! , "! )" end define linebreak Define pyk of f.tacfresh ( asterisk ) as "f.tacfresh ( "! )" end define linebreak Define pyk of f.unitac-ponens ( asterisk ) as "f.unitac-ponens ( "! )" end define linebreak Define pyk of f.unitac-Ponens ( asterisk ) as "f.unitac-Ponens ( "! )" end define linebreak Define pyk of f.unitac-at ( asterisk ) as "f.unitac-at ( "! )" end define linebreak Define pyk of f.unitac-At ( asterisk ) as "f.unitac-At ( "! )" end define linebreak Define pyk of sub ( asterisk , asterisk , asterisk , asterisk ) as "sub ( "! , "! , "! , "! )" end define linebreak Define pyk of sub0 ( asterisk , asterisk , asterisk , asterisk , asterisk ) as "sub0 ( "! , "! , "! , "! , "! )" end define linebreak Define pyk of sub1 ( asterisk , asterisk , asterisk , asterisk , asterisk ) as "sub1 ( "! , "! , "! , "! , "! )" end define linebreak Define pyk of sub* ( asterisk , asterisk , asterisk , asterisk , asterisk ) as "sub* ( "! , "! , "! , "! , "! )" end define linebreak Define pyk of f.subst ( asterisk , asterisk , asterisk ) as "f.subst ( "! , "! , "! )" end define linebreak Define pyk of f.subst* ( asterisk , asterisk , asterisk ) as "f.subst* ( "! , "! , "! )" end define linebreak Define pyk of inst ( asterisk , asterisk ) as "inst ( "! , "! )" end define linebreak Define pyk of inst0 ( asterisk , asterisk , asterisk ) as "inst0 ( "! , "! , "! )" end define linebreak Define pyk of inst1 ( asterisk , asterisk , asterisk ) as "inst1 ( "! , "! , "! )" end define linebreak Define pyk of inst-strip ( asterisk , asterisk , asterisk ) as "inst-strip ( "! , "! , "! )" end define linebreak Define pyk of inst-zip ( asterisk , asterisk ) as "inst-zip ( "! , "! )" end define linebreak Define pyk of inst2 ( asterisk , asterisk , asterisk , asterisk , asterisk ) as "inst2 ( "! , "! , "! , "! , "! )" end define linebreak Define pyk of inst2* ( asterisk , asterisk , asterisk , asterisk , asterisk ) as "inst2* ( "! , "! , "! , "! , "! )" end define linebreak Define pyk of inst3 ( asterisk , asterisk , asterisk ) as "inst3 ( "! , "! , "! )" end define linebreak Define pyk of inst3* ( asterisk , asterisk , asterisk ) as "inst3* ( "! , "! , "! )" end define linebreak Define pyk of def ( asterisk , asterisk ) as "def ( "! , "! )" end define linebreak Define pyk of def0 ( asterisk , asterisk , asterisk ) as "def0 ( "! , "! , "! )" end define linebreak Define pyk of def0* ( asterisk , asterisk , asterisk ) as "def0* ( "! , "! , "! )" end define linebreak Define pyk of def1 ( asterisk , asterisk , asterisk ) as "def1 ( "! , "! , "! )" end define linebreak Define pyk of def2 ( asterisk , asterisk , asterisk ) as "def2 ( "! , "! , "! )" end define linebreak Define pyk of def3 ( asterisk , asterisk , asterisk , asterisk ) as "def3 ( "! , "! , "! , "! )" end define linebreak Define pyk of def3* ( asterisk , asterisk , asterisk , asterisk ) as "def3* ( "! , "! , "! , "! )" end define linebreak Define pyk of defcheck as "defcheck" end define linebreak Define pyk of checked-def ( asterisk , asterisk ) as "checked-def ( "! , "! )" end define linebreak Define pyk of defcheck1 ( asterisk ) as "defcheck1 ( "! )" end define linebreak Define pyk of defcheck2 ( asterisk , asterisk ) as "defcheck2 ( "! , "! )" end define linebreak Define pyk of valid-def ( asterisk , asterisk , asterisk , asterisk ) as "valid-def ( "! , "! , "! , "! )" end define linebreak Define pyk of valid-def* ( asterisk , asterisk , asterisk , asterisk ) as "valid-def* ( "! , "! , "! , "! )" end define linebreak Define pyk of Prop as "Prop" end define linebreak Define pyk of FOL as "FOL" end define linebreak Define pyk of PA as "PA" end define linebreak Define pyk of MP as "MP" end define linebreak Define pyk of Gen as "Gen" end define linebreak Define pyk of Def as "Def" end define linebreak Define pyk of A1 as "A1" end define linebreak Define pyk of A2 as "A2" end define linebreak Define pyk of A3 as "A3" end define linebreak Define pyk of A4 as "A4" end define linebreak Define pyk of AP4 as "AP4" end define linebreak Define pyk of A5 as "A5" end define linebreak Define pyk of tt as "tt" end define linebreak Define pyk of ff as "ff" end define linebreak Define pyk of S1 as "S1" end define linebreak Define pyk of S2 as "S2" end define linebreak Define pyk of S3 as "S3" end define linebreak Define pyk of S4 as "S4" end define linebreak Define pyk of S5 as "S5" end define linebreak Define pyk of S6 as "S6" end define linebreak Define pyk of S7 as "S7" end define linebreak Define pyk of S8 as "S8" end define linebreak Define pyk of S9 as "S9" end define linebreak Define pyk of Mend1.8 as "Mend1.8" end define linebreak Define pyk of A1' as "A1'" end define linebreak Define pyk of A2' as "A2'" end define linebreak Define pyk of Mend1.47b as "Mend1.47b" end define linebreak Define pyk of Mend1.47c as "Mend1.47c" end define linebreak Define pyk of Mend1.47d as "Mend1.47d" end define linebreak Define pyk of Mend1.11b as "Mend1.11b" end define linebreak Define pyk of Mend1.48d as "Mend1.48d" end define linebreak Define pyk of Mend1.48e as "Mend1.48e" end define linebreak Define pyk of Lnexthyp as "Lnexthyp" end define linebreak Define pyk of Lcurry as "Lcurry" end define linebreak Define pyk of LTruth as "LTruth" end define linebreak Define pyk of LElimHyp as "LElimHyp" end define linebreak Define pyk of LA4' as "LA4'" end define linebreak Define pyk of LAP4' as "LAP4'" end define linebreak Define pyk of MP' as "MP'" end define linebreak Define pyk of Gen1 as "Gen1" end define linebreak Define pyk of Gen2 as "Gen2" end define linebreak Define pyk of Gen3 as "Gen3" end define linebreak Define pyk of Induction as "Induction" end define linebreak Define pyk of hook-hyp as "hook-hyp" end define linebreak Define pyk of tactic-Prop ( asterisk ) as "tactic-Prop ( "! )" end define linebreak Define pyk of tactic-FOL ( asterisk ) as "tactic-FOL ( "! )" end define linebreak Define pyk of lemma-x as "lemma-x" end define linebreak Define pyk of lemma-y as "lemma-y" end define linebreak Define pyk of lemma-z as "lemma-z" end define linebreak Define pyk of lemma-u as "lemma-u" end define linebreak Define pyk of lemma-v as "lemma-v" end define linebreak Define pyk of lemma-w as "lemma-w" end define linebreak Define pyk of hyp as "hyp" end define linebreak Define pyk of 3.2a as "3.2a" end define linebreak Define pyk of 3.2b as "3.2b" end define linebreak Define pyk of 3.2c as "3.2c" end define linebreak Define pyk of 3.2d as "3.2d" end define linebreak Define pyk of 3.2e as "3.2e" end define linebreak Define pyk of 3.2f as "3.2f" end define linebreak Define pyk of 3.2g as "3.2g" end define linebreak Define pyk of 3.2h as "3.2h" end define linebreak Define pyk of asterisk First as ""! First" end define linebreak Define pyk of asterisk Second as ""! Second" end define linebreak Define pyk of asterisk suc as ""! suc" end define linebreak Define pyk of not asterisk as "not "!" end define linebreak Define pyk of asterisk and asterisk as ""! and "!" end define linebreak Define pyk of asterisk or asterisk as ""! or "!" end define linebreak Define pyk of all asterisk : asterisk as "all "! : "!" end define linebreak Define pyk of f.allfunc asterisk as "f.allfunc "!" end define linebreak Define pyk of exist asterisk : asterisk as "exist "! : "!" end define linebreak Define pyk of f.existfunc asterisk as "f.existfunc "!" end define linebreak Define pyk of asterisk imply asterisk as ""! imply "!" end define linebreak Define pyk of asterisk when asterisk as ""! when "!" end define linebreak Define pyk of asterisk iff asterisk as ""! iff "!" end define linebreak Define pyk of asterisk avoid asterisk as ""! avoid "!" end define linebreak Define pyk of asterisk f.At as ""! f.At" end define linebreak Define pyk of asterisk Mp as ""! Mp" end define linebreak Define pyk of asterisk mp asterisk as ""! mp "!" end define linebreak Define pyk of asterisk f.at asterisk as ""! f.at "!" end define linebreak Define pyk of line asterisk : Hypothesis >> asterisk ; asterisk as "line "! : Hypothesis >> "! ; "!" end define linebreak Define pyk of Line asterisk : Hypothesis >> asterisk ; asterisk as "Line "! : Hypothesis >> "! ; "!" end define linebreak Define pyk of line asterisk : Deduction ; asterisk as "line "! : Deduction ; "!" end define linebreak Define pyk of Line asterisk : Deduction ; asterisk as "Line "! : Deduction ; "!" end define linebreak Define pyk of Peano as "Peano" end define linebreak empty ]]"
\end{flushleft}



\section{Priority table}

\begin {flushleft}
"[[ define priority of Peano as preassociative priority Peano 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 check 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 equal priority expand-all ( asterisk ) equal priority expand-all1 ( asterisk , asterisk , asterisk ) equal priority is-meta-term ( asterisk , asterisk ) equal priority unitac-hyp equal priority unitac-lemma-hyp ( asterisk ) equal priority unitac-rule-hyp ( asterisk ) equal priority unitac-conclude-hyp ( asterisk ) equal priority tactic-hyp ( asterisk ) equal priority tactic-dummyhyp ( asterisk ) equal priority tactic-ded ( asterisk , asterisk ) equal priority tactic-first-hyp ( asterisk , asterisk , asterisk ) equal priority add-first-hyp* ( asterisk , asterisk , asterisk ) equal priority add-first-hyp ( asterisk , asterisk , asterisk ) equal priority tactic-next-hyp ( asterisk , asterisk , asterisk , asterisk ) equal priority add-next-hyp* ( asterisk , asterisk , asterisk ) equal priority add-next-hyp ( asterisk , asterisk , asterisk ) equal priority f.unitac-adapt ( asterisk , asterisk , asterisk ) equal priority f.unitac-adapt-all ( asterisk , asterisk , asterisk , asterisk , asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority f.tacfresh ( asterisk ) equal priority f.unitac-ponens ( asterisk ) equal priority f.unitac-Ponens ( asterisk ) equal priority f.unitac-at ( asterisk ) equal priority f.unitac-At ( asterisk ) equal priority sub ( asterisk , asterisk , asterisk , asterisk ) equal priority sub0 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority sub1 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority sub* ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority f.subst ( asterisk , asterisk , asterisk ) equal priority f.subst* ( asterisk , asterisk , asterisk ) equal priority inst ( asterisk , asterisk ) equal priority inst0 ( asterisk , asterisk , asterisk ) equal priority inst1 ( asterisk , asterisk , asterisk ) equal priority inst-strip ( asterisk , asterisk , asterisk ) equal priority inst-zip ( asterisk , asterisk ) equal priority inst2 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority inst2* ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority inst3 ( asterisk , asterisk , asterisk ) equal priority inst3* ( asterisk , asterisk , asterisk ) equal priority def ( asterisk , asterisk ) equal priority def0 ( asterisk , asterisk , asterisk ) equal priority def0* ( asterisk , asterisk , asterisk ) equal priority def1 ( asterisk , asterisk , asterisk ) equal priority def2 ( asterisk , asterisk , asterisk ) equal priority def3 ( asterisk , asterisk , asterisk , asterisk ) equal priority def3* ( asterisk , asterisk , asterisk , asterisk ) equal priority defcheck equal priority checked-def ( asterisk , asterisk ) equal priority defcheck1 ( asterisk ) equal priority defcheck2 ( asterisk , asterisk ) equal priority valid-def ( asterisk , asterisk , asterisk , asterisk ) equal priority valid-def* ( asterisk , asterisk , asterisk , asterisk ) equal priority Prop equal priority FOL equal priority PA equal priority MP equal priority Gen equal priority Def equal priority A1 equal priority A2 equal priority A3 equal priority A4 equal priority AP4 equal priority A5 equal priority tt equal priority ff equal priority S1 equal priority S2 equal priority S3 equal priority S4 equal priority S5 equal priority S6 equal priority S7 equal priority S8 equal priority S9 equal priority Mend1.8 equal priority A1' equal priority A2' equal priority Mend1.47b equal priority Mend1.47c equal priority Mend1.47d equal priority Mend1.11b equal priority Mend1.48d equal priority Mend1.48e equal priority Lnexthyp equal priority Lcurry equal priority LTruth equal priority LElimHyp equal priority LA4' equal priority LAP4' equal priority MP' equal priority Gen1 equal priority Gen2 equal priority Gen3 equal priority Induction equal priority hook-hyp equal priority tactic-Prop ( asterisk ) equal priority tactic-FOL ( asterisk ) equal priority lemma-x equal priority lemma-y equal priority lemma-z equal priority lemma-u equal priority lemma-v equal priority lemma-w equal priority hyp equal priority 3.2a equal priority 3.2b equal priority 3.2c equal priority 3.2d equal priority 3.2e equal priority 3.2f equal priority 3.2g equal priority 3.2h 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 equal priority asterisk First equal priority asterisk Second equal priority asterisk suc 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 equal priority 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 equal priority asterisk and asterisk end priority greater than preassociative priority asterisk Or asterisk equal priority asterisk .or. asterisk equal priority asterisk or asterisk end priority greater than preassociative priority all asterisk : asterisk equal priority f.allfunc asterisk equal priority exist asterisk : asterisk equal priority f.existfunc asterisk end priority greater than postassociative priority asterisk Iff asterisk equal priority asterisk p.imply asterisk equal priority asterisk imply asterisk equal priority asterisk when asterisk equal priority asterisk iff 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 avoid 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 equal priority asterisk f.At equal priority asterisk Mp 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 equal priority asterisk mp asterisk equal priority asterisk f.at 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 equal priority line asterisk : Hypothesis >> asterisk ; asterisk equal priority Line asterisk : Hypothesis >> asterisk ; asterisk equal priority line asterisk : Deduction ; asterisk equal priority Line asterisk : Deduction ; 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:13:13.678589 = MJD-54293.TAI:20:13:46.678589 = LGT-4690988026678589e-6