Introduction to Logiweb

Klaus Grue

GRD-2005-05-26.UTC:06:49:32.964854

Contents

1 Introduction 2 1.1 Legal issues . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 More legal issues . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.4 Bibliographies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2 Logiweb sequent calculus 4

2.1 Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.1.1 Parameter terms . . . . . . . . . . . . . . . . . . . . . . . 4 2.1.2 Substitutions . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.1.3 Occurrence . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.1.4 Unifications . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.1.5 Circularity test . . . . . . . . . . . . . . . . . . . . . . . . 5 2.1.6 Unification algorithm . . . . . . . . . . . . . . . . . . . . 5

2.2 Proof generation . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2.1 Example lemmas . . . . . . . . . . . . . . . . . . . . . . . 6 2.2.2 Medium level proofs . . . . . . . . . . . . . . . . . . . . . 6 2.2.3 Proof tactics . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2.4 The proof expander . . . . . . . . . . . . . . . . . . . . . 7 2.2.5 The initial proof state . . . . . . . . . . . . . . . . . . . . 8 2.2.6 The conclusion tactic . . . . . . . . . . . . . . . . . . . . 8 2.2.7 Proof constructors . . . . . . . . . . . . . . . . . . . . . . 9

A Chores 10 A.1 Line numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

B TEX definitions 18

C Test 24

D Priority table 25

E Index 27 F Bibliography 29

1 Introduction

Disclaimer: This document is under construction.

Logiweb [1] is a system for distribution of mathematical definitions, lemmas, and proofs. More precisely, the Logiweb standard comprises a format, a semantics, and a protocol for storage, interpretation, and transmission of formal mathematics.

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

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

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

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

1.1 Legal issues

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

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

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

1.2 More legal issues

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

1.3 References

The reference of the present page is

     01
     37 E5 C4 3D B7  CC 92 BF 23 49
     70 40 5B C5 A3  0D AD A1 5B 46
     F6 EF A9 B0 BF  AA 9B 08 06

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

     nani
     nete kuti kata neki sete  kaka sinu seke nune tasi
     tena tana tise kati sune  naki suki suni tise tatu
     ketu kuke susi sena seke  susu sise nasa natu

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

1.4 Bibliographies

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

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

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

2 Logiweb sequent calculus

2.1 Unification

2.1.1 Parameter terms

We shall refer to terms in which bound metavariables are replaced by cardinals as parameter terms. The function [parm(t, s, n)] converts an ordinary term [t] into a parameter term in which numbers are constructed from [n] using [b +2∗ n] iteratively. When calling [parm(t, s, n)], [s] should be [T].

[parm(t, s, n) ˙= n! if t =^{r} ⌈∀x: y⌉ then ∀n: parm(t^{2}, (t^{1} : : n) : : s, T +2∗ n) else let m = lookup(t, s, T) in if ¬m then m else t^{R} : : parm^{∗}(t^{t}, s, n)]^{1}

[parm^{∗}(t, s, n) ˙= s!n!If(t^{a}, T, parm(t^{h}, s, n) : : parm^{∗}(t^{t}, s, n))]^{2}

2.1.2 Substitutions

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

[inst(t, s) ˙= If(t^{c}, s[t], t^{R} : : inst^{∗}(t^{t}, s))]^{3}

[inst^{∗}(t, s) ˙= s!If(t^{a}, T, inst(t^{h}, s) : : inst^{∗}(t^{t}, s))]^{4}

2.1.3 Occurrence

[occur(t, u)] is true if the parameter [t] occurs in the parameter term [u]:

[occur(t, u) ˙= If(u^{c}, t ≈ u, occur^{∗}(t, u^{t}))]^{5}

[occur^{∗}(t, u) ˙= t!If(u^{a}, F, occur(t, u^{h}) ¨∨ occur^{∗}(t, u^{t}))]^{6} 2.1.4 Unifications

1[parm(t, s, n) =^{pyk} “parameter term ∗ stack ∗ seed ∗ end parameter”]

2[parm^{∗}(t, s, n) =^{pyk} “parameter term star ∗ stack ∗ seed ∗ end parameter”]

3[inst(t, s) =^{pyk} “instantiate ∗ with ∗ end instantiate”]

4[inst^{∗}(t, s) =^{pyk} “instantiate star ∗ with ∗ end instantiate”]

5[occur(t, u) =^{pyk} “occur ∗ in ∗ end occur”]

6[occur^{∗}(t, u) =^{pyk} “occur star ∗ in ∗ end occur”]

We shall refer to the result of applying a substitution to a parameter term as an instance of the term. We shall refer to a common instance of two parameter terms as a unification of the terms. As an example, [A : : 2] and [1 : : B] (where [A] and [B] denote numbers) have exactly one unification, namely [1 : : 2]. We shall say that two terms are compatible if they have at least one unification and incompatible otherwise.

A substitution which yields the same result when applied to two terms [u] and [v] is said to unify the terms. As an example, the substitution which maps [A] to [1] and [B] to [2] unifies [A : : 2] and [1 : : B].

The unification algorithm presented in the following takes two terms as input and returns a unifying substitution if the terms are compatible. As an example, when applied to [A : : 2] and [1 : : B], the unification algorithm returns the substitution which maps [A] to [1] and [B] to [2].

There is more than one substitution which unifies [A : : 2] and [1 : : B]. As an example the substitution that maps [A] to [1], [B] to [2], and [C] to [3] also unifies [A : : 2] and [1 : : B].

2.1.5 Circularity test

[circular(t = u, s)] is true if adding the equation [t = u] to the unification [s] creates a circularity.

[circular(t = u, s) ˙= s!If(u^{c}, t ≈ u ¨∨ occur(t, s[u]), circular^{∗}(t = u^{t}, s))]^{7}

[circular^{∗}(t = u, s) ˙= t!s!If(u^{a}, F, circular(t = u^{h}, s) ¨∨ circular^{∗}(t = u^{t}, s))]^{8}

2.1.6 Unification algorithm

[unify(t = u, s) ˙= t!u! if s^{c} then s else if t^{c} then unify_{2}(t = u, s) else if u^{c} then unify_{2}(u = t, s) else if t =^{r} u then unify^{∗}(t^{t} = u^{t}, s) else 0]^{9}

[unify^{∗}(t = u, s) ˙= u!If(t^{a}, s, unify^{∗}(t^{t} = u^{t}, unify(t^{h} = u^{h}, s)))]^{10}

[unify_{2}(t = u, s) ˙= if t ≈ u then s else let t′ = s[t] in if ¬t′ then unify(t′ = u, s) else if circular(t = u, s) then 0 else s[t→u]]^{11}

7[circular(t = u, s) =^{pyk} “circular ∗ term ∗ substitution ∗ end circular”]

8[circular^{∗}(t = u, s) =^{pyk} “circular star ∗ term ∗ substitution ∗ end circular”]

9[unify(t = u, s) =^{pyk} “unify ∗ with ∗ substitution ∗ end unify”]

10[unify^{∗}(t = u, s) =^{pyk} “unify star ∗ with ∗ substitution ∗ end unify”]

11[unify_{2}(t = u, s) =^{pyk} “unify two ∗ with ∗ substitution ∗ end unify”]

2.2 Proof generation

2.2.1 Example lemmas

As examples of sequent proofs, we prove two lemmas in the example theory [T_{E}]:

[T_{E} lemma Reflexivity: ∀A: A = A]^{12}

[Proof of Reflexivity: ⌈T_{E} ⊢ ∀A: ( HeadPair^{I}^{⊳} ^{∗}^{⊳} @ A @ A; (Transitivity^{I}^{⊳} ^{∗}^{⊳} @(A : : A)^{h} @ A @ A)^{⊳} ^{⊳} )⌉]

[T_{E} lemma Commutativity: ∀A: ∀B: A = B ⊢ B = A]^{13}

[Proof of Commutativity: ⌈T_{E} ⊢ ∀A: ∀B: A = B ⊢ ( Reflexivity^{I}^{⊳} ^{∗}^{⊳} @ A; (Transitivity^{I}^{⊳} ^{∗}^{⊳} @ A @ B @ A)^{⊳} ^{⊳} )⌉]

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

2.2.2 Medium level proofs

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

[T_{E} lemma Reflexivity_{1}: ∀A: A = A]^{14}

T_{E} proof of Reflexivity_{1}:

L01: Arbitrary ≫  A  ;
L02: HeadPair ≫  (A : : A)^{h} = A  ;
L03: Transitivity ⊳ L02 ⊳ L02 ≫  A = A  □

2.2.3 Proof tactics

Counted in sequent operators, proofs typically comprise a small amount of original thought and a lot of trivial derivations. Frequently, trivial derivations can be generated by computer programs. Such programs are typically called tactics or proof tactics [2].

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

12[Reflexivity =^{pyk} “reflexivity lemma”]

13[Commutativity =^{pyk} “commutativity lemma”]

14[Reflexivity_{1} =^{pyk} “reflexivity lemma one”]

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

We make the [<tactic>] aspect self-evaluating and use [tactic] to denote it:

[<tactic> ˙= ⌈<tactic>⌉]^{15}

[tactic =^{msg} <tactic>]^{16}

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

[[x =^{tactic} y] ¨= [(x)^{p} →^{tactic} y]]^{17}

2.2.4 The proof expander

The proof expander [P(t, s, c)] proof expands the term [t] for the proof state [s] and the cache [c] and returns the result as a semitagged map. The untagged version [U(P(t, s, c))] is the expansion itself.

The proof expander [P(t, s, c)] differs from the macro expander [M(t, s, c)] in that it has no special treatment for page symbols and in that it uses the [tactic] aspect instead of the [macro] aspect.

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

The definition of [P(t, s, c)] is almost identical to that of [M(t, s, c)]. But it is easier to express since we can use macros like the ‘let’ macro when defining proof expansion. For obvious reasons, macros cannot be used when defining the notion of macro expansion. The definition of [P(t, s, c)] reads:

[P(t, s, c) ˙= s!

let d = aspect(<tactic>, t, c) in if d then t^{h} : : P^{∗}(t^{t}, s, c) else U^{M}(E(d^{3}, T, c) ‘ t ‘ s ‘ c)]^{18}

[P^{∗}(t, s, c) ˙= s!c!If(t, T, P(t^{h}, s, c) : : P^{∗}(t^{t}, s, c))]^{19} 2.2.5 The initial proof state

15[<tactic> =^{pyk} “the tactic aspect”]

16[tactic =^{pyk} “tactic”]

17[[x =^{tactic} y] =^{pyk} “tactic define ∗ as ∗ end define”]

18[P(t, s, c) =^{pyk} “proof expand ∗ state ∗ cache ∗ end expand”]

19[P^{∗}(t, s, c) =^{pyk} “proof expand list ∗ state ∗ cache ∗ end expand”]

Proof states have exactly the same format as macro states.

The initial proof state [p_{0}] is useful for passing as the second parameter to [P(t, s, c)]. [p_{0}] is a pair whose head is the proof expander itself and whose tail is left blank. The definition of [p_{0}] reads:

[p_{0} →^{val} M(λt.λs.λc.P(t, s, c)) : : T]^{20}

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

2.2.6 The conclusion tactic

The conclusion tactic [x ≫ y] constructs a proof of [y] from the partial proof [x]. The conclusion tactic does the following to the proof [x]:

• Whenever [x] references a lemma [l], the conclusion tactic replaces [l] by [l^{I}^{⊳} ^{∗}^{⊳} ].

• Whenever a subproof [u] of [x] proves [∀v: w], the conclusion tactic replaces [u] by [u @ a] where the tactic uses unification to guess [a].

• Whenever a subproof [u] of [x] proves [v ⊢⊢ w], the conclusion tactic replaces [u] by [u^{V}].

[x ≫ y =^{tactic} λt.λs.λc.conclude_{1}(t, c)]^{21}

[conclude_{1}(t, c) ˙= let r = conclude_{2}(t^{1}, t^{2}, c) in if r^{c} then error(“Unification failed”, t) else r]^{22}

[conclude_{2}(a, t, c) ˙= t! if a =^{r} ⌈x ⊳ y⌉ then conclude_{2}(a^{1}, a-color(t ⊳ a^{2}), c) else if a =^{r} ⌈x ⊳ ⊳ y⌉ then conclude_{2}(a^{1}, a-color(t ⊳ ⊳ a^{2}), c) else if a =^{r} ⌈x @ y⌉ then conclude_{2}(a^{1}, a-color(t @ a^{2}), c) else if aspect(<proof>, a, c) then error(“Lemma expected”, a) else let d = aspect(<stmt>, a, c) in conclude_{3}(a^{I}^{⊳} ^{∗}^{⊳} , t, parm(d^{3}^{2}, T, 1), T)]^{23} [conclude_{3}(a, t, l, s) ˙= a!t!l!s! if l =^{r} ⌈x ⊢ y⌉ then

20[p_{0} =^{pyk} “proof state”] 21[x ≫ y =^{pyk} “∗ conclude ∗”] 22[conclude_{1}(t, c) =^{pyk} “conclude one ∗ cache ∗ end conclude”] 23[conclude_{2}(a, t, c) =^{pyk} “conclude two ∗ proves ∗ cache ∗ end conclude”]

t =^{r} ⌈x ⊳ y⌉ \{ \begin{matrix}conclude_{3}(a^{⊳} , t^{1}, l^{2}, unify(l^{1} = t^{2}, s)) \\ conclude_{3}(a^{⊳} , t, l^{2}, s) \end{matrix} else

if l =^{r} ⌈x ⊢⊢ y⌉ then

t =^{r} ⌈x ⊳ ⊳ y⌉ \{ \begin{matrix}conclude_{3}(a^{⊳} , t^{1}, l^{2}, unify(l^{1} = t^{2}, s)) \\ conclude_{3}(a^{⊳} , t, l^{2}, s) \end{matrix} else

if l =^{r} ⌈∀x: y⌉ then

t =^{r} ⌈x @ y⌉ \{ \begin{matrix}conclude_{3}(a @ t^{2}, t^{1}, l^{2}, unify(l^{1} = t^{2}, s)) \\ conclude_{3}(a @ l^{1}, t, l^{2}, s) \end{matrix} else

let s = unify(l = t, s) in if s^{c} then s else inst(a, s)]^{24}

Modus ponens:

[x ⊳ y ˙= ⟨⌈x ⊳ y⌉^{R}, x, y⟩]^{25}

Modus probans:

[x ⊳ ⊳ y ˙= ⟨⌈x ⊳ ⊳ y⌉^{R}, x, y⟩]^{26}

2.2.7 Proof constructors

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

[t proof of s : p ¨= [Proof of s: λc.λx.P(⌈t ⊢ p⌉, p_{0}, c)]]^{27}

[Line l : a ≫ i; p ¨= (a ≫ i; let l ¨= i in p)]^{28}

[Last line a ≫ i ¨= (a ≫ i)]^{29}

[Line l : Premise ≫ i; p ¨= (i ⊢ let l ¨= i in p)]^{30}

[Line l : Side-condition ≫ i; p ¨= (i ⊢⊢ let l ¨= i in p)]^{31} [Arbitrary ≫ i; p ¨= (∀i: p)]^{32}

24[conclude_{3}(a, t, l, s) =^{pyk} “conclude three ∗ proves ∗ lemma ∗ substitution ∗ end conclude”] 25[x ⊳ y =^{pyk} “∗ modus ponens ∗”] 26[x ⊳ ⊳ y =^{pyk} “∗ modus probans ∗”] 27[t proof of l : p =^{pyk} “∗ proof of ∗ reads ∗”] 28[Line l : a ≫ i; p =^{pyk} “line ∗ because ∗ indeed ∗ cut ∗”] 29[Last line a ≫ i =^{pyk} “because ∗ indeed ∗ qed”] 30[Line l : Premise ≫ i; p =^{pyk} “line ∗ premise ∗ cut ∗”] 31[Line l : Side-condition ≫ i; p =^{pyk} “line ∗ side condition ∗ cut ∗”]

[Local ≫ a = i; p ¨= (let a ¨= i in p)]^{33}

A Chores

The name of the page:

[check =^{pyk} “check”]

A.1 Line numbers

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

[L_{a} =^{pyk} “ell a”] [L_{b} =^{pyk} “ell b”] [L_{c} =^{pyk} “ell c”] [L_{d} =^{pyk} “ell d”] [L_{e} =^{pyk} “ell e”] [L_{f} =^{pyk} “ell f”] [L_{g} =^{pyk} “ell g”] [L_{h} =^{pyk} “ell h”] [L_{i} =^{pyk} “ell i”] [L_{j} =^{pyk} “ell j”] [L_{k} =^{pyk} “ell k”] [L_{l} =^{pyk} “ell l”] [L_{m} =^{pyk} “ell m”] [L_{n} =^{pyk} “ell n”] [L_{o} =^{pyk} “ell o”] [L_{p} =^{pyk} “ell p”] [L_{q} =^{pyk} “ell q”] [L_{r} =^{pyk} “ell r”] [L_{s} =^{pyk} “ell s”] [L_{t} =^{pyk} “ell t”] [L_{u} =^{pyk} “ell u”] [L_{v} =^{pyk} “ell v”] [L_{w} =^{pyk} “ell w”] [L_{x} =^{pyk} “ell x”] [L_{y} =^{pyk} “ell y”] [L_{z} =^{pyk} “ell z”] [L_{A} =^{pyk} “ell big a”] [L_{B} =^{pyk} “ell big b”] [L_{C} =^{pyk} “ell big c”] [L_{D} =^{pyk} “ell big d”] [L_{E} =^{pyk} “ell big e”] [L_{F} =^{pyk} “ell big f”] [L_{G} =^{pyk} “ell big g”] [L_{H} =^{pyk} “ell big h”] [L_{I} =^{pyk} “ell big i”] [L_{J} =^{pyk} “ell big j”] [L_{K} =^{pyk} “ell big k”] [L_{L} =^{pyk} “ell big l”] [L_{M} =^{pyk} “ell big m”] [L_{N} =^{pyk} “ell big n”] [L_{O} =^{pyk} “ell big o”] [L_{P} =^{pyk} “ell big p”] [L_{Q} =^{pyk} “ell big q”] [L_{R} =^{pyk} “ell big r”] [L_{S} =^{pyk} “ell big s”] [L_{T} =^{pyk} “ell big t”] [L_{U} =^{pyk} “ell big u”] [L_{V} =^{pyk} “ell big v”] [L_{W} =^{pyk} “ell big w”] [L_{X} =^{pyk} “ell big x”] [L_{Y} =^{pyk} “ell big y”] [L_{Z} =^{pyk} “ell big z”] [L_{?} =^{pyk} “ell dummy”] [L_{a} =^{name} “L a”] [L_{b} =^{name} “L b”] [L_{c} =^{name} “L c”] [L_{d} =^{name} “L d”] [L_{e} =^{name} “L e”] [L_{f} =^{name} “L f”] [L_{g} =^{name} “L g”] [L_{h} =^{name} “L h”] [L_{i} =^{name} “L i”] [L_{j} =^{name} “L j”] [L_{k} =^{name} “L k”] [L_{l} =^{name} “L l”] [L_{m} =^{name} “L m”] [L_{n} =^{name} “L n”] [L_{o} =^{name} “L o”] [L_{p} =^{name} “L p”] [L_{q} =^{name} “L q”] [L_{r} =^{name} “L r”] [L_{s} =^{name} “L s”] [L_{t} =^{name} “L t”] [L_{u} =^{name} “L u”] [L_{v} =^{name} “L v”] [L_{w} =^{name} “L w”] [L_{x} =^{name} “L x”] [L_{y} =^{name} “L y”] [L_{z} =^{name} “L z”] [L_{A} =^{name} “L A”] [L_{B} =^{name} “L B”] [L_{C} =^{name} “L C”] [L_{D} =^{name} “L D”] [L_{E} =^{name} “L E”] [L_{F} =^{name} “L F”] [L_{G} =^{name} “L G”] [L_{H} =^{name} “L H”] [L_{I} =^{name} “L I”] [L_{J} =^{name} “L J”] [L_{K} =^{name} “L K”] [L_{L} =^{name} “L L”] [L_{M} =^{name} “L M”] [L_{N} =^{name} “L N”] [L_{O} =^{name} “L O”] [L_{P} =^{name} “L P”] [L_{Q} =^{name} “L Q”] [L_{R} =^{name} “L R”] [L_{S} =^{name} “L S”] [L_{T} =^{name} “L T”] [L_{U} =^{name} “L U”] [L_{V} =^{name} “L V”] [L_{W} =^{name} “L W”] [L_{X} =^{name} “L X”] [L_{Y} =^{name} “L Y”] [L_{Z} =^{name} “L Z”]

32[Arbitrary ≫ i; p =^{pyk} “arbitrary ∗ cut ∗”]

33[Local ≫ u = v; p =^{pyk} “locally define ∗ as ∗ cut ∗”]

[L_{?} =^{name} “L ?”]

[L_{a} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L a \else \if \relax \csname lgwella\endcsname \global \advance \lgwproofline by 1 \xdef \lgwella {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwella \fi ”]

[L_{b} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L b \else \if \relax \csname lgwellb\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellb {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellb \fi ”]

[L_{c} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L c \else \if \relax \csname lgwellc\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellc {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellc \fi ”]

[L_{d} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L d \else \if \relax \csname lgwelld\endcsname \global \advance \lgwproofline by 1 \xdef \lgwelld {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwelld \fi ”]

[L_{e} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L e \else \if \relax \csname lgwelle\endcsname \global \advance \lgwproofline by 1 \xdef \lgwelle {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwelle \fi ”]

[L_{f} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L f \else \if \relax \csname lgwellf\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellf {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellf \fi ”]

[L_{g} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L g \else \if \relax \csname lgwellg\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellg {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellg \fi ”]

[L_{h} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L h \else \if \relax \csname lgwellh\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellh {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellh \fi ”]

[L_{i} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L i \else \if \relax \csname lgwelli\endcsname \global \advance \lgwproofline by 1 \xdef \lgwelli {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwelli \fi ”]

[L_{j} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L j \else \if \relax \csname lgwellj\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellj {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellj \fi ”]

[L_{k} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L k \else \if \relax \csname lgwellk\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellk {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellk \fi ”]

[L_{l} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L l \else \if \relax \csname lgwelll\endcsname \global \advance \lgwproofline by 1 \xdef \lgwelll {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwelll \fi ”]

[L_{m} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L m \else \if \relax \csname lgwellm\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellm {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellm \fi ”]

[L_{n} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L n \else \if \relax \csname lgwelln\endcsname \global \advance \lgwproofline by 1 \xdef \lgwelln {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwelln \fi ”]

[L_{o} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{p} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L p \else \if \relax \csname lgwellp\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellp {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellp \fi ”]

[L_{q} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L q \else \if \relax \csname lgwellq\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellq {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellq \fi ”]

[L_{r} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L r \else \if \relax \csname lgwellr\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellr {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellr \fi ”]

[L_{s} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L s \else \if \relax \csname lgwells\endcsname \global \advance \lgwproofline by 1 \xdef \lgwells {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwells \fi ”]

[L_{t} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L t \else \if \relax \csname lgwellt\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellt {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellt \fi ”]

[L_{u} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L u \else \if \relax \csname lgwellu\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellu {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellu \fi ”]

[L_{v} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L v \else \if \relax \csname lgwellv\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellv {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellv \fi ”]

[L_{w} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L w \else \if \relax \csname lgwellw\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellw {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellw \fi ”]

[L_{x} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L x \else \if \relax \csname lgwellx\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellx {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellx \fi ”]

[L_{y} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L y \else \if \relax \csname lgwelly\endcsname \global \advance \lgwproofline by 1 \xdef \lgwelly {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwelly \fi ”]

[L_{z} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L z \else \if \relax \csname lgwellz\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellz {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellz \fi ”]

[L_{A} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L A \else \if \relax \csname lgwellbiga\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbiga {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbiga \fi ”]

[L_{B} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L B \else \if \relax \csname lgwellbigb\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigb {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigb \fi ”]

[L_{C} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L C \else \if \relax \csname lgwellbigc\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigc {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigc \fi ”]

[L_{D} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L D \else \if \relax \csname lgwellbigd\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigd {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigd \fi ”]

[L_{E} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L E \else \if \relax \csname lgwellbige\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbige {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbige \fi ”]

[L_{F} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L F \else \if \relax \csname lgwellbigf\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigf {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigf \fi ”]

[L_{G} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L G \else \if \relax \csname lgwellbigg\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigg {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigg \fi ”]

[L_{H} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L H \else \if \relax \csname lgwellbigh\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigh {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigh \fi ”]

[L_{I} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L I \else \if \relax \csname lgwellbigi\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigi {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigi \fi ”]

[L_{J} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L J \else \if \relax \csname lgwellbigj\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigj {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigj \fi ”]

[L_{K} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L K \else \if \relax \csname lgwellbigk\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigk {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigk \fi ”]

[L_{L} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L L \else \if \relax \csname lgwellbigl\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigl {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigl \fi ”]

[L_{M} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L M \else \if \relax \csname lgwellbigm\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigm {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigm \fi ”]

[L_{N} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L N \else \if \relax \csname lgwellbign\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbign {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbign \fi ”]

[L_{O} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L O \else \if \relax \csname lgwellbigo\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigo {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigo \fi ”]

[L_{P} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L P \else \if \relax \csname lgwellbigp\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigp {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigp \fi ”]

[L_{Q} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L Q \else \if \relax \csname lgwellbigq\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigq {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigq \fi ”]

[L_{R} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L R \else \if \relax \csname lgwellbigr\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigr {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigr \fi ”]

[L_{S} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L S \else \if \relax \csname lgwellbigs\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigs {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigs \fi ”]

[L_{T} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L T \else \if \relax \csname lgwellbigt\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigt {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigt \fi ”]

[L_{U} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L U \else \if \relax \csname lgwellbigu\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigu {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigu \fi ”]

[L_{V} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L V \else \if \relax \csname lgwellbigv\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigv {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigv \fi ”]

[L_{W} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L W \else \if \relax \csname lgwellbigw\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigw {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigw \fi ”]

[L_{X} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L X \else \if \relax \csname lgwellbigx\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigx {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigx \fi ”]

[L_{Y} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L Y \else \if \relax \csname lgwellbigy\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigy {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigy \fi ”]

[L_{Z} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L Z \else \if \relax \csname lgwellbigz\endcsname \global \advance \lgwproofline by 1 \xdef \lgwellbigz {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwellbigz \fi ”]

[L_{?} =^{tex} “

\if \relax \csname lgwprooflinep\endcsname L ? \else \global \advance \lgwproofline by 1 L\ifnum \lgwproofline <10 0\fi \number \lgwproofline \fi ”]

B TEX definitions

[parm(t, s, n) =^{tex} “ parm(#1. , #2. , #3. )”]

[parm^{∗}(t, s, n) =^{tex} “ parmˆ ∗(#1. , #2. , #3. )”]

[inst(t, s) =^{tex} “ inst(#1. , #2. )”]

[inst^{∗}(t, s) =^{tex} “ instˆ ∗(#1. , #2. )”]

[occur(t, u) =^{tex} “ occur(#1. , #2. )”] [occur^{∗}(t, u) =^{tex} “

occurˆ ∗(#1. , #2. )”]

[circular(t = u, s) =^{tex} “ circular(#1. =#2. , #3. )”]

[circular^{∗}(t = u, s) =^{tex} “ circularˆ ∗(#1. =#2. , #3. )”]

[unify(t = u, s) =^{tex} “ unify(#1. =#2. , #3. )”]

[unify^{∗}(t = u, s) =^{tex} “ unifyˆ ∗(#1. =#2. , #3. )”]

[unify_{2}(t = u, s) =^{tex} “ unify 2(#1. =#2. , #3. )”]

[Reflexivity =^{tex} “ Reflexivity”]

[Commutativity =^{tex} “ Commutativity”]

[Reflexivity_{1} =^{tex} “ Reflexivity 1”]

[<tactic> =^{tex} “ {<}tactic{>}”] [tactic =^{tex} “

tactic”]

[[x =^{tactic} y] =^{tex} “ [#1/tex name/tex. \stackrel {tactic}{=}#2. ]”]

[P(t, s, c) =^{tex} “

{\cal P}( #1. , #2. , #3. )”]

[P^{∗}(t, s, c) =^{tex} “

{\cal P}ˆ ∗( #1. , #2. , #3. )”]

[p_{0} =^{tex} “

p 0”]

[x ≫ y =^{tex} “#1.

\gg #2.”]

[conclude_{1}(t, c) =^{tex} “ conclude 1 ( #1. , #2. )”]

[conclude_{2}(a, t, c) =^{tex} “ conclude 2 ( #1. , #2. , #3. )”]

[conclude_{3}(a, t, l, s) =^{tex} “ conclude 3 ( #1. , #2. , #3. , #4. )”]

[x ⊳ y =^{tex} “#1.

\rhd #2.”]

[x ⊳ ⊳ y =^{tex} “#1.

\mathrel {\makebox [0mm][l]{$\rhd $}\, {\rhd }} #2.”]

[t proof of s : p =^{tex} “ \if\relax\csname lgwprooflinep\endcsname \def\lgwprooflinep{x} \newcount\lgwproofline \fi \begingroup \def\insideproof{x} \lgwproofline=0 #1. \mathbf {\ proof\ of\ } #2. \colon #3. \gdef\lgwella{\relax} \gdef\lgwellb{\relax} \gdef\lgwellc{\relax} \gdef\lgwelld{\relax} \gdef\lgwelle{\relax} \gdef\lgwellf{\relax} \gdef\lgwellg{\relax} \gdef\lgwellh{\relax} \gdef\lgwelli{\relax} \gdef\lgwellj{\relax} \gdef\lgwellk{\relax} \gdef\lgwelll{\relax} \gdef\lgwellm{\relax} \gdef\lgwelln{\relax} \gdef\lgwello{\relax} \gdef\lgwellp{\relax} \gdef\lgwellq{\relax} \gdef\lgwellr{\relax} \gdef\lgwells{\relax} \gdef\lgwellt{\relax} \gdef\lgwellu{\relax} \gdef\lgwellv{\relax} \gdef\lgwellw{\relax} \gdef\lgwellx{\relax} \gdef\lgwelly{\relax} \gdef\lgwellz{\relax} \gdef\lgwellbiga{\relax} \gdef\lgwellbigb{\relax} \gdef\lgwellbigc{\relax} \gdef\lgwellbigd{\relax} \gdef\lgwellbige{\relax} \gdef\lgwellbigf{\relax} \gdef\lgwellbigg{\relax} \gdef\lgwellbigh{\relax} \gdef\lgwellbigi{\relax} \gdef\lgwellbigj{\relax} \gdef\lgwellbigk{\relax} \gdef\lgwellbigl{\relax} \gdef\lgwellbigm{\relax} \gdef\lgwellbign{\relax} \gdef\lgwellbigo{\relax} \gdef\lgwellbigp{\relax} \gdef\lgwellbigq{\relax} \gdef\lgwellbigr{\relax} \gdef\lgwellbigs{\relax} \gdef\lgwellbigt{\relax} \gdef\lgwellbigu{\relax} \gdef\lgwellbigv{\relax} \gdef\lgwellbigw{\relax} \gdef\lgwellbigx{\relax} \gdef\lgwellbigy{\relax} \gdef\lgwellbigz{\relax} \endgroup ”]

[t proof of s : p =^{name} “#1. \mathbf{\ proof\ of\ } #2. : #3.”]

[Line l : a ≫ i; p =^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#1. $:}$#2. {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#3. $\hfill \makebox [0mm][l]{\quad ; }}#4.”]

[Line l : a ≫ i; p =^{name} “ Line \, #1. : #2. \gg #3. ; #4.”]

[Last line a ≫ i =^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$ \if \relax \csname lgwprooflinep\endcsname L ? \else \global \advance \lgwproofline by 1 L\ifnum \lgwproofline <10 0\fi \number \lgwproofline \fi $:}$#1. {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#2. $\hfill \makebox [0mm][l]{\quad \makebox[0mm]{$\Box$}}}”]

[Last line a ≫ i =^{name} “ Last\ line \, #1. \gg #2.”]

[Line l : Premise ≫ i; p =^{tex} “ \newline \makebox [0.1\textwidth ][l]{$#1. $:}\makebox [0.4\textwidth ][l]{$Premise{}\gg{}$}\quad \parbox [t]{0.4\textwidth }{$#2. $\hfill \makebox [0mm][l]{\quad ; }}#3.”]

[Line l : Premise ≫ i; p =^{name} “ Line \, #1. : Premise \gg #2. ; #3.”]

[Line l : Side-condition ≫ i; p =^{tex} “ \newline \makebox [0.1\textwidth ][l]{$#1. $:}\makebox [0.4\textwidth ][l]{ $\mbox{Side-condition}{}\gg{}$}\quad \parbox [t]{0.4\textwidth }{$#2. $\hfill \makebox [0mm][l]{\quad ; }}#3.”]

[Line l : Side-condition ≫ i; p =^{name} “ Line \, #1. : \mbox{Side-condition} \gg #2. ; #3.”]

[Arbitrary ≫ i; p =^{tex} “ \newline \makebox [0.1\textwidth ][l]{$ \if \relax \csname lgwprooflinep\endcsname L ? \else \global \advance \lgwproofline by 1 L\ifnum \lgwproofline <10 0\fi \number \lgwproofline \fi $:}\makebox [0.4\textwidth ][l]{$Arbitrary{}\gg{}$}\quad \parbox [t]{0.4\textwidth }{$#1. $\hfill \makebox [0mm][l]{\quad ; }}#2.”]

[Arbitrary ≫ i; p =^{name} “ Arbitrary \gg #1. ; #2.”] [Local ≫ a = i; p =^{tex} “

\newline\makebox[0.1\textwidth]{$ \if \relax \csname lgwprooflinep\endcsname L ? \else \global \advance \lgwproofline by 1 L\ifnum \lgwproofline <10 0\fi \number \lgwproofline \fi $:}% \makebox[0.4\textwidth]{$Local{}\gg{}$}% \quad% \parbox[t]{0.4\textwidth}{$#1. = #2. $\hfill\makebox[0mm][l]{\quad ; }}#3.”]

[Local ≫ a = i; p =^{name} “ Local \gg #1. = #2. ; #3.”]

C Test

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

[inst(parm(⌈∀x: ∀y: x + y⌉, T, 4), T[4→⌈u⌉][8→⌈v⌉]) =^{t} ⌈∀u: ∀v: u + v⌉]^{·}

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

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

[unify(⌈2⌉ = ⌈2⌉, T)]^{·}

[unify(⌈2⌉ = ⌈3⌉, T) ≈ 0]^{·}

[unify(⌈2 + 3⌉ = ⌈2 + 3⌉, T)]^{·}

[unify(⌈2 + 3⌉ = ⌈2 + 4⌉, T) ≈ 0]^{·}

[unify(⌈2⌉ = 3, T)[3] =^{t} ⌈2⌉]^{·}

[unify(3 = ⌈2⌉, T)[3] =^{t} ⌈2⌉]^{·}

[unify(⟨⌈x + y⌉^{R}, 1, ⌈3⌉⟩ = ⌈2 + 3⌉, T)[1] =^{t} ⌈2⌉]^{·}

[unify(⟨⌈x + y⌉^{R}, 1, ⌈3⌉⟩ = ⟨⌈x + y⌉^{R}, ⌈2⌉, 2⟩, T)[1] =^{t} ⌈2⌉]^{·}

[unify(parm(⌈A + 3⌉, ⟨⌈A⌉ : : 1⟩, 1) = parm(⌈2 + B⌉, ⟨⌈B⌉ : : 2⟩, 1), T)[1] =^{t} ⌈2⌉]^{·} [unify(parm(⌈A + 3⌉, ⟨⌈A⌉ : : 1⟩, 1) = parm(⌈2 + B⌉, ⟨⌈B⌉ : : 2⟩, 1), T)[2] =^{t} ⌈3⌉]^{·}

[inst(parm(⌈A + B⌉, ⟨⌈A⌉ : : 1, ⌈B⌉ : : 2⟩, 1), unify(parm(⌈A + 3⌉, ⟨⌈A⌉ : : 1⟩, 1) =

parm(⌈2 + B⌉, ⟨⌈B⌉ : : 2⟩, 1), T)) =^{t} ⌈2 + 3⌉]^{·}

[T]^{·}

D Priority table

Priority table Preassociative [check], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [math ∗ end math], [flush left [∗]], [x], [y], [z], [[∗ ▷◁ ∗]], [[∗ →^{∗} ∗]], [pyk], [tex], [name], [prio], [∗], [T], [if(∗, ∗, ∗)], [[∗ ⇒^{∗} ∗]], [val], [claim], [⊥], [f(∗)], [(∗)^{I}], [F], [\underline{0}], [\underline{1}], [\underline{2}], [\underline{3}], [\underline{4}], [\underline{5}], [\underline{6}], [\underline{7}], [\underline{8}], [\underline{9}], [0], [1], [2], [3], [4], [5], [6], [7], [8], [9], [a], [b], [c], [d], [e], [f], [g], [h], [i], [j], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [(∗)^{M}], [If(∗, ∗, ∗)], [array{∗} ∗ end array], [l], [c], [r], [empty], [⟨∗ | ∗:= ∗⟩], [M(∗)], [Ũ(∗)], [U(∗)], [U^{M}(∗)], [apply(∗, ∗)], [apply_{1}(∗, ∗)], [identifier(∗)], [identifier_{1}(∗, ∗)], [arrayplus(∗, ∗)], [array-remove(∗, ∗, ∗)], [array-put(∗, ∗, ∗, ∗)], [array-add(∗, ∗, ∗, ∗, ∗)], [bit(∗, ∗)], [bit_{1}(∗, ∗)], [rack], ["vector"], ["bibliography"], ["dictionary"], ["body"], ["codex"], ["expansion"], ["code"], ["cache"], ["diagnose"], ["pyk"], ["tex"], ["texname"], ["value"], ["message"], ["macro"], ["definition"], ["unpack"], ["claim"], ["priority"], ["lambda"], ["apply"], ["true"], ["if"], ["quote"], ["proclaim"], ["define"], ["introduce"], ["hide"], ["pre"], ["post"], [E(∗, ∗, ∗)], [E_{2}(∗, ∗, ∗, ∗, ∗)], [E_{3}(∗, ∗, ∗, ∗)], [E_{4}(∗, ∗, ∗, ∗)], [lookup(∗, ∗, ∗)], [abstract(∗, ∗, ∗, ∗)], [⌈∗⌉], [M(∗, ∗, ∗)], [M_{2}(∗, ∗, ∗, ∗)], [M^{∗}(∗, ∗, ∗)], [macro], [s_{0}], [zip(∗, ∗)], [assoc_{1}(∗, ∗, ∗)], [(∗)^{p}], [self], [[∗ ¨= ∗]], [[∗ ˙= ∗]], [[∗ ´= ∗]], [[∗ =^{pyk} ∗]], [[∗ =^{tex} ∗]], [[∗ =^{name} ∗]], [Priority table[∗]], [M̃_{1}], [M̃_{2}(∗)], [M̃_{3}(∗)], [M̃_{4}(∗, ∗, ∗, ∗)], [M̃(∗, ∗, ∗)], [Q̃(∗, ∗, ∗)], [Q̃_{2}(∗, ∗, ∗)], [Q̃_{3}(∗, ∗, ∗, ∗)], [Q̃^{∗}(∗, ∗, ∗)], [(∗)], [aspect(∗, ∗)], [aspect(∗, ∗, ∗)], [⟨∗⟩], [tuple_{1}(∗)], [tuple_{2}(∗)], [let_{2}(∗, ∗)], [let_{1}(∗, ∗)], [[∗ =^{claim} ∗]], [checker], [check(∗, ∗)], [check_{2}(∗, ∗, ∗)], [check_{3}(∗, ∗, ∗)], [check^{∗}(∗, ∗)], [check_{2}^{∗}(∗, ∗, ∗)], [[∗]^{·}], [[∗]^{−}], [[∗]^{∘}], [msg], [[∗ =^{msg} ∗]], [<stmt>], [stmt], [[∗ =^{stmt} ∗]], [HeadNil′], [HeadPair′], [Transitivity′], [⊥ ⊥], [Contra′], [T′_{E}], [L_{1}], [\underline{∗}], [A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N], [O], [P], [Q], [R], [S], [T ], [U], [V], [W], [X], [Y], [Z], [⟨∗ | ∗:= ∗⟩], [⟨^{∗}∗ | ∗:= ∗⟩], [∅], [Remainder], [(∗)^{v}], [error(∗, ∗)], [error_{2}(∗, ∗)], [proof(∗, ∗, ∗)], [proof_{2}(∗, ∗)], [S(∗, ∗)], [S^{I}(∗, ∗)], [S^{⊳} (∗, ∗)], [S_{1}^{⊳} (∗, ∗, ∗)], [S^{E}(∗, ∗)], [S_{1}^{E}(∗, ∗, ∗)], [S^{+}(∗, ∗)], [S_{1}^{+}(∗, ∗, ∗)], [S^{−}(∗, ∗)], [S_{1}^{−}(∗, ∗, ∗)], [S^{∗}(∗, ∗)], [S_{1}^{∗}(∗, ∗, ∗)], [S_{2}^{∗}(∗, ∗, ∗, ∗)], [S^{@}(∗, ∗)],

[S_{1}^{@}(∗, ∗, ∗)], [S^{⊢}(∗, ∗)], [S_{1}^{⊢}(∗, ∗, ∗, ∗)], [S⊢ ⊢(∗, ∗)], [S⊢ ⊢ ; 1(∗, ∗, ∗, ∗)], [S^{i.e.}(∗, ∗)],

[S_{1}^{i.e.}(∗, ∗, ∗, ∗)], [S_{2}^{i.e.}(∗, ∗, ∗, ∗, ∗)], [S^{∀}(∗, ∗)], [S_{1}^{∀}(∗, ∗, ∗, ∗)], [S^{;}(∗, ∗)], [S_{1}^{;}(∗, ∗, ∗)], [S_{2}^{;}(∗, ∗, ∗, ∗)], [T (∗)], [claims(∗, ∗, ∗)], [claims_{2}(∗, ∗, ∗)], [<proof>], [proof], [[Lemma ∗: ∗]], [[Proof of ∗: ∗]], [[∗ lemma ∗: ∗]], [[∗ antilemma ∗: ∗]], [[∗ rule ∗: ∗]], [[∗ antirule ∗: ∗]], [verifier], [V_{1}(∗)], [V_{2}(∗, ∗)], [V_{3}(∗, ∗, ∗, ∗)], [V_{4}(∗, ∗)], [V_{5}(∗, ∗, ∗, ∗)], [V_{6}(∗, ∗, ∗, ∗)], [V_{7}(∗, ∗, ∗, ∗)], [Cut(∗, ∗)], [Head_{⊕}(∗)], [Tail_{⊕}(∗)], [rule_{1}(∗, ∗)], [rule(∗, ∗)], [Rule tactic], [Plus(∗, ∗)], [[Theory ∗]], [theory_{2}(∗, ∗)], [theory_{3}(∗, ∗)], [theory_{4}(∗, ∗, ∗)], [HeadNil′′], [HeadPair′′], [Transitivity′′], [Contra′′], [HeadNil], [HeadPair], [Transitivity], [Contra], [T_{E}], [ragged right], [ragged right expansion ], [color(∗ : ∗)], [color^{∗}(∗ : ∗)], [vars(∗)], [vars^{∗}(∗)], [instantiate(∗ + ∗ : ∗)], [instantiate^{∗}(∗ + ∗ : ∗)], [unify(∗ : ∗ = ∗ : ∗ + ∗)], [unify^{∗}(∗ : ∗ = ∗ : ∗ + ∗)], [unify_{1}(∗ : ∗ = ∗ : ∗ + ∗)], [unify_{2}(∗ + ∗)], [unify_{3}(∗ = ∗ + ∗)], [parm(∗, ∗, ∗)], [parm^{∗}(∗, ∗, ∗)], [inst(∗, ∗)], [inst^{∗}(∗, ∗)], [occur(∗, ∗)], [occur^{∗}(∗, ∗)], [circular(∗ = ∗, ∗)], [circular^{∗}(∗ = ∗, ∗)], [unify(∗ = ∗, ∗)], [unify^{∗}(∗ = ∗, ∗)], [unify_{2}(∗ = ∗, ∗)], [L_{a}], [L_{b}], [L_{c}], [L_{d}], [L_{e}], [L_{f}], [L_{g}], [L_{h}], [L_{i}], [L_{j}], [L_{k}], [L_{l}], [L_{m}], [L_{n}], [L_{o}], [L_{p}], [L_{q}], [L_{r}], [L_{s}], [L_{t}], [L_{u}], [L_{v}], [L_{w}], [L_{x}], [L_{y}], [L_{z}], [L_{A}], [L_{B}], [L_{C}], [L_{D}], [L_{E}], [L_{F}], [L_{G}], [L_{H}], [L_{I}], [L_{J}], [L_{K}], [L_{L}], [L_{M}], [L_{N}], [L_{O}], [L_{P}], [L_{Q}], [L_{R}], [L_{S}], [L_{T}], [L_{U}], [L_{V}], [L_{W}], [L_{X}], [L_{Y}], [L_{Z}], [L_{?}], [Reflexivity], [Reflexivity_{1}], [Commutativity], [<tactic>], [tactic], [[∗ =^{tactic} ∗]], [P(∗, ∗, ∗)], [P^{∗}(∗, ∗, ∗)], [p_{0}], [conclude_{1}(∗, ∗)], [conclude_{2}(∗, ∗, ∗)], [conclude_{3}(∗, ∗, ∗, ∗)]; Preassociative [∗ {∗}], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]]; Preassociative [“ ∗ ”], [], [(∗)^{t}], [string(∗) + ∗], [string(∗) ++ ∗], [ ∗], [ ∗], [!∗], [”∗], [#∗], [$∗], [%∗], [&∗], [’∗], [(∗], [)∗], [∗∗], [+∗], [, ∗], [-∗], [.∗], [/∗], [0∗], [1∗], [2∗], [3∗], [4∗], [5∗], [6∗], [7∗], [8∗], [9∗], [:∗], [; ∗], [<∗], [=∗], [>∗], [?∗], [@∗], [A∗], [B∗], [C∗], [D∗], [E∗], [F∗], [G∗], [H∗], [I∗], [J∗], [K∗], [L∗], [M∗], [N∗], [O∗], [P∗], [Q∗], [R∗], [S∗], [T∗], [U∗], [V∗], [W∗], [X∗], [Y∗], [Z∗], [[∗], [\∗], []∗], [ˆ ∗], [ ∗], [‘∗], [a∗], [b∗], [c∗], [d∗], [e∗], [f∗], [g∗], [h∗], [i∗], [j∗], [k∗], [l∗], [m∗], [n∗], [o∗], [p∗], [q∗], [r∗], [s∗], [t∗], [u∗], [v∗], [w∗], [x∗], [y∗], [z∗], [{∗], [|∗], [}∗], [˜ ∗], [Preassociative ∗; ∗], [Postassociative ∗; ∗], [[∗], ∗], [priority ∗ end], [newline ∗], [macro newline ∗]; Preassociative [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗^{H}], [∗^{T}], [∗^{U}], [∗^{h}], [∗^{t}], [∗^{s}], [∗^{c}], [∗^{d}], [∗^{a}], [∗^{C}], [∗^{M}], [∗^{B}], [∗^{r}], [∗^{i}], [∗^{d}], [∗^{R}], [∗^{0}], [∗^{1}], [∗^{2}], [∗^{3}], [∗^{4}], [∗^{5}], [∗^{6}], [∗^{7}], [∗^{8}], [∗^{9}], [∗^{E}], [∗^{V}], [∗^{C}], [∗^{C^{∗}}]; Preassociative [∗ · ∗], [∗ ·_{0} ∗]; Preassociative [∗ + ∗], [∗ +_{0} ∗], [∗ +_{1} ∗], [∗ − ∗], [∗ −_{0} ∗], [∗ −_{1} ∗]; Preassociative [∗ ∪ {∗}], [∗ ∪ ∗], [∗\{∗}]; Postassociative [∗ ˙. . ∗], [∗ \underline{˙. .} ∗], [∗ \underline{: :} ∗], [∗ \underline{+2∗} ∗], [∗ : : ∗], [∗ +2∗ ∗]; Postassociative [∗, ∗]; Preassociative

[∗ ≈^{B} ∗], [∗ ≈^{D} ∗], [∗ ≈^{C} ∗], [∗ ≈^{P} ∗], [∗ ≈ ∗], [∗ = ∗], [∗ →^{+} ∗], [∗ =^{t} ∗], [∗ =^{t^{∗}} ∗], [∗ =^{r} ∗],

[∗ ∈_{t} ∗], [∗ ⊆_{T} ∗], [∗ =^{T} ∗], [∗ =^{s} ∗], [∗ free in ∗], [∗ free in^{∗} ∗], [∗ free for ∗ in ∗], [∗ free for^{∗} ∗ in ∗], [∗ ∈_{c} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗]; Preassociative [¬∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗]; Postassociative [∗ ¨⇒ ∗]; Postassociative [∗ : ∗], [∗!∗]; Preassociative

[∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix} ];

Preassociative [λ ∗ .∗], [Λ∗], [if ∗ then ∗ else ∗], [let ∗ = ∗ in ∗], [let ∗ ¨= ∗ in ∗]; Preassociative [∗^{I}], [∗^{⊳} ], [∗^{V}], [∗^{+}], [∗^{−}], [∗^{∗}]; Preassociative [∗ @ ∗], [∗ ⊳ ∗], [∗ ⊳ ⊳ ∗], [∗ ≫ ∗]; Postassociative [∗ ⊢ ∗], [∗ ⊢⊢ ∗], [∗ i.e. ∗]; Preassociative [∀∗: ∗]; Postassociative [∗ ⊕ ∗]; Postassociative [∗; ∗]; Preassociative [∗ proves ∗]; Preassociative [∗ proof of ∗ : ∗], [Line ∗ : ∗ ≫ ∗; ∗], [Last line ∗ ≫ ∗], [Line ∗ : Premise ≫ ∗; ∗], [Line ∗ : Side-condition ≫ ∗; ∗], [Arbitrary ≫ ∗; ∗], [Local ≫ ∗ = ∗; ∗]; Postassociative [∗ then ∗], [∗[ ∗]∗]; Preassociative [∗&∗]; Preassociative [∗\\∗]; End table

E Index

[x ≫ y] x conclude y, 8 [x ⊳ y] x modus ponens y, 9 [x ⊳ ⊳ y] x modus probans y, 9 [x proof of y : z] x proof of y reads z, 9

algorithm, unification, 5 [Arbitrary ≫ y; z] arbitrary x cut y, 10 arbitrary x cut y [Arbitrary ≫ x; y], 10

because x indeed y qed [Last line x ≫ y], 9

[circular(x = y, z)] circular x term y substitution z end circular, 5 [circular^{∗}(x = y, z)] circular star x term y substitution z end circular, 5 circular star x term y substitution z end circular [circular^{∗}(x = y, z)], 5 circular x term y substitution z end circular [circular(x = y, z)], 5 [Commutativity] commutativity lemma, 6 commutativity lemma [Commutativity], 6 compatible, 5 [conclude_{1}(x, y)] conclude one x cache y end conclude, 8 [conclude_{2}(x, y, z)] conclude two x proves y cache z end conclude, 8 [conclude_{3}(x, y, z, a)] conclude three x proves y lemma z substitution a end conclude, 9 conclusion tactic, 8

incompatible, 5 initial proof state, 8 [inst(x, y)] instantiate x with y end instantiate, 4 [inst^{∗}(x, y)] instantiate star x with y end instantiate, 4 instance, 5 instantiate star x with y end instantiate [inst^{∗}(x, y)], 4 instantiate x with y end instantiate [inst(x, y)], 4

[Last line x ≫ y] because x indeed y qed, 9 [Line x : y ≫ z; a] line x because y indeed z cut a, 9 line x because y indeed z cut a [Line x : y ≫ z; a], 9 line x premise y cut z [Line x : Premise ≫ y; z], 9 line x side condition y cut z [Line x : Side-condition ≫ y; z], 9 [Local ≫ x = y; z] locally define x as y cut z, 10 locally define x as y cut z [Local ≫ x = y; z], 10

mixed endian hexadecimal, 3

[occur(x, y)] occur x in y end occur, 4 [occur^{∗}(x, y)] occur star x in y end occur, 4 occur star x in y end occur [occur^{∗}(x, y)], 4 occur x in y end occur [occur(x, y)], 4

p: [p_{0}] proof state, 8 p: [P(x, y, z)] proof expand x state y cache z end expand, 7 p: [P^{∗}(x, y, z)] proof expand list x state y cache z end expand, 7 parameter term, 4 parameter term star x stack y seed z end parameter [parm^{∗}(x, y, z)], 4 parameter term x stack y seed z end parameter [parm(x, y, z)], 4 [parm(x, y, z)] parameter term x stack y seed z end parameter, 4 [parm^{∗}(x, y, z)] parameter term star x stack y seed z end parameter, 4 [Line x : Premise ≫ y; z] line x premise y cut z, 9 proof expander, 6 proof state, 7 proof state, initial, 8 proof tactic, 6 proof: [x proof of y : z] x proof of y reads z, 9

[Reflexivity] reflexivity lemma, 6 [Reflexivity_{1}] reflexivity lemma one, 6 reflexivity lemma [Reflexivity], 6 reflexivity lemma one [Reflexivity_{1}], 6

[Line x : Side-condition ≫ y; z] line x side condition y cut z, 9

[<tactic>] the tactic aspect, 7 tactic [tactic], 7 tactic aspect, 6 tactic define x as y end define [x =^{tactic} y], 7 tactic, conclusion, 8 tactic, proof, 6 tactic: [x =^{tactic} y], 7 term, parameter, 4 the tactic aspect [<tactic>], 7

unification, 5 unification algorithm, 5 unify, 5 [unify(x = y, z)] unify x with y substitution z end unify, 5 [unify^{∗}(x = y, z)] unify star x with y substitution z end unify, 5 [unify_{2}(x = y, z)] unify two x with y substitution z end unify, 5 unify star x with y substitution z end unify [unify^{∗}(x = y, z)], 5 unify two x with y substitution z end unify [unify_{2}(x = y, z)], 5 unify x with y substitution z end unify [unify(x = y, z)], 5

F Bibliography

[1] K. Grue. Logiweb. In Fairouz Kamareddine, editor, Mathematical Knowledge Management Symposium 2003, volume 93 of Electronic Notes in Theoretical Computer Science, pages 70–101. Elsevier, 2004.

[2] C. P. Wadsworth M. J. Gordon, A. J. Milner. Edinburgh LCF, A mechanised logic of computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.