Logiweb codex of base

Up Help

base, [∗ ▷◁ ∗], “ ∗ ”, , ∗ then ∗, ∗[ ∗]∗, Preassociative ∗; ∗, Postassociative ∗; ∗, [∗], ∗, priority ∗ end, ∗, ∗, (∗)^{t}, string(∗) + ∗, string(∗) ++ ∗, bracket ∗ end bracket, big bracket ∗ end bracket, math ∗ end math, flush left [∗], x, y, z, [∗ →^{∗} ∗], pyk, tex, name, prio, T, if(∗, ∗, ∗), [∗ ⇒^{∗} ∗], val, claim, ∗, !∗, ”∗, #∗, $∗, %∗, &∗, ’∗, (∗, )∗, ∗∗, +∗, , ∗, -∗, .∗, /∗, 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∗, \{∗, |∗, \}∗, ˜ ∗, ⊥, 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}(∗, ∗), array-plus(∗, ∗), arrayremove(∗, ∗, ∗), 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}, intro(∗, ∗, ∗, ∗), intro(∗, ∗, ∗), 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 , parm(∗, ∗, ∗), parm^{∗}(∗, ∗, ∗), inst(∗, ∗), inst^{∗}(∗, ∗), occur(∗, ∗, ∗), occur^{∗}(∗, ∗, ∗), 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, Commutativity_{1}, <tactic>, tactic, [∗ =^{tactic} ∗], P(∗, ∗, ∗), P^{∗}(∗, ∗, ∗), p_{0}, conclude_{1}(∗, ∗), conclude_{2}(∗, ∗, ∗), conclude_{3}(∗, ∗, ∗, ∗), conclude_{4}(∗, ∗), ∗ {∗}, ∗′, ∗[ ∗], ∗[∗→∗], ∗[∗⇒∗], newline ∗, macro newline ∗, ∗0, ∗1, 0b, ∗-color(∗), ∗-color^{∗}(∗), ∗ ’ ∗, ∗ ‘ ∗, ∗^{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^{∗}}, ∗ · ∗, ∗ ·_{0} ∗, ∗ + ∗, ∗ +_{0} ∗, ∗ +_{1} ∗, ∗ − ∗, ∗ −_{0} ∗,

∗ −_{1} ∗, ∗ ∪ \{∗\}, ∗ ∪ ∗, ∗\\{∗\}, ∗ ˙. . ∗, ∗ \underline{˙. .} ∗, ∗ \underline{: :} ∗, ∗ \underline{+2∗} ∗, ∗ : : ∗, ∗ +2∗ ∗, ∗, ∗,

∗ ≈^{B} ∗, ∗ ≈^{D} ∗, ∗ ≈^{C} ∗, ∗ ≈^{P} ∗, ∗ ≈ ∗, ∗ = ∗, ∗ →^{+} ∗, ∗ =^{t} ∗, ∗ =^{t^{∗}} ∗, ∗ =^{r} ∗, ∗ ∈_{t} ∗,

∗ ⊆_{T} ∗, ∗ =^{T} ∗, ∗ =^{s} ∗, ∗ free in ∗, ∗ free in^{∗} ∗, ∗ free for ∗ in ∗, ∗ free for^{∗} ∗ in ∗,

∗ ∈_{c} ∗, ∗ < ∗, ∗ <′ ∗, ∗ ≤′ ∗, ¬∗, ∗ ∧ ∗, ∗ ¨∧ ∗, ∗ ˜∧ ∗, ∗ ∧_{c} ∗, ∗ ∨ ∗, ∗ ∥ ∗, ∗ ¨∨ ∗,

∗ ¨⇒ ∗, ∗ : ∗, ∗!∗, ∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix} , λ ∗ .∗, Λ∗, if ∗ then ∗ else ∗, let ∗ = ∗ in ∗,

let ∗ ¨= ∗ in ∗, ∗^{I}, ∗^{⊳} , ∗^{V}, ∗^{+}, ∗^{−}, ∗^{∗}, ∗ @ ∗, ∗ ⊳ ∗, ∗ ⊳ ⊳ ∗, ∗ ≫ ∗, ∗ ⊢ ∗, ∗ ⊢⊢ ∗,

∗ i.e. ∗, ∀∗: ∗, ∗ ⊕ ∗, ∗; ∗, ∗ proves ∗, ∗ proof of ∗ : ∗, Line ∗ : ∗ ≫ ∗; ∗, Last line ∗ ≫ ∗ □, Line ∗ : Premise ≫ ∗; ∗, Line ∗ : Side-condition ≫ ∗; ∗, Arbitrary ≫ ∗; ∗, Local ≫ ∗ = ∗; ∗, ∗&∗, ∗\\∗,

base

[base →^{prio} Preassociative [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}], [intro(∗, ∗, ∗, ∗)], [intro(∗, ∗, ∗)], [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 ], [parm(∗, ∗, ∗)], [parm^{∗}(∗, ∗, ∗)], [inst(∗, ∗)], [inst^{∗}(∗, ∗)], [occur(∗, ∗, ∗)], [occur^{∗}(∗, ∗, ∗)], [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], [Commutativity_{1}], [<tactic>], [tactic], [[∗ =^{tactic} ∗]], [P(∗, ∗, ∗)], [P^{∗}(∗, ∗, ∗)], [p_{0}], [conclude_{1}(∗, ∗)], [conclude_{2}(∗, ∗, ∗)], [conclude_{3}(∗, ∗, ∗, ∗)], [conclude_{4}(∗, ∗)]; 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 [∗\\∗]; ]

[base →^{macro} λt.λc.M(t, s_{0}, c)]

[base →^{claim} checker ∧_{c} verifier]

[base →^{pyk} “base”]

[∗ ▷◁ ∗]

Predef: proclaim

[[x ▷◁ y] →^{tex} “

[#1/tex name/tex. \bowtie#2. ]”]

[[x ▷◁ y] →^{pyk} “proclaim ∗ as ∗ end proclaim”]

“ ∗ ”

Predef: hide

[“x” →^{name} “

\mbox{‘‘}#1. \mbox{’’}”]

[“x” →^{macro} λt.λs.λc.t]

[“x” →^{tex} “#1.”]

[“x” →^{pyk} “unicode start of text ∗ end unicode text”]

[→^{tex} “”]

[ →^{pyk} “unicode end of text”]

∗ then ∗

[x then y →^{name} “#1. \mathrel{\mathrm{then}}#2.”]

[x then y →^{val} ⌈∗∗⌉^{R} : : [ x : : [ y : : T ] ] ]

[x then y →^{tex} “#1.#2.”]

[x then y →^{pyk} “∗

then ∗”]

∗[ ∗]∗

[x[y]z →^{name} “#1.

{[}#2. {]}#3.”]

[x[y]z →^{tex} “#1.#2.#3.”]

[x[y]z →^{pyk} “∗

begin ∗

end ∗”]

Preassociative ∗; ∗

Predef: pre

[Preassociative x; y →^{name} “ \mathbf{Preassociative}\, #1. ; #2.”]

[Preassociative x; y →^{tex} “ \newline \mathbf {Preassociative} \newline #1. ; #2.”] [Preassociative x; y →^{pyk} “preassociative ∗ greater than ∗”]

Postassociative ∗; ∗

Predef: post

[Postassociative x; y →^{name} “ \mathbf{Postassociative}\, #1. ; #2.”]

[Postassociative x; y →^{tex} “ \newline\mathbf{Postassociative} \newline #1. ; #2.”]

[Postassociative x; y →^{pyk} “postassociative ∗ greater than ∗”]

[∗], ∗

[[x], y →^{name} “

[#1. ] , \linebreak [0] #2.”]

[[x], y →^{tex} “

[#1/tex name/tex. ] , \linebreak [0] #2.”]

[[x], y →^{pyk} “priority ∗ equal ∗”]

priority ∗ end

[priority x end →^{name} “ \mathrm{priority} \, #1. \, \mathrm{end}”]

[priority x end →^{tex} “ [#1/tex name/tex. ]”]

[priority x end →^{pyk} “priority ∗ end priority”]

∗

[

x →^{name} “

\newline #1.”]

[

x →^{tex} “

#1.”]

[

x →^{pyk} “

unicode newline ∗”]

∗

[∗ →^{tex} “

\ast ”]

[∗ →^{pyk} “x”]

(∗)^{t}

[(x)^{t} →^{name} “

(#1. )ˆ {\bf t}”]

[(x)^{t} →^{val} ⌈∗⌉^{R} : : [ x : : T ] ]

[(x)^{t} →^{tex} “#1/tex name.”]

[(x)^{t} →^{pyk} “text ∗ end text”]

string(∗) + ∗

[string(x) + y →^{name} “ \mbox{string}(#1. )+#2.”]

[string(x) + y →^{tex} “ \mathrm{#1/tex name. }+\newline#2.”] [string(x) + y →^{pyk} “text ∗ plus ∗”]

string(∗) ++ ∗

[string(x) ++ y →^{name} “\mbox{string}(#1. )\mathrel{++}#2.”]

[string(x) ++ y →^{tex} “ \mathrm{#1/tex name. }\; {++}\newline{}\qquad#2.”]

[string(x) ++ y →^{pyk} “text ∗ plus indent ∗”]

bracket ∗ end bracket

[bracket x end bracket →^{name} “ \mbox{bracket $#1.$ end bracket}”]

[bracket x end bracket →^{tex} “$[#1.]$”]

[bracket x end bracket →^{pyk} “bracket ∗ end bracket”]

big bracket ∗ end bracket

[big bracket x end bracket →^{name} “ \mbox{big bracket $#1.$ end bracket}”]

[big bracket x end bracket →^{tex} “$\left[#1.\right]$”]

[big bracket x end bracket →^{pyk} “big bracket ∗ end bracket”]

math ∗ end math

[math x end math →^{name} “ \mbox{math $#1.$ end math}”]

[math x end math →^{tex} “$#1.$”]

[math x end math →^{pyk} “math ∗ end math”]

flush left [∗]

[flush left [x] →^{name} “ \mathbf{flush\ left\ }[ #1. ]”]

[flush left [x] →^{tex} “ \begin {flushleft}#1. \end {flushleft}”]

[flush left [x] →^{pyk} “flush left ∗ end left”]

x

[x →^{tex} “

\mathsf{x}”]

[x →^{pyk} “var x”]

y

[y →^{tex} “

\mathsf{y}”]

[y →^{pyk} “var y”]

z

[z →^{tex} “

\mathsf{z}”]

[z →^{pyk} “var z”]

[∗ →^{∗} ∗]

Predef: define

[[y →^{x} z] →^{tex} “

[#2/tex name/tex. \stackrel{#1. }{\rightarrow}#3. ]”] [[y →^{x} z] →^{pyk} “define ∗ of ∗ as ∗ end define”]

pyk

Predef: pyk

[pyk →^{tex} “

\mathrm{pyk}”] [pyk →^{pyk} “pyk”]

tex

Predef: tex

[tex →^{tex} “

\mathrm{tex}”] [tex →^{pyk} “tex”]

name

Predef: texname

[name →^{tex} “

\mathrm{name}”] [name →^{pyk} “tex name”]

prio

Predef: priority

[prio →^{tex} “

\mathrm{prio}”] [prio →^{pyk} “priority”]

T

Predef: true

[T →^{tex} “

\mathsf {T}”]

[T →^{pyk} “true”]

if(∗, ∗, ∗)

Predef: if

[if(∗, ∗, ∗) →^{tex} “

\mathrm {if}(#1. , \linebreak [0]#2. , \linebreak [0]#3. )”]

[if(∗, ∗, ∗) →^{pyk} “if ∗ then ∗ else ∗ end if”]

[∗ ⇒^{∗} ∗]

Predef: introduce

[[∗ ⇒^{∗} ∗] →^{tex} “

[#2/tex name/tex. \stackrel {#1. }{\Rightarrow }#3. ]”]

[[∗ ⇒^{∗} ∗] →^{pyk} “introduce ∗ of ∗ as ∗ end introduce”]

val

Predef: value

[val →^{tex} “

\mathrm {val}”]

[val →^{pyk} “value”]

claim

Predef: claim

[claim →^{tex} “ \mathrm {claim}”] [claim →^{pyk} “claim”]

∗

[ x →^{name} “

\linebreak [0]\ \hskip0em plus2.0em{}#1.”]

[ x →^{tex} “ #1.”]

[ x →^{pyk} “unicode space ∗”]

!∗

[!x →^{tex} “!#1.”]

[!x →^{pyk} “unicode exclamation mark ∗”]

”∗

[”x →^{tex} “”#1.”]

[”x →^{pyk} “unicode quotation mark ∗”]

#∗

[#x →^{name} “

\#.#1.”]

[#x →^{tex} “#.#1.”]

[#x →^{pyk} “unicode number sign ∗”]

$∗

[$x →^{name} “

\$#1.”]

[$x →^{tex} “$#1.”]

[$x →^{pyk} “unicode dollar sign ∗”]

%∗

[%x →^{name} “

\%#1.”]

[%x →^{tex} “%#1.”]

[%x →^{pyk} “unicode percent ∗”]

&∗

[&x →^{name} “

\&#1.”]

[&x →^{tex} “&#1.”]

[&x →^{pyk} “unicode ampersand ∗”]

’∗

[’x →^{name} “

\mbox {’}#1.”]

[’x →^{tex} “’#1.”]

[’x →^{pyk} “unicode apostrophe ∗”]

(∗

[(x →^{tex} “(#1.”]

[(x →^{pyk} “unicode left parenthesis ∗”]

)∗

[)x →^{tex} “)#1.”]

[)x →^{pyk} “unicode right parenthesis ∗”]

∗∗

[∗x →^{name} “

{∗}#1.”]

[∗x →^{tex} “∗#1.”]

[∗x →^{pyk} “unicode asterisk ∗”]

+∗

[+x →^{name} “

{+}#1.”]

[+x →^{tex} “+#1.”]

[+x →^{pyk} “unicode plus sign ∗”]

, ∗

[, x →^{tex} “, #1.”]

[, x →^{pyk} “unicode comma ∗”]

-∗

[-x →^{name} “

\mbox{-}#1.”]

[-x →^{tex} “-#1.”]

[-x →^{pyk} “unicode hyphen ∗”]

.∗

[.x →^{tex} “.#1.”]

[.x →^{pyk} “unicode period ∗”]

/∗

[/x →^{tex} “/#1.”]

[/x →^{pyk} “unicode slash ∗”]

0∗

[0x →^{tex} “0#1.”]

[0x →^{pyk} “unicode zero ∗”]

1∗

[1x →^{tex} “1#1.”]

[1x →^{pyk} “unicode one ∗”]

2∗

[2x →^{tex} “2#1.”]

[2x →^{pyk} “unicode two ∗”]

3∗

[3x →^{tex} “3#1.”]

[3x →^{pyk} “unicode three ∗”]

4∗

[4x →^{tex} “4#1.”]

[4x →^{pyk} “unicode four ∗”]

5∗

[5x →^{tex} “5#1.”]

[5x →^{pyk} “unicode five ∗”]

6∗

[6x →^{tex} “6#1.”]

[6x →^{pyk} “unicode six ∗”]

7∗

[7x →^{tex} “7#1.”]

[7x →^{pyk} “unicode seven ∗”]

8∗

[8x →^{tex} “8#1.”]

[8x →^{pyk} “unicode eight ∗”]

9∗

[9x →^{tex} “9#1.”]

[9x →^{pyk} “unicode nine ∗”]

:∗

[:x →^{name} “

{:}#1.”]

[:x →^{tex} “:#1.”]

[:x →^{pyk} “unicode colon ∗”]

; ∗

[; x →^{tex} “; #1.”]

[; x →^{pyk} “unicode semicolon ∗”]

<∗

[<x →^{name} “

{<}#1.”]

[<x →^{tex} “<#1.”]

[<x →^{pyk} “unicode less than ∗”]

=∗

[=x →^{name} “

{=}#1.”]

[=x →^{tex} “=#1.”]

[=x →^{pyk} “unicode equal sign ∗”]

>∗

[>x →^{name} “

{>}#1.”]

[>x →^{tex} “>#1.”]

[>x →^{pyk} “unicode greater than ∗”]

?∗

[?x →^{tex} “?#1.”]

[?x →^{pyk} “unicode question mark ∗”]

@∗

[@x →^{tex} “@#1.”]

[@x →^{pyk} “unicode commercial at ∗”]

A∗

[Ax →^{tex} “A#1.”]

[Ax →^{pyk} “unicode capital a ∗”]

B∗

[Bx →^{tex} “B#1.”]

[Bx →^{pyk} “unicode capital b ∗”]

C∗

[Cx →^{tex} “C#1.”]

[Cx →^{pyk} “unicode capital c ∗”]

D∗

[Dx →^{tex} “D#1.”]

[Dx →^{pyk} “unicode capital d ∗”]

E∗

[Ex →^{tex} “E#1.”]

[Ex →^{pyk} “unicode capital e ∗”]

F∗

[Fx →^{tex} “F#1.”]

[Fx →^{pyk} “unicode capital f ∗”]

G∗

[Gx →^{tex} “G#1.”]

[Gx →^{pyk} “unicode capital g ∗”]

H∗

[Hx →^{tex} “H#1.”]

[Hx →^{pyk} “unicode capital h ∗”]

I∗

[Ix →^{tex} “I#1.”]

[Ix →^{pyk} “unicode capital i ∗”]

J∗

[Jx →^{tex} “J#1.”]

[Jx →^{pyk} “unicode capital j ∗”]

K∗

[Kx →^{tex} “K#1.”]

[Kx →^{pyk} “unicode capital k ∗”]

L∗

[Lx →^{tex} “L#1.”]

[Lx →^{pyk} “unicode capital l ∗”]

M∗

[Mx →^{tex} “M#1.”]

[Mx →^{pyk} “unicode capital m ∗”]

N∗

[Nx →^{tex} “N#1.”]

[Nx →^{pyk} “unicode capital n ∗”]

O∗

[Ox →^{tex} “O#1.”]

[Ox →^{pyk} “unicode capital o ∗”]

P∗

[Px →^{tex} “P#1.”]

[Px →^{pyk} “unicode capital p ∗”]

Q∗

[Qx →^{tex} “Q#1.”]

[Qx →^{pyk} “unicode capital q ∗”]

R∗

[Rx →^{tex} “R#1.”]

[Rx →^{pyk} “unicode capital r ∗”]

S∗

[Sx →^{tex} “S#1.”]

[Sx →^{pyk} “unicode capital s ∗”]

T∗

[Tx →^{tex} “T#1.”]

[Tx →^{pyk} “unicode capital t ∗”]

U∗

[Ux →^{tex} “U#1.”]

[Ux →^{pyk} “unicode capital u ∗”]

V∗

[Vx →^{tex} “V#1.”]

[Vx →^{pyk} “unicode capital v ∗”]

W∗

[Wx →^{tex} “W#1.”]

[Wx →^{pyk} “unicode capital w ∗”]

X∗

[Xx →^{tex} “X#1.”]

[Xx →^{pyk} “unicode capital x ∗”]

Y∗

[Yx →^{tex} “Y#1.”]

[Yx →^{pyk} “unicode capital y ∗”]

Z∗

[Zx →^{tex} “Z#1.”]

[Zx →^{pyk} “unicode capital z ∗”]

[∗

[[x →^{tex} “[#1.”]

[[x →^{pyk} “unicode left bracket ∗”]

\∗

[\x →^{name} “

\mbox {$\backslash $}#1.”]

[\x →^{tex} “\#1.”]

[\x →^{pyk} “unicode backslash ∗”]

]∗

[]x →^{tex} “]#1.”]

[]x →^{pyk} “unicode right bracket ∗”]

ˆ ∗

[ˆ x →^{name} “

{\char94}#1.”]

[ˆ x →^{tex} “ˆ #1.”]

[ˆ x →^{pyk} “unicode circumflex ∗”]

∗

[ x →^{name} “

\ #1.”]

[ x →^{tex} “ #1.”]

[ x →^{pyk} “unicode underscore ∗”]

‘∗

[‘x →^{name} “

\mbox {‘}#1.”]

[‘x →^{tex} “‘#1.”]

[‘x →^{pyk} “unicode grave accent ∗”]

a∗

[ax →^{tex} “a#1.”]

[ax →^{pyk} “unicode small a ∗”]

b∗

[bx →^{tex} “b#1.”]

[bx →^{pyk} “unicode small b ∗”]

c∗

[cx →^{tex} “c#1.”]

[cx →^{pyk} “unicode small c ∗”]

d∗

[dx →^{tex} “d#1.”]

[dx →^{pyk} “unicode small d ∗”]

e∗

[ex →^{tex} “e#1.”]

[ex →^{pyk} “unicode small e ∗”]

f∗

[fx →^{tex} “f#1.”]

[fx →^{pyk} “unicode small f ∗”]

g∗

[gx →^{tex} “g#1.”]

[gx →^{pyk} “unicode small g ∗”]

h∗

[hx →^{tex} “h#1.”]

[hx →^{pyk} “unicode small h ∗”]

i∗

[ix →^{tex} “i#1.”]

[ix →^{pyk} “unicode small i ∗”]

j∗

[jx →^{tex} “j#1.”]

[jx →^{pyk} “unicode small j ∗”]

k∗

[kx →^{tex} “k#1.”]

[kx →^{pyk} “unicode small k ∗”]

l∗

[lx →^{tex} “l#1.”]

[lx →^{pyk} “unicode small l ∗”]

m∗

[mx →^{tex} “m#1.”]

[mx →^{pyk} “unicode small m ∗”]

n∗

[nx →^{tex} “n#1.”]

[nx →^{pyk} “unicode small n ∗”]

o∗

[ox →^{tex} “o#1.”]

[ox →^{pyk} “unicode small o ∗”]

p∗

[px →^{tex} “p#1.”]

[px →^{pyk} “unicode small p ∗”]

q∗

[qx →^{tex} “q#1.”]

[qx →^{pyk} “unicode small q ∗”]

r∗

[rx →^{tex} “r#1.”]

[rx →^{pyk} “unicode small r ∗”]

s∗

[sx →^{tex} “s#1.”]

[sx →^{pyk} “unicode small s ∗”]

t∗

[tx →^{tex} “t#1.”]

[tx →^{pyk} “unicode small t ∗”]

u∗

[ux →^{tex} “u#1.”]

[ux →^{pyk} “unicode small u ∗”]

v∗

[vx →^{tex} “v#1.”]

[vx →^{pyk} “unicode small v ∗”]

w∗

[wx →^{tex} “w#1.”]

[wx →^{pyk} “unicode small w ∗”]

x∗

[xx →^{tex} “x#1.”]

[xx →^{pyk} “unicode small x ∗”]

y∗

[yx →^{tex} “y#1.”]

[yx →^{pyk} “unicode small y ∗”]

z∗

[zx →^{tex} “z#1.”]

[zx →^{pyk} “unicode small z ∗”]

{∗

[{x →^{name} “

\{#1.”]

[{x →^{tex} “{#1.”]

[{x →^{pyk} “unicode left brace ∗”]

|∗

[|x →^{tex} “|#1.”]

[|x →^{pyk} “unicode vertical line ∗”]

}∗

[}x →^{name} “

\}#1.”]

[}x →^{tex} “}#1.”]

[}x →^{pyk} “unicode right brace ∗”]

˜ ∗

[˜ x →^{name} “

\char126 #1.”]

[˜ x →^{tex} “˜ #1.”]

[˜ x →^{pyk} “unicode tilde ∗”]

⊥

[⊥ ⇒^{val} (λx. [ x ’ x ] )^{I} ’ (λx. [ x ’ x ] )^{I}]

[⊥ →^{tex} “

\bot ”] [⊥ →^{pyk} “bottom”]

f(∗)

[f(x) →^{val} if(x, T, f(x ’ T))]

[f(∗) →^{tex} “

f(#1. )”]

[f(∗) →^{pyk} “function f of ∗ end function”]

(∗)^{I}

[(x)^{I} →^{val} x]

[(∗)^{I} →^{tex} “

(#1. ){}ˆ {I} ”]

[(∗)^{I} →^{pyk} “identity ∗ end identity”]

F

[F ⇒^{val} T ˙. . T]

[F →^{tex} “

\mathsf {F}”]

[F →^{pyk} “false”]

\underline{0}

[\underline{0} →^{val} T]

[\underline{0} →^{tex} “

\underline {0}”]

[\underline{0} →^{pyk} “untagged zero”]

\underline{1}

[\underline{1} →^{val} F \underline{+2∗} \underline{0}]

[\underline{1} →^{tex} “

\underline {1}”] [\underline{1} →^{pyk} “untagged one”]

\underline{2}

[\underline{2} →^{val} T \underline{+2∗} \underline{1}]

[\underline{2} →^{tex} “

\underline {2}”] [\underline{2} →^{pyk} “untagged two”]

\underline{3}

[\underline{3} →^{val} F \underline{+2∗} \underline{1}]

[\underline{3} →^{tex} “

\underline {3}”] [\underline{3} →^{pyk} “untagged three”]

\underline{4}

[\underline{4} →^{val} T \underline{+2∗} \underline{2}]

[\underline{4} →^{tex} “

\underline {4}”] [\underline{4} →^{pyk} “untagged four”]

\underline{5}

[\underline{5} →^{val} F \underline{+2∗} \underline{2}]

[\underline{5} →^{tex} “

\underline {5}”] [\underline{5} →^{pyk} “untagged five”]

\underline{6}

[\underline{6} →^{val} T \underline{+2∗} \underline{3}]

[\underline{6} →^{tex} “

\underline {6}”] [\underline{6} →^{pyk} “untagged six”]

\underline{7}

[\underline{7} →^{val} F \underline{+2∗} \underline{3}]

[\underline{7} →^{tex} “

\underline {7}”] [\underline{7} →^{pyk} “untagged seven”]

\underline{8}

[\underline{8} →^{val} T \underline{+2∗} \underline{4}]

[\underline{8} →^{tex} “

\underline {8}”] [\underline{8} →^{pyk} “untagged eight”]

\underline{9}

[\underline{9} →^{val} F \underline{+2∗} \underline{4}]

[\underline{9} →^{tex} “

\underline {9}”] [\underline{9} →^{pyk} “untagged nine”]

0

[0 ⇒^{val} T ˙. . T]

[0 →^{tex} “

0”]

[0 →^{pyk} “zero”]

1

[1 →^{val} F +2∗ 0]

[1 →^{tex} “

1”]

[1 →^{pyk} “one”]

2

[2 →^{val} T +2∗ 1]

[2 →^{tex} “

2”]

[2 →^{pyk} “two”]

3

[3 →^{val} F +2∗ 1]

[3 →^{tex} “

3”]

[3 →^{pyk} “three”]

4

[4 →^{val} T +2∗ 2]

[4 →^{tex} “

4”]

[4 →^{pyk} “four”]

[5 →^{val} F +2∗ 2]

[5 →^{tex} “

5”]

[5 →^{pyk} “five”]

6

[6 →^{val} T +2∗ 3]

[6 →^{tex} “

6”]

[6 →^{pyk} “six”]

7

[7 →^{val} F +2∗ 3]

[7 →^{tex} “

7”] [7 →^{pyk} “seven”]

8

[8 →^{val} T +2∗ 4]

[8 →^{tex} “

8”] [8 →^{pyk} “eight”]

9

[9 →^{val} F +2∗ 4]

[9 →^{tex} “

9”]

[9 →^{pyk} “nine”]

a

[a →^{tex} “

\mathsf {a}”] [a →^{pyk} “var a”]

b

[b →^{tex} “

\mathsf {b}”] [b →^{pyk} “var b”]

c

[c →^{tex} “

\mathsf {c}”] [c →^{pyk} “var c”]

d

[d →^{tex} “

\mathsf {d}”] [d →^{pyk} “var d”]

e

[e →^{tex} “

\mathsf {e}”] [e →^{pyk} “var e”]

f

[f →^{tex} “

\mathsf {f}”] [f →^{pyk} “var f”]

g

[g →^{tex} “

\mathsf {g}”]

[g →^{pyk} “var g”]

h

[h →^{tex} “

\mathsf {h}”]

[h →^{pyk} “var h”]

i

[i →^{tex} “

\mathsf {i}”]

[i →^{pyk} “var i”]

j

[j →^{tex} “

\mathsf {j}”]

[j →^{pyk} “var j”]

k

[k →^{tex} “

\mathsf {k}”]

[k →^{pyk} “var k”]

l

[l →^{tex} “

\mathsf {l}”]

[l →^{pyk} “var l”]

[m →^{tex} “

\mathsf {m}”]

[m →^{pyk} “var m”]

n

[n →^{tex} “

\mathsf {n}”]

[n →^{pyk} “var n”]

o

[o →^{tex} “

\mathsf {o}”]

[o →^{pyk} “var o”]

p

[p →^{tex} “

\mathsf {p}”]

[p →^{pyk} “var p”]

q

[q →^{tex} “

\mathsf {q}”]

[q →^{pyk} “var q”]

r

[r →^{tex} “

\mathsf {r}”]

[r →^{pyk} “var r”]

s

[s →^{tex} “

\mathsf {s}”]

[s →^{pyk} “var s”]

t

[t →^{tex} “

\mathsf {t}”]

[t →^{pyk} “var t”]

u

[u →^{tex} “

\mathsf {u}”]

[u →^{pyk} “var u”]

v

[v →^{tex} “

\mathsf {v}”]

[v →^{pyk} “var v”]

w

[w →^{tex} “

\mathsf {w}”]

[w →^{pyk} “var w”]

(∗)^{M}

[(x)^{M} →^{val} x^{M}]

[(∗)^{M} →^{tex} “

(#1.

)ˆ M”]

[(∗)^{M} →^{pyk} “tagged parenthesis ∗ end tagged”]

If(∗, ∗, ∗)

[If(x, y, z) ⇒^{val} if(x^{M}, y^{M}, z^{M})]

[If(∗, ∗, ∗) →^{tex} “

\mathrm {If}(#1. , \linebreak [0]#2. , \linebreak [0]#3. )”]

[If(∗, ∗, ∗) →^{pyk} “tagged if ∗ then ∗ else ∗ end if”]

array{∗} ∗ end array

[array{∗} ∗ end array →^{name} “\mathrm {array}\{#1. \}#2. \mathrm {end\ array}”]

[array{∗} ∗ end array →^{tex} “ \begin {array}{#1. }#2. \end {array}”]

[array{∗} ∗ end array →^{pyk} “array ∗ is ∗ end array”]

l

[l →^{tex} “

l”]

[l →^{pyk} “left”]

c

[c →^{tex} “

c”]

[c →^{pyk} “center”]

r

[r →^{tex} “

r”]

[r →^{pyk} “right”]

empty

[empty →^{name} “ \mathrm {empty}”]

[empty →^{tex} “ ”]

[empty →^{pyk} “empty”]

⟨∗ | ∗:= ∗⟩

[⟨∗ | ∗:= ∗⟩ →^{tex} “

\langle #1. \, {|}#2. {:=}\, #3. \rangle ”]

[⟨∗ | ∗:= ∗⟩ →^{pyk} “substitute ∗ set ∗ to ∗ end substitute”]

M(∗)

[M(x) →^{val} (\underline{0} \underline{˙. .} [ \underline{1} \underline{˙. .} T ] )^{I} ˙. . x]

[M(∗) →^{tex} “

{\cal M}(#1. )”]

[M(∗) →^{pyk} “map tag ∗ end tag”]

Ũ(∗)

[Ũ(x) →^{val} if(x^{d}, x, x^{T})]

[Ũ(∗) →^{tex} “

\tilde {{\cal U}}(#1. )”]

[Ũ(∗) →^{pyk} “raw map untag ∗ end untag”]

U(∗)

[U(x) →^{val} Ũ(x^{M})]

[U(∗) →^{tex} “

{\cal U}(#1. )”]

[U(∗) →^{pyk} “map untag ∗ end untag”]

U^{M}(∗)

[U^{M}(x) ⇒^{val} U(x)^{M}]

[U^{M}(∗) →^{tex} “

{\cal U}ˆ M(#1. )”]

[U^{M}(∗) →^{pyk} “normalizing untag ∗ end untag”]

apply(∗, ∗)

[apply(f, x) ⇒^{val} apply_{1}(f^{M}, x^{M})]

[apply(∗, ∗) →^{tex} “ \mathbf {apply}(#1. , #2. )”]

[apply(∗, ∗) →^{pyk} “apply ∗ to ∗ end apply”]

apply_{1}(∗, ∗)

[apply_{1}(f, x) →^{val} f^{d} \{ \begin{matrix}If(x^{d}, f, f) \\ If(x^{d}, M(f^{T} ’ x), M(f^{T} ’ (x^{T})^{I})) \end{matrix} ] [apply_{1}(∗, ∗) →^{tex} “ \mathbf {apply} 1(#1. , #2. )”]

[apply_{1}(∗, ∗) →^{pyk} “apply one ∗ to ∗ end apply”]

identifier(∗)

[identifier(x) →^{val} If(x^{t}, 0, identifier_{1}(x^{i}, identifier(x^{1})))]

[identifier(x) →^{tex} “ identifier( #1. )”]

[identifier(x) →^{pyk} “identifier ∗ end identifier”]

identifier_{1}(∗, ∗)

[identifier_{1}(x, y) →^{val} If(x^{6}, y, x^{0} +2∗ [ x^{1} +2∗ [ x^{2} +2∗ [ x^{3} +2∗ [ x^{4} +2∗ [ x^{5} +2∗ [ F +2∗ [ T +2∗ y ] ] ] ] ] ] ] )]

[identifier_{1}(x, y) →^{tex} “ identifier {1}( #1. , #2. )”]

[identifier_{1}(x, y) →^{pyk} “identifier one ∗ plus id ∗ end identifier”]

array-plus(∗, ∗)

[array-plus(x, y) →^{val} x^{a} \{ \begin{matrix}y^{a} \{ \begin{matrix}T \\ y^{h}^{c} \{ \begin{matrix}y \\ x : : y \end{matrix} \end{matrix} \\ y^{a} \{ \begin{matrix}x^{h}^{c} \{ \begin{matrix}x \\ x : : y \end{matrix} \\ x : : y \end{matrix} \end{matrix} ]

[array-plus(x, y) →^{tex} “ array\mbox{-}\linebreak[0]plus( #1. , #2. )”]

[array-plus(x, y) →^{pyk} “array plus ∗ and ∗ end plus”]

array-remove(∗, ∗, ∗)

[array-remove(i, a, l) →^{val} [ [ i ] ! [ l! [ a^{a} ] ] ]

\{ \begin{matrix}T \\ a^{h}^{c} \{ \begin{matrix}[ a^{h} ≈ i ] \{ \begin{matrix}T \\ a \end{matrix} \\ bit(l, i) \{ \begin{matrix}array-plus(array-remove(i, a^{h}, l + 1), a^{t}) \\ array-plus(a^{h}, array-remove(i, a^{t}, l + 1)) \end{matrix} \end{matrix} \end{matrix} ]

[array-remove(i, a, l) →^{tex} “ array\mbox{-}\linebreak[0]remove( #1. , #2. , #3. )”]

[array-remove(i, a, l) →^{pyk} “array remove ∗ array ∗ level ∗ end remove”]

array-put(∗, ∗, ∗, ∗)

[array-put(i, v, a, l) →^{val} [ [

l ] ! [ a^{a} ] ] \{ \begin{matrix}i : : v \\ a^{h}^{c} \{ \begin{matrix}[ a^{h} ≈ i ] \{ \begin{matrix}i : : v \\ array-add(i, v, a^{h}, a^{t}, l) \end{matrix} \\ bit(l, i) \{ \begin{matrix}array-put(i, v, a^{h}, l + 1) : : [ a^{t} ] \\ a^{h} : : array-put(i, v, a^{t}, l + 1) \end{matrix} \end{matrix} \end{matrix} ]

[array-put(i, v, a, l) →^{tex} “ array\mbox{-}\linebreak[0]put( #1. , #2. , #3. , #4. )”]

[array-put(i, v, a, l) →^{pyk} “array put ∗ value ∗ array ∗ level ∗ end put”]

array-add(∗, ∗, ∗, ∗, ∗)

[array-add(i, v, i′, v′, l) →^{val} [

bit(l, i) ] \{ \begin{matrix}bit(l, i′) \{ \begin{matrix}array-add(i, v, i′, v′, l + 1) : : T \\ (i : : v)^{M} : : (i′ : : [ v′ ] )^{M} \end{matrix} \\ bit(l, i′) \{ \begin{matrix}(i′ : : [ v′ ] )^{M} : : (i : : v)^{M} \\ T : : array-add(i, v, i′, v′, l + 1) \end{matrix} \end{matrix} ]

[array-add(i, v, i′, v′, l) →^{tex} “ array\mbox{-}\linebreak[0]add( #1. , #2. , #3. , #4. , #5. )”]

[array-add(i, v, i′, v′, l) →^{pyk} “array add ∗ value ∗ index ∗ value ∗ level ∗ end add”]

bit(∗, ∗)

[bit(x, y) →^{val} If(x^{c} ∧ [ y^{c} ] , bit_{1}(x, y), T)]

[bit(x, y) →^{tex} “ bit( #1. , #2. )”]

[bit(x, y) →^{pyk} “bit ∗ of ∗ end bit”]

bit_{1}(∗, ∗)

[bit_{1}(x, y) →^{val} If(x^{s}, y^{h}, bit(x − 1, y^{t}))]

[bit_{1}(x, y) →^{tex} “ bit 1( #1. , #2. )”]

[bit_{1}(x, y) →^{pyk} “bit one ∗ of ∗ end bit”]

rack

[rack →^{val} base[base[0]]]

[rack →^{tex} “

rack”]

[rack →^{pyk} “example rack”]

"vector"

["vector" →^{val} identifier(⌈“vector”⌉)] ["vector" →^{tex} “ \mbox {\tt \char34}\mathrm {vector}\mbox {\tt \char34}”] ["vector" →^{pyk} “vector hook”]

"bibliography"

["bibliography" →^{val} identifier(⌈“bibliography”⌉)] ["bibliography" →^{tex} “ \mbox {\tt \char34}\mathrm {bibliography}\mbox {\tt \char34}”] ["bibliography" →^{pyk} “bibliography hook”]

"dictionary"

["dictionary" →^{val} identifier(⌈“dictionary”⌉)] ["dictionary" →^{tex} “ \mbox {\tt \char34}\mathrm {dictionary}\mbox {\tt \char34}”] ["dictionary" →^{pyk} “dictionary hook”]

"body"

["body" →^{val} identifier(⌈“body”⌉)]

["body" →^{tex} “

\mbox {\tt \char34}\mathrm {body}\mbox {\tt \char34}”] ["body" →^{pyk} “body hook”]

"codex"

["codex" →^{val} identifier(⌈“codex”⌉)] ["codex" →^{tex} “ \mbox {\tt \char34}\mathrm {codex}\mbox {\tt \char34}”] ["codex" →^{pyk} “codex hook”]

"expansion"

["expansion" →^{val} identifier(⌈“expansion”⌉)] ["expansion" →^{tex} “ \mbox {\tt \char34}\mathrm {expansion}\mbox {\tt \char34}”] ["expansion" →^{pyk} “expansion hook”]

"code"

["code" →^{val} identifier(⌈“code”⌉)]

["code" →^{tex} “

\mbox {\tt \char34}\mathrm {code}\mbox {\tt \char34}”] ["code" →^{pyk} “code hook”]

"cache"

["cache" →^{val} identifier(⌈“cache”⌉)] ["cache" →^{tex} “ \mbox {\tt \char34}\mathrm {cache}\mbox {\tt \char34}”] ["cache" →^{pyk} “cache hook”]

"diagnose"

["diagnose" →^{val} identifier(⌈“diagnose”⌉)] ["diagnose" →^{tex} “ \mbox {\tt \char34}\mathrm {diagnose}\mbox {\tt \char34}”] ["diagnose" →^{pyk} “diagnose hook”]

"pyk"

["pyk" →^{val} identifier(⌈“pyk”⌉)]

["pyk" →^{tex} “

\mbox {\tt \char34}\mathrm {pyk}\mbox {\tt \char34}”]

["pyk" →^{pyk} “pyk aspect”]

"tex"

["tex" →^{val} identifier(⌈“tex”⌉)]

["tex" →^{tex} “

\mbox {\tt \char34}\mathrm {tex}\mbox {\tt \char34}”]

["tex" →^{pyk} “tex aspect”]

"texname"

["texname" →^{val} identifier(⌈“texname”⌉)]

["texname" →^{tex} “ \mbox {\tt \char34}\mathrm {texname}\mbox {\tt \char34}”]

["texname" →^{pyk} “texname aspect”]

"value"

["value" →^{val} identifier(⌈“value”⌉)]

["value" →^{tex} “ \mbox {\tt \char34}\mathrm {value}\mbox {\tt \char34}”]

["value" →^{pyk} “value aspect”]

"message"

["message" →^{val} identifier(⌈“message”⌉)]

["message" →^{tex} “ \mbox {\tt \char34}\mathrm {message}\mbox {\tt \char34}”]

["message" →^{pyk} “message aspect”]

"macro"

["macro" →^{val} identifier(⌈“macro”⌉)] ["macro" →^{tex} “ \mbox {\tt \char34}\mathrm {macro}\mbox {\tt \char34}”] ["macro" →^{pyk} “macro aspect”]

"definition"

["definition" →^{val} identifier(⌈“definition”⌉)] ["definition" →^{tex} “ \mbox {\tt \char34}\mathrm {definition}\mbox {\tt \char34}”] ["definition" →^{pyk} “definition aspect”]

"unpack"

["unpack" →^{val} identifier(⌈“unpack”⌉)] ["unpack" →^{tex} “ \mbox {\tt \char34}\mathrm {unpack}\mbox {\tt \char34}”] ["unpack" →^{pyk} “unpack aspect”]

"claim"

["claim" →^{val} identifier(⌈“claim”⌉)] ["claim" →^{tex} “ \mbox {\tt \char34}\mathrm {claim}\mbox {\tt \char34}”] ["claim" →^{pyk} “claim aspect”]

"priority"

["priority" →^{val} identifier(⌈“priority”⌉)] ["priority" →^{tex} “ \mbox {\tt \char34}\mathrm {priority}\mbox {\tt \char34}”] ["priority" →^{pyk} “priority aspect”]

"lambda"

["lambda" →^{val} identifier(⌈“lambda”⌉)] ["lambda" →^{tex} “ \mbox {\tt \char34}\mathrm {lambda}\mbox {\tt \char34}”] ["lambda" →^{pyk} “lambda identifier”]

"apply"

["apply" →^{val} identifier(⌈“apply”⌉)] ["apply" →^{tex} “ \mbox {\tt \char34}\mathrm {apply}\mbox {\tt \char34}”] ["apply" →^{pyk} “apply identifier”]

"true"

["true" →^{val} identifier(⌈“true”⌉)]

["true" →^{tex} “

\mbox {\tt \char34}\mathrm {true}\mbox {\tt \char34}”] ["true" →^{pyk} “true identifier”]

"if"

["if" →^{val} identifier(⌈“if”⌉)]

["if" →^{tex} “

\mbox {\tt \char34}\mathrm {if}\mbox {\tt \char34}”] ["if" →^{pyk} “if identifier”]

"quote"

["quote" →^{val} identifier(⌈“quote”⌉)] ["quote" →^{tex} “ \mbox {\tt \char34}\mathrm {quote}\mbox {\tt \char34}”] ["quote" →^{pyk} “quote identifier”]

"proclaim"

["proclaim" →^{val} identifier(⌈“proclaim”⌉)] ["proclaim" →^{tex} “ \mbox {\tt \char34}\mathrm {proclaim}\mbox {\tt \char34}”] ["proclaim" →^{pyk} “proclaim identifier”]

"define"

["define" →^{val} identifier(⌈“define”⌉)] ["define" →^{tex} “ \mbox {\tt \char34}\mathrm {define}\mbox {\tt \char34}”] ["define" →^{pyk} “define identifier”]

"introduce"

["introduce" →^{val} identifier(⌈“introduce”⌉)] ["introduce" →^{tex} “ \mbox {\tt \char34}\mathrm {introduce}\mbox {\tt \char34}”] ["introduce" →^{pyk} “introduce identifier”]

"hide"

["hide" →^{val} identifier(⌈“hide”⌉)]

["hide" →^{tex} “

\mbox {\tt \char34}\mathrm {hide}\mbox {\tt \char34}”] ["hide" →^{pyk} “hide identifier”]

"pre"

["pre" →^{val} identifier(⌈“pre”⌉)]

["pre" →^{tex} “

\mbox {\tt \char34}\mathrm {pre}\mbox {\tt \char34}”] ["pre" →^{pyk} “pre identifier”]

"post"

["post" →^{val} identifier(⌈“post”⌉)]

["post" →^{tex} “

\mbox {\tt \char34}\mathrm {post}\mbox {\tt \char34}”]

["post" →^{pyk} “post identifier”]

E(∗, ∗, ∗)

[E(t, s, c) →^{val} E_{2}(t, t^{r}, t^{i}, s, c)]

[E(∗, ∗, ∗) →^{tex} “

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

[E(∗, ∗, ∗) →^{pyk} “eval ∗ stack ∗ cache ∗ end eval”]

E_{2}(∗, ∗, ∗, ∗, ∗)

[E_{2}(t, r, i, s, c) →^{val} i^{s} \{ \begin{matrix}t! [ s!If(r ≈ [ c[0] ] , c, c[c[0]]["cache"][r]) ] \\ E_{3}(t, c[r]["code"][i], s, c) \end{matrix} ]

[E_{2}(∗, ∗, ∗, ∗, ∗) →^{tex} “

{\cal E} 2(#1. , #2. , #3. , #4. , #5. )”]

[E_{2}(∗, ∗, ∗, ∗, ∗) →^{pyk} “eval two ∗ ref ∗ id ∗ stack ∗ cache ∗ end eval”]

E_{3}(∗, ∗, ∗, ∗)

[E_{3}(t, f, s, c) →^{val} f^{c} \{ \begin{matrix}f^{s} \{ \begin{matrix}abstract(t^{1}, t^{2}, s, c) \\ c! [ s! [ t^{1} ] ] \end{matrix} \\ f \{ \begin{matrix}c!lookup(t, s, T) \\ E_{4}(f, t^{t}, s, c) \end{matrix} \end{matrix} ]

[E_{3}(∗, ∗, ∗, ∗) →^{tex} “

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

[E_{3}(∗, ∗, ∗, ∗) →^{pyk} “eval three ∗ function ∗ stack ∗ cache ∗ end eval”]

E_{4}(∗, ∗, ∗, ∗)

[E_{4}(f, a, s, c) →^{val} If(a, s! [ c!f ] , E_{4}(apply(f, E(a^{h}, s, c)), a^{t}, s, c))]

[E_{4}(∗, ∗, ∗, ∗) →^{tex} “

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

[E_{4}(∗, ∗, ∗, ∗) →^{pyk} “eval four ∗ arguments ∗ stack ∗ cache ∗ end eval”]

lookup(∗, ∗, ∗)

[lookup(v, s, d) →^{val} v! [ d!If(s, d, If(v =^{t} [ s^{h}^{h} ] , s^{h}^{t}, lookup(v, s^{t}, d))) ] ]

[lookup(∗, ∗, ∗) →^{tex} “ \mathbf {lookup}(#1. , #2. , #3. )”]

[lookup(∗, ∗, ∗) →^{pyk} “lookup ∗ stack ∗ default ∗ end lookup”]

abstract(∗, ∗, ∗, ∗)

[abstract(v, t, s, c) →^{val} v! [ t! [ s! [ c!Λλx.E(t, (v : : x)^{M} : : s, c) ] ] ] ]

[abstract(∗, ∗, ∗, ∗) →^{tex} “ \mathbf {abstract}(#1. , #2. , #3.

, #4. )”]

[abstract(∗, ∗, ∗, ∗) →^{pyk} “abstract ∗ term ∗ stack ∗ cache ∗ end abstract”]

⌈∗⌉

Predef: quote

[⌈∗⌉ →^{tex} “

\lceil #1. \rceil ”]

[⌈∗⌉ →^{pyk} “quote ∗ end quote”]

M(∗, ∗, ∗)

[M(t, s, c) →^{val} s! [ c!If(t^{i}^{s}, t, M_{2}(t, aspect("macro", t, c), s, c)) ] ]

[M(∗, ∗, ∗) →^{tex} “

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

[M(∗, ∗, ∗) →^{pyk} “expand ∗ state ∗ cache ∗ end expand”]

M_{2}(∗, ∗, ∗, ∗)

[M_{2}(t, d, s, c) →^{val} d \{ \begin{matrix}t^{h} : : M^{∗}(t^{t}, s, c) \\ U^{M}( [ [ E(d^{3}, T, c) ‘ t ] ‘ s ] ‘ c) \end{matrix} ]

[M_{2}(∗, ∗, ∗, ∗) →^{tex} “

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

[M_{2}(∗, ∗, ∗, ∗) →^{pyk} “expand two ∗ definition ∗ state ∗ cache ∗ end expand”]

M^{∗}(∗, ∗, ∗)

[M^{∗}(a, s, c) →^{val} s! [ c!If(a, T, M(a^{h}, s, c) : : M^{∗}(a^{t}, s, c)) ] ]

[M^{∗}(∗, ∗, ∗) →^{tex} “

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

[M^{∗}(∗, ∗, ∗) →^{pyk} “expand list ∗ state ∗ cache ∗ end expand”]

macro

Predef: macro

[macro →^{tex} “ \mathrm {macro}”]

[macro →^{pyk} “macro”]

s_{0}

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

[s_{0} →^{tex} “

s 0”]

[s_{0} →^{pyk} “macro state”]

zip(∗, ∗)

[zip(p, a) →^{val} a!If(p, T, (p^{h} : : [ a^{h} ] )^{M} : : zip(p^{t}, a^{t}))]

[zip(∗, ∗) →^{tex} “

\mathbf {zip}(#1. , #2. )”]

[zip(∗, ∗) →^{pyk} “zip ∗ with ∗ end zip”]

assoc_{1}(∗, ∗, ∗)

[assoc_{1}(a, d, i) →^{val} a^{a} \{ \begin{matrix}d! [ i!T ] \\ a^{h}^{c} \{ \begin{matrix}[ i ≈ [ a^{h} ] ] \{ \begin{matrix}d! [ a^{t} ] \\ d!T \end{matrix} \\ d^{h} \{ \begin{matrix}assoc_{1}(a^{h}, d^{t}, i) \\ assoc_{1}(a^{t}, d^{t}, i) \end{matrix} \end{matrix} \end{matrix} ]

[assoc_{1}(∗, ∗, ∗) →^{tex} “ \mathbf {assoc} 1(#1. , #2. , #3. )”]

[assoc_{1}(∗, ∗, ∗) →^{pyk} “assoc one ∗ address ∗ index ∗ end assoc”]

(∗)^{p}

[(x)^{p} →^{macro} λt.λs.λc. [ t^{1} ] ]

[(∗)^{p} →^{tex} “(#1.

)ˆ {\mathbf {p}}”]

[(∗)^{p} →^{pyk} “protect ∗ end protect”]

self

[self →^{macro} λt.λs.λc. [ (c[0] : : [ 0 : : [ t^{d} ] ] )^{I} : : T ] ]

[self →^{pyk} “self”]

[∗ ¨= ∗]

[[x ¨= y] →^{macro} λt.λs.λc.M̃_{3}(t)]

[[∗ ¨= ∗] →^{tex} “

[#1/tex name/tex. \mathrel {\ddot {=}}#2. ]”]

[[∗ ¨= ∗] →^{pyk} macrodefine ∗ as ∗ enddefine]

[∗ ˙= ∗]

[[x ˙= y] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x ˙= y] ¨= [(x)^{p} →^{val} y]]⌉)]

[[∗ ˙= ∗] →^{tex} “

[#1/tex name/tex. \mathrel {\dot {=}}#2. ]”]

[[∗ ˙= ∗] →^{pyk} “value define ∗ as ∗ end define”]

[∗ ´= ∗]

[[x ´= y] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x ´= y] ¨= [(x)^{p} ⇒^{val} y]]⌉)]

[[∗ ´= ∗] →^{tex} “

[#1/tex name/tex. \mathrel {\acute {=}}#2. ]”]

[[∗ ´= ∗] →^{pyk} “intro define ∗ as ∗ end define”]

[∗ =^{pyk} ∗]

[[x =^{pyk} y] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x =^{pyk} y] ¨= [(x)^{p} →^{pyk} y]]⌉)]

[[∗ =^{pyk} ∗] →^{tex} “

[#1/tex name/tex. \stackrel {\mathrm {pyk}}{=} #2/tex name. ]”]

[[∗ =^{pyk} ∗] →^{pyk} “pyk define ∗ as ∗ end define”]

[∗ =^{tex} ∗]

[[x =^{tex} y] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x =^{tex} y] ¨= [(x)^{p} →^{tex} y]]⌉)]

[[∗ =^{tex} ∗] →^{tex} “

[#1/tex name/tex. \stackrel {\mathrm {tex}}{=} #2/tex name. ]”]

[[∗ =^{tex} ∗] →^{pyk} “tex define ∗ as ∗ end define”]

[∗ =^{name} ∗]

[[x =^{name} y] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x =^{name} y] ¨= [(x)^{p} →^{name} y]]⌉)]

[[∗ =^{name} ∗] →^{tex} “

[#1/tex name/tex. \stackrel {\mathrm {name}}{=} #2/tex name. ]”]

[[∗ =^{name} ∗] →^{pyk} “tex name define ∗ as ∗ end define”]

Priority table[∗]

[Priority table[x] →^{name} “ \mathbf{Priority\ table} [ #1. ]”]

[Priority table[x] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Priority table[x] ¨= [self →^{prio} (x)^{p}]]⌉)]

[Priority table[x] →^{tex} “ \mathbf{Priority\ table} #1. \mathbf{End\ table}”]

[Priority table[x] →^{pyk} “priority table ∗ end table”]

M̃_{1}

[M̃_{1} →^{val} ⌈[x →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈d⌉)]⌉]

[M̃_{1} →^{tex} “

\tilde {{\cal M}} 1”]

[M̃_{1} →^{pyk} “macro define one”]

M̃_{2}(∗)

[M̃_{2}(t) →^{val} (⌈x⌉ : : [ t^{1} ] )^{M} : : [ (⌈d⌉ : : t)^{M} : : T ] ]

[M̃_{2}(∗) →^{tex} “

\tilde {{\cal M}} 2(#1. )”]

[M̃_{2}(∗) →^{pyk} “macro define two ∗ end define”]

M̃_{3}(∗)

[M̃_{3}(t) →^{val} Q̃(t, M̃_{1}, M̃_{2}(t))]

[M̃_{3}(∗) →^{tex} “

\tilde {{\cal M}} 3(#1. )”]

[M̃_{3}(∗) →^{pyk} “macro define three ∗ end define”]

M̃_{4}(∗, ∗, ∗, ∗)

[M̃_{4}(t, s, c, d) →^{val} M̃(Q̃(t, d^{2}, zip(d^{1}^{t}, t^{t})), s, c)]

[M̃_{4}(∗, ∗, ∗, ∗) →^{tex} “

\tilde {{\cal M}} 4(#1. , #2. , #3. , #4. )”]

[M̃_{4}(∗, ∗, ∗, ∗) →^{pyk} “macro define four ∗ state ∗ cache ∗ definition ∗ end define”]

M̃(∗, ∗, ∗)

[M̃(t, s, c) →^{val} U( [ [ s^{h} ‘ t ] ‘ s ] ‘ c)]

[M̃(∗, ∗, ∗) →^{tex} “

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

[M̃(∗, ∗, ∗) →^{pyk} “state expand ∗ state ∗ cache ∗ end expand”]

Q̃(∗, ∗, ∗)

[Q̃(r, t, s) →^{val} Q̃_{2}(r^{d}, t, s)]

[Q̃(∗, ∗, ∗) →^{tex} “

\tilde {{\cal Q}}(#1. , #2.

[Q̃(∗, ∗, ∗) →^{pyk} “quote expand ∗ term ∗ stack ∗ end expand”]

Q̃_{2}(∗, ∗, ∗)

[Q̃_{2}(r, t, s) →^{val} Q̃_{3}(r, t, s, lookup(t, s, T))]

[Q̃_{2}(∗, ∗, ∗) →^{tex} “

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

[Q̃_{2}(∗, ∗, ∗) →^{pyk} “quote expand two ∗ term ∗ stack ∗ end expand”]

Q̃_{3}(∗, ∗, ∗, ∗)

[Q̃_{3}(r, t, s, v) →^{val} v \{ \begin{matrix}(t^{r} : : [ t^{i} : : r ] )^{M} : : Q̃^{∗}(r, t^{t}, s) \\ r! [ t! [ s!v ] ] \end{matrix} ]

[Q̃_{3}(∗, ∗, ∗, ∗) →^{tex} “

\tilde {{\cal Q}} 3(#1. , #2. , #3. , #4. )”]

[Q̃_{3}(∗, ∗, ∗, ∗) →^{pyk} “quote expand three ∗ term ∗ stack ∗ value ∗ end expand”]

Q̃^{∗}(∗, ∗, ∗)

[Q̃^{∗}(r, t, s) →^{val} t \{ \begin{matrix}r! [ t! [ s!T ] ] \\ Q̃_{2}(r, t^{h}, s) : : Q̃^{∗}(r, t^{t}, s) \end{matrix} ]

[Q̃^{∗}(∗, ∗, ∗) →^{tex} “

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

[Q̃^{∗}(∗, ∗, ∗) →^{pyk} “quote expand star ∗ term ∗ stack ∗ end expand”]

(∗)

[(x) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(x) ¨= x]⌉)]

[(∗) →^{tex} “

(#1. )”]

[(∗) →^{pyk} “parenthesis ∗ end parenthesis”]

aspect(∗, ∗)

[aspect(a, c) →^{val} a^{c} \{ \begin{matrix}c[0][a] \\ c[a^{r}][a^{i}] \end{matrix} ]

[aspect(a, c) →^{tex} “ \mathbf{aspect}( #1. , #2. )”]

[aspect(a, c) →^{pyk} “aspect ∗ subcodex ∗ end aspect”]

aspect(∗, ∗, ∗)

[aspect(a, t, c) →^{val} aspect(a, c[t^{r}]["codex"][t^{r}][t^{i}])]

[aspect(∗, ∗, ∗) →^{tex} “ \mathbf{aspect}( #1. , #2. , #3. )”]

[aspect(a, t, c) →^{pyk} “aspect ∗ term ∗ cache ∗ end aspect”]

⟨∗⟩

[⟨x⟩ →^{macro} λt.λs.λc.M̃(tuple_{1}(t), s, c)]

[⟨∗⟩ →^{tex} “

\langle #1. \rangle ”]

[⟨x⟩ →^{pyk} “tuple ∗ end tuple”]

tuple_{1}(∗)

[tuple_{1}(t) →^{val} [ t^{1} =^{r} ⌈x, y⌉ ] \{ \begin{matrix}Q̃(t, ⌈x : : ⟨y⟩⌉, tuple_{2}(t^{1})) \\ Q̃(t, ⌈x : : T⌉, [ ⌈x⌉ : : [ t^{1} ] ] : : T) \end{matrix} ]

[tuple_{1}(∗) →^{tex} “ \mathbf {tuple} 1( #1. ) ”]

[tuple_{1}(t) →^{pyk} “tuple one ∗ end tuple”]

tuple_{2}(∗)

[tuple_{2}(t) →^{val} [ ⌈x⌉ : : [ t^{1} ] ] : : [ [ ⌈y⌉ : : [ t^{2} ] ] : : T ] ]

[tuple_{2}(∗) →^{tex} “ \mathbf {tuple} 2( #1. ) ”]

[tuple_{2}(t) →^{pyk} “tuple two ∗ end tuple”]

let_{2}(∗, ∗)

[let_{2}(f, y) →^{val} (y! [ f ’ y ] )^{I}]

[let_{2}(f, y) →^{tex} “ let 2( #1. , #2. )”]

[let_{2}(f, y) →^{pyk} “let two ∗ apply ∗ end let”]

let_{1}(∗, ∗)

[let_{1}(f, y) ⇒^{val} let_{2}(f, y^{M})^{M}]

[let_{1}(f, y) →^{tex} “ let 1( #1. , #2. )”]

[let_{1}(f, y) →^{pyk} “let one ∗ apply ∗ end let”]

[∗ =^{claim} ∗]

[[x =^{claim} y] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x =^{claim} y] ¨= [x →^{claim} y]]⌉)]

[[∗ =^{claim} ∗] →^{tex} “ [#1/tex name/tex. \stackrel {claim}{=}#2. ]”]

[[x =^{claim} y] →^{pyk} “claim define ∗ as ∗ end define”]

checker

[checker →^{val} λt.λc.check(t, c)]

[checker →^{pyk} “checker”]

check(∗, ∗)

[check(t, c) →^{val} If(t^{i}^{s}, c!T, check_{2}(t, c, aspect("claim", t, c)))]

[check(∗, ∗) →^{tex} “ \mathbf{check}( #1. , #2. )”]

[check(t, c) →^{pyk} “check ∗ cache ∗ end check”]

check_{2}(∗, ∗, ∗)

[check_{2}(t, c, d) →^{val} d \{ \begin{matrix}check_{3}(t, c, aspect("definition", t, c)) \\ U^{M}( [ E(d^{3}, T, c) ‘ t ] ‘ c) \end{matrix} ]

[check_{2}(∗, ∗, ∗) →^{tex} “ \mathbf{check} 2( #1. , #2. , #3. )”]

[check_{2}(t, c, d) →^{pyk} “check two ∗ cache ∗ def ∗ end check”]

check_{3}(∗, ∗, ∗)

[check_{3}(t, c, d) →^{val} If(d, check^{∗}(t^{t}, c), t! [ c!T ] )]

[check_{3}(∗, ∗, ∗) →^{tex} “ \mathbf{check} 3( #1. , #2. , #3. )”]

[check_{3}(t, c, d) →^{pyk} “check three ∗ cache ∗ def ∗ end check”]

check^{∗}(∗, ∗)

[check^{∗}(t, c) →^{val} If(t, c!T, check_{2}^{∗}(t^{t}, c, check(t^{h}, c)))]

[check^{∗}(∗, ∗) →^{tex} “ \mathbf{check}ˆ ∗( #1. , #2. )”]

[check^{∗}(t, c) →^{pyk} “check list ∗ cache ∗ end check”]

check_{2}^{∗}(∗, ∗, ∗)

[check_{2}^{∗}(t, c, v) →^{val} If(¬v, t! [ c!v ] , check^{∗}(t, c))]

[check_{2}^{∗}(∗, ∗, ∗) →^{tex} “ \mathbf{check}ˆ ∗ 2( #1. , #2. , #3. )”]

[check_{2}^{∗}(t, c, v) →^{pyk} “check list two ∗ cache ∗ value ∗ end check”]

[∗]^{·}

[[t]^{·} →^{claim} λt.λc.if(U(E(t^{1}, T, c)), T, t)]

[[∗]^{·} →^{tex} “

\relax [ #1. \relax ]ˆ {\cdot} ”] [[t]^{·} →^{pyk} “test ∗ end test”]

[∗]^{−}

[[x]^{−} →^{claim} λt.λc.if(U(E(t^{1}, T, c)), t, T)]

[[x]^{−} →^{tex} “

\relax [ #1. \relax ]ˆ {-} ”]

[[x]^{−} →^{pyk} “false test ∗ end test”]

[∗]^{∘}

[[t]^{∘} →^{claim} λt.λc.U(E(t^{1}, T, c))]

[[∗]^{∘} →^{tex} “

\relax [ #1. \relax ]ˆ {\circ} ”]

[[t]^{∘} →^{pyk} “raw test ∗ end test”]

msg

Predef: message

[msg →^{tex} “

msg”]

[msg →^{pyk} “message”]

[∗ =^{msg} ∗]

[[x =^{msg} y] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x =^{msg} y] ¨= [(x)^{p} →^{msg} y]]⌉)]

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

[[x =^{msg} y] →^{pyk} “message define ∗ as ∗ end define”]

<stmt>

[<stmt> →^{val} ⌈<stmt>⌉]

[<stmt> →^{tex} “

{<}stmt{>}”]

[<stmt> →^{pyk} “the statement aspect”]

stmt

[stmt →^{msg} <stmt>]

[stmt →^{tex} “

stmt”]

[stmt →^{pyk} “statement”]

[∗ =^{stmt} ∗]

[[x =^{stmt} y] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x =^{stmt} y] ¨= [(x)^{p} →^{stmt} y]]⌉)]

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

[[x =^{stmt} y] →^{pyk} “statement define ∗ as ∗ end define”]

HeadNil′

[HeadNil′ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[HeadNil′ ¨= T^{h} = T]⌉)]

[HeadNil′ →^{tex} “ HeadNil’”]

[HeadNil′ →^{pyk} “example axiom”]

HeadPair′

[HeadPair′ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[HeadPair′ ¨= ∀A: ∀B: [ (A : : B)^{h} = A ] ]⌉)] [HeadPair′ →^{tex} “ HeadPair’”]

[HeadPair′ →^{pyk} “example scheme”]

Transitivity′

[Transitivity′ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Transitivity′ ¨= ∀A: ∀B: ∀C: [ [ A = B ] ⊢ [ [ A = C ] ⊢ [ B = C ] ] ] ]⌉)]

[Transitivity′ →^{tex} “ Transitivity’”]

[Transitivity′ →^{pyk} “example rule”]

⊥ ⊥

[⊥ ⊥ →^{val} ⌈⊥ ⊥⌉^{R} : : T]

[⊥ ⊥ →^{tex} “

{\makebox [0mm][l]{$\bot $}\, {\bot }}”]

[⊥ ⊥ →^{pyk} “absurdity”]

Contra′

[Contra′ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Contra′ ¨= [ [ T : : T ] = T ] ⊢ ⊥ ⊥]⌉)]

[Contra′ →^{tex} “ Contra’”]

[Contra′ →^{pyk} “contraexample”]

T′_{E}

[T′_{E} →^{stmt} [ T^{h} = T ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} : : \underline{b} ] ^{h} = \underline{a} ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} = \underline{b} ] ⊢ [ [ \underline{a} = \underline{c} ] ⊢ [ \underline{b} = \underline{c} ] ] ] ] ⊕ [ [ [ T : : T ] = T ] ⊢ ⊥ ⊥ ] ] ] ]

[T′_{E} →^{tex} “

T’ {E}”]

[T′_{E} →^{pyk} “example theory primed”]

L_{1}

[L_{1} →^{stmt} T′_{E} ⊢ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} = \underline{b} ] ⊢ [ \underline{b} = \underline{a} ] ] ]

[L_{1} →^{tex} “

L {1}”]

[L_{1} →^{pyk} “example lemma”]

\underline{∗}

[\underline{x} →^{tex} “\underline\{#1.\}”]

[\underline{x} →^{pyk} “metavar ∗ end metavar”]

A

[A →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[A ¨= \underline{a}]⌉)]

[A →^{tex} “{\cal A}”]

[A →^{pyk} “meta a”]

B

[B →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[B ¨= \underline{b}]⌉)]

[B →^{tex} “{\cal B}”]

[B →^{pyk} “meta b”]

C

[C →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[C ¨= \underline{c}]⌉)]

[C →^{tex} “{\cal C}”]

[C →^{pyk} “meta c”]

D

[D →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[D ¨= \underline{d}]⌉)]

[D →^{tex} “{\cal D}”]

[D →^{pyk} “meta d”]

E

[E →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[E ¨= \underline{e}]⌉)]

[E →^{tex} “{\cal E}”]

[E →^{pyk} “meta e”]

F

[F →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[F ¨= \underline{f}]⌉)]

[F →^{tex} “{\cal F}”]

[F →^{pyk} “meta f”]

G

[G →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[G ¨= \underline{g}]⌉)]

[G →^{tex} “{\cal G}”]

[G →^{pyk} “meta g”]

H

[H →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[H ¨= \underline{h}]⌉)]

[H →^{tex} “{\cal H}”]

[H →^{pyk} “meta h”]

I

[I →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[I ¨= \underline{i}]⌉)]

[I →^{tex} “{\cal I}”]

[I →^{pyk} “meta i”]

J

[J →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[J ¨= \underline{j}]⌉)]

[J →^{tex} “{\cal J}”]

[J →^{pyk} “meta j”]

K

[K →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[K ¨= \underline{k}]⌉)]

[K →^{tex} “{\cal K}”]

[K →^{pyk} “meta k”]

L

[L →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[L ¨= \underline{l}]⌉)]

[L →^{tex} “{\cal L}”]

[L →^{pyk} “meta l”]

M

[M →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[M ¨= \underline{m}]⌉)]

[M →^{tex} “{\cal M}”]

[M →^{pyk} “meta m”]

N

[N →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[N ¨= \underline{n}]⌉)]

[N →^{tex} “{\cal N}”]

[N →^{pyk} “meta n”]

O

[O →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[O ¨= \underline{o}]⌉)]

[O →^{tex} “{\cal O}”]

[O →^{pyk} “meta o”]

P

[P →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[P ¨= \underline{p}]⌉)]

[P →^{tex} “{\cal P}”]

[P →^{pyk} “meta p”]

Q

[Q →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Q ¨= \underline{q}]⌉)]

[Q →^{tex} “{\cal Q}”]

[Q →^{pyk} “meta q”]

R

[R →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[R ¨= \underline{r}]⌉)]

[R →^{tex} “{\cal R}”]

[R →^{pyk} “meta r”]

S

[S →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[S ¨= \underline{s}]⌉)]

[S →^{tex} “{\cal S}”]

[S →^{pyk} “meta s”]

T

[T →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[T ¨= \underline{t}]⌉)]

[T →^{tex} “{\cal T}”]

[T →^{pyk} “meta t”]

U

[U →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[U ¨= \underline{u}]⌉)]

[U →^{tex} “{\cal U}”]

[U →^{pyk} “meta u”]

V

[V →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[V ¨= \underline{v}]⌉)]

[V →^{tex} “{\cal V}”]

[V →^{pyk} “meta v”]

W

[W →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[W ¨= \underline{w}]⌉)]

[W →^{tex} “{\cal W}”]

[W →^{pyk} “meta w”]

X

[X →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[X ¨= \underline{x}]⌉)]

[X →^{tex} “{\cal X}”]

[X →^{pyk} “meta x”]

Y

[Y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Y ¨= \underline{y}]⌉)]

[Y →^{tex} “{\cal Y}”]

[Y →^{pyk} “meta y”]

Z

[Z →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Z ¨= \underline{z}]⌉)]

[Z →^{tex} “{\cal Z}”]

[Z →^{pyk} “meta z”]

⟨∗ | ∗:= ∗⟩

[⟨a |x:= b⟩ →^{val} x! [ b! If(a^{V}, If(a =^{t} x, b, a), If(¬ [ a =^{r} ⌈∀∗: ∗⌉ ] , a^{h} : : ⟨^{∗}a^{t} |x:= b⟩,

If(a^{1} =^{t} x, a,

[ a^{0} : : [ a^{1} : : [ ⟨a^{2} |x:= b⟩ : : T ] ] ] ))) ] ]

[⟨a |x:= b⟩ →^{tex} “

\langle #1. \, {\protect\vert}#2. {:=}\, #3. \rangle ”]

[⟨a |x:= b⟩ →^{pyk} “sub ∗ set ∗ to ∗ end sub”]

⟨^{∗}∗ | ∗:= ∗⟩

[⟨^{∗}a |x:= b⟩ →^{val} x! [ b!If(a, T, ⟨a^{h} |x:= b⟩ : : ⟨^{∗}a^{t} |x:= b⟩) ] ]

[⟨^{∗}a |x:= b⟩ →^{tex} “

\langle ˆ { \ast } #1. \, {\protect\vert}#2. {:=}\, #3. \rangle ”]

[⟨^{∗}a |x:= b⟩ →^{pyk} “sub star ∗ set ∗ to ∗ end sub”]

∅

[∅ →^{val} T]

[∅ →^{tex} “

\emptyset ”]

[∅ →^{pyk} “the empty set”]

Remainder

[Remainder →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Remainder ¨= HeadPair′ ⊕ [ Transitivity′ ⊕ Contra′ ] ]⌉)]

[Remainder →^{tex} “ Remainder”]

[Remainder →^{pyk} “example remainder”]

(∗)^{v}

[(x)^{v} →^{name} “

( #1. )ˆ {\bf v}”]

[(x)^{v} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[(x)^{v} ¨= x]⌉)]

[(x)^{v} →^{tex} “#1/tex name.”]

[(x)^{v} →^{pyk} “make visible ∗ end visible”]

intro(∗, ∗, ∗, ∗)

[intro(x, i, p, t) →^{name} “ intro(#1. , #2. , #3. , #4. )”]

[intro(x, i, p, t) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[intro(x, i, p, t) ¨= math [x =^{pyk} p] end mathmath [x =^{tex} t] end math]⌉)]

[intro(x, i, p, t) →^{tex} “\index{#2.: #3. @#2.: $[#1/tex name/tex.]$ #3.}% \index{pyk: #3. $[#1/tex name/tex.]$}% \tex{ $[#1/tex name/tex. \stackrel {\mathrm {tex}}{=} #4/tex name. ]$}$[ #1/tex name/tex.% ]$\footnote{$[#1/tex name/tex. \stackrel {\mathrm {pyk}}{=} #3/tex name. ]$}”]

[intro(x, i, p, t) →^{pyk} “intro ∗ index ∗ pyk ∗ tex ∗ end intro”]

intro(∗, ∗, ∗)

[intro(x, p, t) →^{name} “ intro(#1. , #2. , #3. )”]

[intro(x, p, t) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[intro(x, p, t) ¨= math [x =^{pyk} p] end mathmath [x =^{tex} t] end math]⌉)]

[intro(x, p, t) →^{tex} “\index{\alpha #2. @\back \makebox[20mm][l]{$[#1/tex name/tex.]$}#2.}% \index{pyk: #2. $[#1/tex name/tex.]$}% \tex{ $[#1/tex name/tex. \stackrel {\mathrm {tex}}{=} #3/tex name. ]$}$[ #1/tex name/tex.% ]$\footnote{$[#1/tex name/tex. \stackrel {\mathrm {pyk}}{=} #2/tex name. ]$}”]

[intro(x, p, t) →^{pyk} “intro ∗ pyk ∗ tex ∗ end intro”]

error(∗, ∗)

[error(m, t) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[error(m, t) ¨= error_{2}(⌈m⌉, t)]⌉)]

[error(m, t) →^{tex} “ error(#1/tex name. , #2. )”]

[error(m, t) →^{pyk} “error ∗ term ∗ end error”]

error_{2}(∗, ∗)

[error_{2}(m, t) →^{val} t-color(m^{1} [ ⌈“ ”⌉^{1}t ] )]

[error_{2}(m, t) →^{tex} “ error {2}(#1/tex name. , #2. )”] [error_{2}(m, t) →^{pyk} “error two ∗ term ∗ end error”]

proof(∗, ∗, ∗)

[proof(p, t, c) →^{val} proof_{2}(S(c, p), t)]

[proof(p, t, c) →^{tex} “ proof( #1. , #2. , #3. )”]

[proof(p, t, c) →^{pyk} “proof ∗ term ∗ cache ∗ end proof”]

proof_{2}(∗, ∗)

[proof_{2}(q, t) →^{val} t! If(q^{E}, q, If(¬ [ q^{0} ] , error_{2}(⌈“Proof has at least one unresolved premise. Lemma; premise reads:”⌉, t; [ q^{0}^{h} ] ), If(¬ [ q^{1} ] , error_{2}(⌈“Proof has at least one unresolved side condition. Lemma; condition reads:”⌉, t; [ q^{1}^{h} ] ),

If(q^{2} =^{t} t, T,

error_{2}(⌈“Lemma does not match conclusion. Lemma; conclusion reads:”⌉, t; [ q^{2} ] )))))]

[proof_{2}(q, t) →^{tex} “ proof {2}( #1. , #2. )”]

[proof_{2}(q, t) →^{pyk} “proof two ∗ term ∗ end proof”]

S(∗, ∗)

[S(c, t) →^{val} c!

If(t^{E}, t, If(t =^{r} ⌈∗^{I}⌉, S^{I}(c, t),

If(t =^{r} ⌈∗^{⊳} ⌉, S^{⊳} (c, t),

If(t =^{r} ⌈∗^{V}⌉, S^{E}(c, t),

If(t =^{r} ⌈∗^{+}⌉, S^{+}(c, t),

If(t =^{r} ⌈∗^{−}⌉, S^{−}(c, t),

If(t =^{r} ⌈∗^{∗}⌉, S^{∗}(c, t),

If(t =^{r} ⌈∗ @ ∗⌉, S^{@}(c, t),

If(t =^{r} ⌈∗ ⊢ ∗⌉, S^{⊢}(c, t),

If(t =^{r} ⌈∗ ⊢⊢ ∗⌉, S⊢ ⊢(c, t),

If(t =^{r} ⌈∗ i.e. ∗⌉, S^{i.e.}(c, t),

If(t =^{r} ⌈∀∗: ∗⌉, S^{∀}(c, t),

If(t =^{r} ⌈∗; ∗⌉, S^{;}(c, t),

error_{2}(⌈“Unknown sequent operator:”⌉, t))))))))))))))]

[S(x, y) →^{tex} “

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

[S(x, y) →^{pyk} “sequent eval ∗ term ∗ end eval”]

S^{I}(∗, ∗)

[S^{I}(c, t) →^{val} c! [ ∅ : : [ ∅ : : [ t-color(t^{1} ⊢ [ t^{1} ] ) : : T ] ] ] ]

[S^{I}(x, y) →^{tex} “

{\cal S}ˆ {I}(#1. , #2. )”]

[S^{I}(x, y) →^{pyk} “seqeval init ∗ term ∗ end eval”]

S^{⊳}(∗, ∗)

[S^{⊳} (c, t) →^{val} S_{1}^{⊳} (c, t, S(c, t^{1}))]

[S^{⊳} (x, y) →^{tex} “

{\cal S}ˆ {\rhd}(#1. , #2. )”]

[S^{⊳} (x, y) →^{pyk} “seqeval modus ∗ term ∗ end eval”]

S_{1}^{⊳}(∗, ∗, ∗)

[S_{1}^{⊳} (c, t, q) →^{val} c! [ t! If(q^{E}, q, If(q^{2} =^{r} ⌈∗ ⊢ ∗⌉, q^{0} ∪ {q^{2}^{1}} : : [ q^{1} : : [ q^{2}^{2} : : T ] ] , If(q^{2} =^{r} ⌈∗ ⊢⊢ ∗⌉, q^{0} : : [ q^{1} ∪ {q^{2}^{1}} : : [ q^{2}^{2} : : T ] ] , error_{2}(⌈“The modus operation requires the conclusion of its argument to be an inference or an endorsement”⌉, t)))) ] ]

[S_{1}^{⊳} (x, y, z) →^{tex} “

{\cal S} {1}ˆ {\rhd}(#1. , #2. , #3. )”]

[S_{1}^{⊳} (x, y, z) →^{pyk} “seqeval modus one ∗ term ∗ sequent ∗ end eval”]

S^{E}(∗, ∗)

[S^{E}(c, t) →^{val} S_{1}^{E}(c, t, S(c, t^{1}))]

[S^{E}(x, y) →^{tex} “

{\cal S}ˆ {E}(#1. , #2. )”]

[S^{E}(x, y) →^{pyk} “seqeval verify ∗ term ∗ end eval”]

S_{1}^{E}(∗, ∗, ∗)

[S_{1}^{E}(c, t, q) →^{val} c! [ t! If(q^{E}, q, If(¬ [ q^{2} =^{r} ⌈∗ ⊢⊢ ∗⌉ ] , error_{2}(⌈“The verify operation requires the conclusion of its argument to be an endorsement:”⌉, t), If(¬ [ q^{2}^{1}^{C} ] , error_{2}(⌈“The verify operation requires the side condition to contain no metavariables. Term; condition:”⌉, t; [ q^{2}^{1} ] ), If(U^{M}(U^{M}(E(q^{2}^{1}, T, c)) ‘ c), q^{0} : : [ q^{1} : : [ q^{2}^{2} : : T ] ] , error_{2}(⌈“False side condition:”⌉, t))))) ] ]

[S_{1}^{E}(x, y, z) →^{tex} “

{\cal S} {1}ˆ {E}(#1. , #2. , #3.

)”]

[S_{1}^{E}(x, y, z) →^{pyk} “seqeval verify one ∗ term ∗ sequent ∗ end eval”]

S^{+}(∗, ∗)

[S^{+}(c, t) →^{val} S_{1}^{+}(c, t, S(c, t^{1}))]

[S^{+}(x, y) →^{tex} “

{\cal S}ˆ {+}(#1. , #2. )”]

[S^{+}(x, y) →^{pyk} “sequent eval plus ∗ term ∗ end eval”]

S_{1}^{+}(∗, ∗, ∗)

[S_{1}^{+}(c, t, q) →^{val} c! [ t! If(q^{E}, q,

If( [ q^{2} =^{r} ⌈∗ ⊢ ∗⌉ ] ∧ [ q^{2}^{2} =^{r} ⌈∗ ⊢ ∗⌉ ] ,

[ q^{0} : : [ q^{1} : : [ t-color( [ q^{2}^{1} ⊕ [ q^{2}^{2}^{1} ] ] ⊢ [ q^{2}^{2}^{2} ] ) : : T ] ] ] , error_{2}(⌈“Term; conclusion not fit for decurrying:”⌉, t; [ q^{2} ] ))) ] ]

[S_{1}^{+}(x, y, z) →^{tex} “

{\cal S} {1}ˆ {+}(#1. , #2. , #3. )”]

[S_{1}^{+}(x, y, z) →^{pyk} “seqeval plus one ∗ term ∗ sequent ∗ end eval”]

S^{−}(∗, ∗)

[S^{−}(c, t) →^{val} S_{1}^{−}(c, t, S(c, t^{1}))]

[S^{−}(x, y) →^{tex} “

{\cal S}ˆ {-}(#1. , #2. )”]

[S^{−}(x, y) →^{pyk} “seqeval minus ∗ term ∗ end eval”]

S_{1}^{−}(∗, ∗, ∗)

[S_{1}^{−}(c, t, q) →^{val} c! [ t! If(q^{E}, q,

If( [ q^{2} =^{r} ⌈∗ ⊢ ∗⌉ ] ∧ [ q^{2}^{1} =^{r} ⌈∗ ⊕ ∗⌉ ] ,

[ q^{0} : : [ q^{1} : : [ t-color(q^{2}^{1}^{1} ⊢ [ q^{2}^{1}^{2} ⊢ [ q^{2}^{2} ] ] ) : : T ] ] ] , error_{2}(⌈“Term; conclusion not fit for decurrying:”⌉, t; [ q^{2} ] ))) ] ]

[S_{1}^{−}(x, y, z) →^{tex} “

{\cal S} {1}ˆ {-}(#1. , #2. , #3. )”]

[S_{1}^{−}(x, y, z) →^{pyk} “seqeval minus one ∗ term ∗ sequent ∗ end eval”]

S^{∗}(∗, ∗)

[S^{∗}(c, t) →^{val} S_{1}^{∗}(c, t, S(c, t^{1}))]

[S^{∗}(x, y) →^{tex} “

{\cal S}ˆ {\ast}(#1. , #2. )”]

[S^{∗}(x, y) →^{pyk} “seqeval deref ∗ term ∗ end eval”]

S_{1}^{∗}(∗, ∗, ∗)

[S_{1}^{∗}(c, t, q) →^{val} c! [ t! If(q^{E}, q, S_{2}^{∗}(c, t, q, aspect(<stmt>, q^{2}, c))) ] ]

[S_{1}^{∗}(x, y, z) →^{tex} “

{\cal S} {1}ˆ {\ast}(#1. , #2. , #3. )”]

[S_{1}^{∗}(x, y, z) →^{pyk} “seqeval deref one ∗ term ∗ sequent ∗ end eval”]

S_{2}^{∗}(∗, ∗, ∗, ∗)

[S_{2}^{∗}(c, t, q, d) →^{val} c! [ t! [ q! If(d, error_{2}(⌈“Dereferencing construct that has no statement def:”⌉, t), [ q^{0} : : [ q^{1} : : [ d^{3} : : T ] ] ] ) ] ] ]

[S_{2}^{∗}(c, t, q, d) →^{tex} “

{\cal S} {2}ˆ {\ast}(#1. , #2. , #3. , #4. )”]

[S_{2}^{∗}(c, t, q, d) →^{pyk} “seqeval deref two ∗ term ∗ sequent ∗ def ∗ end eval”]

S^{@}(∗, ∗)

[S^{@}(c, t) →^{val} S_{1}^{@}(c, t, S(c, t^{1}))]

[S^{@}(x, y) →^{tex} “

{\cal S}ˆ {\char64}(#1. , #2. )”]

[S^{@}(x, y) →^{pyk} “seqeval at ∗ term ∗ end eval”]

S_{1}^{@}(∗, ∗, ∗)

[S_{1}^{@}(c, t, q) →^{val} c! [ t! If(q^{E}, q, If(¬ [ q^{2} =^{r} ⌈∀∗: ∗⌉ ] , error_{2}(⌈“Quantifier elimination requires the conclusion of its argument to be a quantifier:”⌉, t), If(¬ [ t^{2} free for q^{2}^{1} in [ q^{2}^{2} ] ] , error_{2}(⌈“Quantifier elimination leads to variable clash:”⌉, t), [ q^{0} : : [ q^{1} : : [ ⟨q^{2}^{2} |q^{2}^{1}:= t^{2}⟩ : : T ] ] ] ))) ] ]

[S_{1}^{@}(c, t, q) →^{tex} “

{\cal S} {1}ˆ {\char64}(#1. , #2. , #3. )”]

[S_{1}^{@}(c, t, q) →^{pyk} “seqeval at one ∗ term ∗ sequent ∗ end eval”]

S^{⊢}(∗, ∗)

[S^{⊢}(c, t) →^{val} S_{1}^{⊢}(c, t, t^{1}, S(c, t^{2}))]

[S^{⊢}(x, y) →^{tex} “

{\cal S}ˆ {\vdash}(#1. , #2. )”]

[S^{⊢}(x, y) →^{pyk} “seqeval infer ∗ term ∗ end eval”]

S_{1}^{⊢}(∗, ∗, ∗, ∗)

[S_{1}^{⊢}(c, t, p, q) →^{val} c! [ t! [ p! If(q^{E}, q, [ q^{0}\{p} : : [ q^{1} : : [ t-color(p ⊢ [ q^{2} ] ) : : T ] ] ] ) ] ] ]

[S_{1}^{⊢}(x, y, z, u) →^{tex} “

{\cal S} {1}ˆ {\vdash}(#1. , #2. , #3. , #4. )”]

[S_{1}^{⊢}(x, y, z, u) →^{pyk} “seqeval infer one ∗ term ∗ premise ∗ sequent ∗ end eval”]

S ⊢^{⊢}(∗, ∗)

[S⊢ ⊢(c, t) →^{val} S⊢ ⊢ ; 1(c, t, t^{1}, S(c, t^{2}))]

[S⊢ ⊢(x, y) →^{tex} “

{\cal S}ˆ {\makebox [0mm][l]{\scriptsize $\vdash $}\, {\vdash }}(#1. , #2. )”]

[S⊢ ⊢(x, y) →^{pyk} “seqeval endorse ∗ term ∗ end eval”]

S ⊢^{⊢} ; 1(∗, ∗, ∗, ∗)

[S⊢ ⊢ ; 1(c, t, p, q) →^{val} c! [ t! [ p! If(q^{E}, q, [ q^{0} : : [ q^{1}\{p} : : [ t-color(p ⊢⊢ [ q^{2} ] ) : : T ] ] ] ) ] ] ]

[S⊢ ⊢ ; 1(x, y, z, u) →^{tex} “

{\cal S} {1}ˆ {\makebox [0mm][l]{\scriptsize $\vdash $}\, {\vdash }}(#1. , #2. , #3. , #4. )”]

[S⊢ ⊢ ; 1(x, y, z, u) →^{pyk} “seqeval endorse one ∗ term ∗ side ∗ sequent ∗ end eval”]

S^{i.e.}(∗, ∗)

[S^{i.e.}(c, t) →^{val} S_{1}^{i.e.}(c, t, t^{2}, S(c, t^{1}))]

[S^{i.e.}(x, y) →^{tex} “

{\cal S}ˆ {i.e.}(#1. , #2. )”]

[S^{i.e.}(x, y) →^{pyk} “seqeval est ∗ term ∗ end eval”]

S_{1}^{i.e.}(∗, ∗, ∗, ∗)

[S_{1}^{i.e.}(c, t, a, q) →^{val} c! [ t! [ a! If(q^{E}, q, S_{2}^{i.e.}(c, t, a, q, aspect(<stmt>, a, c))) ] ] ]

[S_{1}^{i.e.}(x, y, z, u) →^{tex} “ {\cal S} {1}ˆ {i.e.}(#1. , #2. , #3. , #4. )”]

[S_{1}^{i.e.}(x, y, z, u) →^{pyk} “seqeval est one ∗ term ∗ name ∗ sequent ∗ end eval”]

S_{2}^{i.e.}(∗, ∗, ∗, ∗, ∗)

[S_{2}^{i.e.}(c, t, a, q, d) →^{val} c! [ t! [ a! [ q! If(d, error_{2}(⌈“Referencing construct that has no statement def:”⌉, t), If(¬ [ d^{3} =^{t} [ q^{2} ] ] , error_{2}(⌈“Reference; conclusion do not match:”⌉, a; [ q^{2} ] ), [ q^{0} : : [ q^{1} : : [ a : : T ] ] ] )) ] ] ] ]

[S_{2}^{i.e.}(c, t, a, q, d) →^{tex} “ {\cal S} {2}ˆ {i.e.}(#1.

, #2. , #3. , #4. , #5. )”]

[S_{2}^{i.e.}(c, t, a, q, d) →^{pyk} “seqeval est two ∗ term ∗ name ∗ sequent ∗ def ∗ end eval”]

S^{∀}(∗, ∗)

[S^{∀}(c, t) →^{val} S_{1}^{∀}(c, t, t^{1}, S(c, t^{2}))]

[S^{∀}(x, y) →^{tex} “

{\cal S}ˆ {\forall}(#1. , #2. )”]

[S^{∀}(x, y) →^{pyk} “seqeval all ∗ term ∗ end eval”]

S_{1}^{∀}(∗, ∗, ∗, ∗)

[S_{1}^{∀}(c, t, v, q) →^{val} c! [ t! [ v! If(q^{E}, q, If(¬ [ v^{V} ] , error_{2}(⌈“Metageneralization over non-metavariable:”⌉, t), If(v free in [ q^{0} ] , error_{2}(⌈“Metageneralization over metavariable that occurs free in some premise:”⌉, t), If(v free in [ q^{1} ] , error_{2}(⌈“Metageneralization over metavariable that occurs free in some side condition:”⌉, t), [ q^{0} : : [ q^{1} : : [ t-color(∀v: [ q^{2} ] ) : : T ] ] ] )))) ] ] ]

[S_{1}^{∀}(c, t, v, q) →^{tex} “

{\cal S} {1}ˆ {\forall}(#1. , #2. , #3. , #4. )”]

[S_{1}^{∀}(c, t, v, q) →^{pyk} “seqeval all one ∗ term ∗ variable ∗ sequent ∗ end eval”]

S^{;}(∗, ∗)

[S^{;}(c, t) →^{val} S_{1}^{;}(c, t, S(c, t^{1}))]

[S^{;}(x, y) →^{tex} “

{\cal S}ˆ {; }(#1. , #2. )”]

[S^{;}(x, y) →^{pyk} “seqeval cut ∗ term ∗ end eval”]

S_{1}^{;}(∗, ∗, ∗)

[S_{1}^{;}(c, t, p) →^{val} c! [ t! If(p^{E}, p, S_{2}^{;}(c, t, p, S(c, t^{2}))) ] ]

[S_{1}^{;}(x, y, z) →^{tex} “

{\cal S} {1}ˆ {; }(#1. , #2. , #3. )”]

[S_{1}^{;}(c, t, p) →^{pyk} “seqeval cut one ∗ term ∗ forerunner ∗ end eval”]

S_{2}^{;}(∗, ∗, ∗, ∗)

[S_{2}^{;}(c, t, p, q) →^{val} c! [ t! [ p! If(q^{E}, q, [ p^{0} ∪ [ q^{0}\{p^{2}} ] ] : : [ [ p^{1} ∪ [ q^{1} ] ] : : [ q^{2} : : T ] ] ) ] ] ]

[S_{2}^{;}(c, t, p, q) →^{tex} “

{\cal S} {2}ˆ {; }(#1. , #2. , #3. , #4. )”]

[S_{2}^{;}(x, y, z, u) →^{pyk} “seqeval cut two ∗ term ∗ forerunner ∗ sequent ∗ end eval”]

T (∗)

[T (x) →^{val} x!Λλc.x]

[T (x) →^{tex} “

{\cal T}( #1. )”]

[T (x) →^{pyk} “computably true ∗ end true”]

claims(∗, ∗, ∗)

[claims(t, c, r) →^{val} If(claims_{2}(t, c, r), T, claims_{2}(t, c, c[r]["bibliography"]^{1}))]

[claims(t, c, r) →^{tex} “ claims( #1. , #2. , #3. )”]

[claims(t, c, r) →^{pyk} “claims ∗ cache ∗ ref ∗ end claims”]

claims_{2}(∗, ∗, ∗)

[claims_{2}(t, c, r) →^{val} If(¬ [ r^{c} ] , t! [ c!F ] , t ∈_{c} [ c[r]["codex"][r][0][0]["claim"]^{3} ] )]

[claims_{2}(t, c, r) →^{tex} “ claims 2( #1. , #2. , #3. )”]

[claims_{2}(t, c, r) →^{pyk} “claims two ∗ cache ∗ ref ∗ end claims”]

<proof>

[<proof> →^{val} ⌈<proof>⌉]

[<proof> →^{tex} “ {<}proof{>}”]

[<proof> →^{pyk} “the proof aspect”]

proof

[proof →^{msg} <proof>]

[proof →^{tex} “ proof”]

[proof →^{pyk} “proof”]

[Lemma ∗: ∗]

[[Lemma x: y] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[Lemma x: y] ¨= [x →^{stmt} y]]⌉)]

[[Lemma x: y] →^{tex} “ [ \mathbf{Lemma\ } #1. \colon #2. ]”]

[[Lemma x: y] →^{pyk} “lemma ∗ says ∗ end lemma”]

[Proof of ∗: ∗]

[[Proof of x: y] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[Proof of x: y] ¨= [x →^{proof} y]]⌉)]

[[Proof of x: y] →^{tex} “ [ \mathbf{Proof\ of\ }#1/tex name/tex. \colon #2. ]”]

[[Proof of x: y] →^{pyk} “proof of ∗ reads ∗ end proof”]

[∗ lemma ∗: ∗]

[[x lemma y: z] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x lemma y: z] ¨= [y =^{stmt} x ⊢ z]]⌉)]

[[x lemma y: z] →^{tex} “ [ #1. \mathbf{\ lemma\ } #2. \colon #3. ]”]

[[x lemma y: z] →^{pyk} “in theory ∗ lemma ∗ says ∗ end lemma”]

[∗ antilemma ∗: ∗]

[[x antilemma y: z] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x antilemma y: z] ¨= [x lemma y: z ⊢ ⊥ ⊥]]⌉)]

[[x antilemma y: z] →^{tex} “ [ #1. \mathbf{\ antilemma\ } #2.

\colon #3. ]”]

[[x antilemma y: z] →^{pyk} “in theory ∗ antilemma ∗ says ∗ end antilemma”]

[∗ rule ∗: ∗]

[[x rule y: z] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x rule y: z] ¨= [x lemma y: z][Proof of y: Rule tactic]]⌉)]

[[x rule y: z] →^{tex} “ [ #1. \mathbf{\ rule\ } #2. \colon #3. ]”]

[[x rule y: z] →^{pyk} “in theory ∗ rule ∗ says ∗ end rule”]

[∗ antirule ∗: ∗]

[[x antirule y: z] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x antirule y: z] ¨= [x rule y: z ⊢ ⊥ ⊥]]⌉)]

[[x antirule y: z] →^{tex} “ [ #1. \mathbf{\ antirule\ } #2. \colon #3. ]”]

[[x antirule y: z] →^{pyk} “in theory ∗ antirule ∗ says ∗ end antirule”]

verifier

[verifier →^{val} λt.λc.V_{1}(c)]

[verifier →^{pyk} “verifier”]

V_{1}(∗)

[V_{1}(c) →^{val}

let_{1}(λr. let_{1}(λx. let_{1}(λp. let_{1}(λd. If(¬d, d, let_{1}(λi. If(¬ [ i^{c} ] , T, error_{2}(⌈“Circular proof. Circle includes:”⌉, p[i]^{0}^{h})), V_{5}(c, r, p, p))), V_{3}(c, r, p, T)), V_{2}(c, x)), c[r]["codex"][r]), c[0])]

[V_{1}(c) →^{tex} “

{\cal V} 1( #1. )”]

[V_{1}(c) →^{pyk} “verify one ∗ end verify”]

V_{2}(∗, ∗)

[V_{2}(c, p) →^{val} c!

If(p, T, If(¬ [ p^{h}^{c} ] , V_{2}(c, p^{h}) : : V_{2}(c, p^{t}), p^{h} : : let_{1}(λd. If(d, T, let_{1}(λr. If(r^{E}, error_{2}(⌈“Error in proof of”⌉, d^{2} [ ⌈“ ”⌉^{1}r ] ), r), S(c, U^{M}( [ E(d^{3}, T, c) ‘ c ] ‘ p)))), aspect(<proof>, p^{t}))))]

[V_{2}(c, p) →^{tex} “

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

[V_{2}(c, p) →^{pyk} “verify two ∗ proofs ∗ end verify”]

V_{3}(∗, ∗, ∗, ∗)

[V_{3}(c, r, p, d) →^{val} c! [ r! [ p! If(¬d, d, If(p, T, If(¬ [ p^{h}^{c} ] , V_{3}(c, r, p^{t}, V_{3}(c, r, p^{h}, T)), let_{1}(λi. let_{1}(λq. If(q, T, If(q^{E}, q, If(¬ [ q^{1} ] , error_{2}(⌈“Unchecked sidecondition:”⌉, q^{1}^{h}), let_{1}(λd.

If(d, error_{2}(⌈“Proof of non-existent lemma:”⌉, q^{2}), If(¬ [ q^{2} =^{t} [ d^{3} ] ] , error_{2}(⌈“Lemma/proof mismatch:”⌉, d^{2}; [ q^{2} ] ), V_{4}(c, q^{0}))), aspect(<stmt>, c[r]["codex"][r][i]))))), p^{t}), p^{h})))) ] ] ]

[V_{3}(c, r, p, d) →^{tex} “

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

[V_{3}(c, r, p, d) →^{pyk} “verify three ∗ ref ∗ sequents ∗ diagnose ∗ end verify”]

V_{4}(∗, ∗)

[V_{4}(c, p) →^{val} c!

If(p, T, let_{1}(λd. If(¬d, d, let_{1}(λp. let_{1}(λr. let_{1}(λi. If(¬ [ c[r]["diagnose"] ] , error_{2}(⌈“Reference to erroneous page”⌉, p), If(¬claims(⌈verifier⌉, c, r), error_{2}(⌈“Reference to unchecked lemma”⌉, p), If(aspect(<proof>, p, c), error_{2}(⌈“Reference to unproved lemma”⌉, p), T))), p^{i}), p^{r}), p^{h})), V_{4}(c, p^{t})))]

[V_{4}(c, p) →^{tex} “

{\cal V} 4( #1. , #2. )”]

[V_{4}(c, p) →^{pyk} “verify four ∗ premises ∗ end verify”]

V_{5}(∗, ∗, ∗, ∗)

[V_{5}(c, r, a, q) →^{val} c! [ r! [ a! If(q^{c}, q, If(a, q, If(¬ [ a^{h}^{c} ] , V_{5}(c, r, a^{t}, V_{5}(c, r, a^{h}, q)), V_{7}(c, r, a^{h}, q)))) ] ] ]

[V_{5}(c, r, a, q) →^{tex} “

{\cal V} 5( #1. , #2. , #3. , #4. )”]

[V_{5}(c, r, a, q) →^{pyk} “verify five ∗ ref ∗ array ∗ sequents ∗ end verify”]

V_{6}(∗, ∗, ∗, ∗)

[V_{6}(c, r, p, q) →^{val} c! [ r! [ p! If(q^{c}, q, If(p, q, let_{1}(λq. If(q^{c}, q, If(¬ [ r ≈ [ p^{h}^{r} ] ] , q, V_{7}(c, r, p^{h}^{i}, q))), V_{6}(c, r, p^{t}, q)))) ] ] ]

[V_{6}(c, r, p, q) →^{tex} “

{\cal V} 6( #1. , #2. , #3. , #4. )”]

[V_{6}(c, r, p, q) →^{pyk} “verify six ∗ ref ∗ list ∗ sequents ∗ end verify”]

V_{7}(∗, ∗, ∗, ∗)

[V_{7}(c, r, i, q) →^{val} c! [ r! let_{1}(λv. If(v, q, If(v ≈ 0, i, If(v ≈ 1, q, let_{1}(λq. If(q^{c}, q, q[i→1]), V_{6}(c, r, v^{0}, q[i→0]))))), q[i]) ] ]

[V_{7}(c, r, i, q) →^{tex} “

{\cal V} 7( #1. , #2. , #3. , #4. )”] [V_{7}(c, r, i, q) →^{pyk} “verify seven ∗ ref ∗ id ∗ sequents ∗ end verify”]

Cut(∗, ∗)

[Cut(a, b) →^{val} If(b, a, a; b)]

[Cut(a, b) →^{tex} “ Cut( #1. , #2. )”]

[Cut(a, b) →^{pyk} “cut ∗ and ∗ end cut”]

Head_{⊕}(∗)

[Head_{⊕}(s) →^{val} [ s^{1} ⊢ [ s^{2} ⊢ [ s^{1}^{I}^{⊳} ] ] ] ^{+}^{⊳} ]

[Head_{⊕}(s) →^{tex} “ Head {\oplus} ( #1. )”]

[Head_{⊕}(s) →^{pyk} “head ∗ end head”]

Tail_{⊕}(∗)

[Tail_{⊕}(s) →^{val} [ s^{1} ⊢ [ s^{2}^{I} ] ] ^{+}^{⊳} ]

[Tail_{⊕}(s) →^{tex} “ Tail {\oplus} ( #1. )”]

[Tail_{⊕}(s) →^{pyk} “tail ∗ end tail”]

rule_{1}(∗, ∗)

[rule_{1}(s, t) →^{val}

If(s =^{t} t, T,

If(¬ [ t =^{r} ⌈x ⊕ y⌉ ] , 0,

let_{1}(λp. If(¬ [ p^{c} ] , Cut(Head_{⊕}(t), p), let_{1}(λp. If(¬ [ p^{c} ] , Cut(Tail_{⊕}(t), p), 0), rule_{1}(s, t^{2}))), rule_{1}(s, t^{1}))))]

[rule_{1}(s, t) →^{tex} “ rule 1( #1. , #2. )”]

[rule_{1}(s, t) →^{pyk} “rule one ∗ theory ∗ end rule”]

rule(∗, ∗)

[rule(c, p) →^{val} c! let_{1}(λs. If(s, ⌈“Rule has no statement aspect”⌉, If(¬ [ s =^{r} ⌈x ⊢ y⌉ ] , error_{2}(⌈“Rule has invalid statement aspect”⌉, s), let_{1}(λt. If(t, ⌈“Theory has no statement aspect”⌉, let_{1}(λr. If(r^{c}, error_{2}(⌈“The theory does not assert the given rule”⌉, s; t), [ s^{1} ⊢ Cut(s^{1}^{I}^{⊳} ^{∗}, r) ] ), rule_{1}(s^{2}, t))), aspect(<stmt>, s^{1}, c)^{3}))), aspect(<stmt>, p^{t})^{3})]

[rule(c, p) →^{tex} “ rule( #1. , #2. )”]

[rule(c, p) →^{pyk} “rule ∗ subcodex ∗ end rule”]

Rule tactic

[Rule tactic →^{val} λc.λp.rule(c, p)]

[Rule tactic →^{tex} “ Rule\ tactic”]

[Rule tactic →^{pyk} “rule tactic”]

Plus(∗, ∗)

[Plus(a, b) →^{val} If(b, a, a ⊕ b)]

[Plus(a, b) →^{tex} “ Plus( #1. , #2. )”]

[Plus(a, b) →^{pyk} “plus ∗ and ∗ end plus”]

[Theory ∗]

[[Theory n] →^{macro} λt.λs.λc.theory_{2}(t, c)]

[[Theory n] →^{tex} “ [ \mathbf{Theory\ } #1. ]”]

[[Theory n] →^{pyk} “theory ∗ end theory”]

theory_{2}(∗, ∗)

[theory_{2}(t, c) →^{val} let_{1}(λn. let_{1}(λs. Q̃(t, ⌈[n →^{stmt} x]⌉, s), [ ⌈n⌉ : : n ] : : [ [ ⌈x⌉ : : theory_{3}(c, n) ] : : T ] ), t^{1})]

[theory_{2}(t, c) →^{tex} “ theory 2( #1. , #2. )”]

[theory_{2}(t, c) →^{pyk} “theory two ∗ cache ∗ end theory”]

theory_{3}(∗, ∗)

[theory_{3}(c, n) →^{val} n! let_{1}(λr. theory_{4}(c[r]["codex"][r], n, T), c[0])]

[theory_{3}(c, n) →^{tex} “ theory 3( #1. , #2. )”]

[theory_{3}(c, n) →^{pyk} “theory three ∗ name ∗ end theory”]

theory_{4}(∗, ∗, ∗)

[theory_{4}(c, n, s) →^{val} n! If(c, s, If(¬ [ c^{h}^{c} ] , theory_{4}(c^{t}, n, theory_{4}(c^{h}, n, s)), If(¬ [ aspect(<proof>, c^{t})^{3} =^{t} ⌈Rule tactic⌉ ] , s, let_{1}(λd.

If(¬ [ d^{1} =^{t} n ] , s,

Plus(d^{2}, s)), aspect(<stmt>, c^{t})^{3}))))]

[theory_{4}(c, n, s) →^{tex} “ theory 4( #1. , #2. , #3. )”]

[theory_{4}(c, n, s) →^{pyk} “theory four ∗ name ∗ sum ∗ end theory”]

HeadNil′′

[HeadNil′′ →^{proof} Rule tactic]

[HeadNil′′ →^{stmt} T′_{E} ⊢ [ T^{h} = T ] ]

[HeadNil′′ →^{tex} “ HeadNil’’”]

[HeadNil′′ →^{pyk} “example axiom lemma primed”]

HeadPair′′

[HeadPair′′ →^{proof} Rule tactic]

[HeadPair′′ →^{stmt} T′_{E} ⊢ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} : : \underline{b} ] ^{h} = \underline{a} ] ]

[HeadPair′′ →^{tex} “ HeadPair’’”]

[HeadPair′′ →^{pyk} “example scheme lemma primed”]

Transitivity′′

[Transitivity′′ →^{proof} Rule tactic] [Transitivity′′ →^{stmt} T′_{E} ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} = \underline{b} ] ⊢ [ [ \underline{a} = \underline{c} ] ⊢ [ \underline{b} = \underline{c} ] ] ] ] [Transitivity′′ →^{tex} “ Transitivity’’”] [Transitivity′′ →^{pyk} “example rule lemma primed”]

Contra′′

[Contra′′ →^{proof} Rule tactic] [Contra′′ →^{stmt} T′_{E} ⊢ [ [ [ T : : T ] = T ] ⊢ ⊥ ⊥ ] ] [Contra′′ →^{tex} “ Contra’’”] [Contra′′ →^{pyk} “contraexample lemma primed”]

HeadNil

[HeadNil →^{proof} Rule tactic] [HeadNil →^{stmt} T_{E} ⊢ [ T^{h} = T ] ] [HeadNil →^{tex} “ HeadNil”] [HeadNil →^{pyk} “example axiom lemma”]

HeadPair

[HeadPair →^{proof} Rule tactic] [HeadPair →^{stmt} T_{E} ⊢ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} : : \underline{b} ] ^{h} = \underline{a} ] ] [HeadPair →^{tex} “ HeadPair”] [HeadPair →^{pyk} “example scheme lemma”]

Transitivity

[Transitivity →^{proof} Rule tactic] [Transitivity →^{stmt} T_{E} ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} = \underline{b} ] ⊢ [ [ \underline{a} = \underline{c} ] ⊢ [ \underline{b} = \underline{c} ] ] ] ] [Transitivity →^{tex} “ Transitivity”]

[Transitivity →^{pyk} “example rule lemma”]

Contra

[Contra →^{proof} Rule tactic]

[Contra →^{stmt} T_{E} ⊢ [ [ [ T : : T ] = T ] ⊢ ⊥ ⊥ ] ]

[Contra →^{tex} “ Contra”]

[Contra →^{pyk} “contraexample lemma”]

T_{E}

[T_{E} →^{stmt} [ [ [ T : : T ] = T ] ⊢ ⊥ ⊥ ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} : : \underline{b} ] ^{h} = \underline{a} ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} = \underline{b} ] ⊢ [ [ \underline{a} = \underline{c} ] ⊢ [ \underline{b} = \underline{c} ] ] ] ] ⊕ [ T^{h} = T ] ] ] ]

[T_{E} →^{tex} “

T E”]

[T_{E} →^{pyk} “example theory”]

ragged right

[ragged right →^{name} “ ragged\ right”]

[ragged right →^{tex} “ \raggedright”]

[ragged right →^{pyk} “ragged right”]

ragged right expansion

[ragged right expansion →^{name} “ ragged\ right\ expansion\ ”]

[ragged right expansion →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ragged right expansion ¨= ragged right]⌉)] [ragged right expansion →^{tex} “”]

[ragged right expansion →^{pyk} “ragged right expansion”]

parm(∗, ∗, ∗)

[parm(t, s, n) →^{val} n! If(t =^{r} ⌈∀x: y⌉, ∀n: parm(t^{2}, [ t^{1} : : n ] : : s, T +2∗ n), let_{1}(λm. If(¬m, m, t^{R} : : parm^{∗}(t^{t}, s, n)), lookup(t, s, T)))]

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

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

parm^{∗}(∗, ∗, ∗)

[parm^{∗}(t, s, n) →^{val} s! [ n!If(t^{a}, T, parm(t^{h}, s, n) : : parm^{∗}(t^{t}, s, n)) ] ]

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

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

inst(∗, ∗)

[inst(t, s) →^{val} If(t^{c}, inst(s[t], s), t^{R} : : inst^{∗}(t^{t}, s))]

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

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

inst^{∗}(∗, ∗)

[inst^{∗}(t, s) →^{val} s!If(t^{a}, T, inst(t^{h}, s) : : inst^{∗}(t^{t}, s))]

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

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

occur(∗, ∗, ∗)

[occur(t, u, s) →^{val} s!If(u^{c}, If(t ≈ u, T, occur(t, s[u], s)), occur^{∗}(t, u^{t}, s))]

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

[occur(t, u, s) →^{pyk} “occur ∗ in ∗ substitution ∗ end occur”]

occur^{∗}(∗, ∗, ∗)

[occur^{∗}(t, u, s) →^{val} t! [ s!If(u^{a}, F, If(occur(t, u^{h}, s), T, occur^{∗}(t, u^{t}, s))) ] ]

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

[occur^{∗}(t, u, s) →^{pyk} “occur star ∗ in ∗ substitution ∗ end occur”]

unify(∗ = ∗, ∗)

[unify(t = u, s) →^{val} t! [ u! If(s^{c}, s, If(t^{c}, unify_{2}(t = u, s), If(u^{c}, unify_{2}(u = t, s), If(t =^{r} u, unify^{∗}(t^{t} = u^{t}, s), 0)))) ] ] [unify(t = u, s) →^{tex} “ unify(#1. =#2. , #3. )”]

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

unify^{∗}(∗ = ∗, ∗)

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

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

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

unify_{2}(∗ = ∗, ∗)

[unify_{2}(t = u, s) →^{val} If(t ≈ u, s, let_{1}(λt′. If(¬ [ t′ ] , unify(t′ = u, s), If(occur(t, u, s), 0, s[t→u])), s[t]))]

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

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

L_{a}

[L_{a} →^{name} “L a”]

[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_{a} →^{pyk} “ell a”]

L_{b}

[L_{b} →^{name} “L b”]

[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_{b} →^{pyk} “ell b”]

L_{c}

[L_{c} →^{name} “L c”]

[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_{c} →^{pyk} “ell c”]

L_{d}

[L_{d} →^{name} “L d”]

[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_{d} →^{pyk} “ell d”]

L_{e}

[L_{e} →^{name} “L e”]

[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_{e} →^{pyk} “ell e”]

L_{f}

[L_{f} →^{name} “L f”]

[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_{f} →^{pyk} “ell f”]

L_{g}

[L_{g} →^{name} “L g”]

[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_{g} →^{pyk} “ell g”]

L_{h}

[L_{h} →^{name} “L h”]

[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_{h} →^{pyk} “ell h”]

L_{i}

[L_{i} →^{name} “L i”]

[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_{i} →^{pyk} “ell i”]

L_{j}

[L_{j} →^{name} “L j”]

[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_{j} →^{pyk} “ell j”]

L_{k}

[L_{k} →^{name} “L k”]

[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_{k} →^{pyk} “ell k”]

L_{l}

[L_{l} →^{name} “L l”]

[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_{l} →^{pyk} “ell l”]

L_{m}

[L_{m} →^{name} “L m”]

[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_{m} →^{pyk} “ell m”]

L_{n}

[L_{n} →^{name} “L n”]

[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_{n} →^{pyk} “ell n”]

L_{o}

[L_{o} →^{name} “L o”]

[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_{o} →^{pyk} “ell o”]

L_{p}

[L_{p} →^{name} “L p”]

[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_{p} →^{pyk} “ell p”]

L_{q}

[L_{q} →^{name} “L q”]

[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_{q} →^{pyk} “ell q”]

L_{r}

[L_{r} →^{name} “L r”]

[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_{r} →^{pyk} “ell r”]

L_{s}

[L_{s} →^{name} “L s”]

[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_{s} →^{pyk} “ell s”]

L_{t}

[L_{t} →^{name} “L t”]

[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_{t} →^{pyk} “ell t”]

L_{u}

[L_{u} →^{name} “L u”]

[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_{u} →^{pyk} “ell u”]

L_{v}

[L_{v} →^{name} “L v”]

[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_{v} →^{pyk} “ell v”]

L_{w}

[L_{w} →^{name} “L w”]

[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_{w} →^{pyk} “ell w”]

L_{x}

[L_{x} →^{name} “L x”]

[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_{x} →^{pyk} “ell x”]

L_{y}

[L_{y} →^{name} “L y”]

[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_{y} →^{pyk} “ell y”]

L_{z}

[L_{z} →^{name} “L z”]

[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_{z} →^{pyk} “ell z”]

L_{A}

[L_{A} →^{name} “L A”]

[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_{A} →^{pyk} “ell big a”]

L_{B}

[L_{B} →^{name} “L B”]

[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_{B} →^{pyk} “ell big b”]

L_{C}

[L_{C} →^{name} “L C”]

[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_{C} →^{pyk} “ell big c”]

L_{D}

[L_{D} →^{name} “L D”]

[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_{D} →^{pyk} “ell big d”]

L_{E}

[L_{E} →^{name} “L E”]

[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_{E} →^{pyk} “ell big e”]

L_{F}

[L_{F} →^{name} “L F”]

[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_{F} →^{pyk} “ell big f”]

L_{G}

[L_{G} →^{name} “L G”]

[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_{G} →^{pyk} “ell big g”]

L_{H}

[L_{H} →^{name} “L H”]

[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_{H} →^{pyk} “ell big h”]

L_{I}

[L_{I} →^{name} “L I”]

[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_{I} →^{pyk} “ell big i”]

L_{J}

[L_{J} →^{name} “L J”]

[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_{J} →^{pyk} “ell big j”]

L_{K}

[L_{K} →^{name} “L K”]

[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_{K} →^{pyk} “ell big k”]

L_{L}

[L_{L} →^{name} “L L”]

[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_{L} →^{pyk} “ell big l”]

L_{M}

[L_{M} →^{name} “L M”]

[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_{M} →^{pyk} “ell big m”]

L_{N}

[L_{N} →^{name} “L N”]

[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_{N} →^{pyk} “ell big n”]

L_{O}

[L_{O} →^{name} “L O”]

[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_{O} →^{pyk} “ell big o”]

L_{P}

[L_{P} →^{name} “L P”]

[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_{P} →^{pyk} “ell big p”]

L_{Q}

[L_{Q} →^{name} “L Q”]

[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_{Q} →^{pyk} “ell big q”]

L_{R}

[L_{R} →^{name} “L R”]

[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_{R} →^{pyk} “ell big r”]

L_{S}

[L_{S} →^{name} “L S”]

[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_{S} →^{pyk} “ell big s”]

L_{T}

[L_{T} →^{name} “L T”]

[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_{T} →^{pyk} “ell big t”]

L_{U}

[L_{U} →^{name} “L U”]

[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_{U} →^{pyk} “ell big u”]

L_{V}

[L_{V} →^{name} “L V”]

[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_{V} →^{pyk} “ell big v”]

L_{W}

[L_{W} →^{name} “L W”]

[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_{W} →^{pyk} “ell big w”]

L_{X}

[L_{X} →^{name} “L X”]

[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_{X} →^{pyk} “ell big x”]

L_{Y}

[L_{Y} →^{name} “L Y”]

[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_{Y} →^{pyk} “ell big y”]

L_{Z}

[L_{Z} →^{name} “L Z”]

[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_{Z} →^{pyk} “ell big z”]

L_{?}

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

[L_{?} →^{tex} “

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

[L_{?} →^{pyk} “ell dummy”]

Reflexivity

[Reflexivity →^{proof} ⌈T_{E} ⊢ ∀\underline{a}: [ [ [ HeadPair^{I}^{⊳} ^{∗}^{⊳} @ \underline{a} ] @ \underline{a} ] ; [ [ [ [ Transitivity^{I}^{⊳} ^{∗}^{⊳} @ [ [ \underline{a} : : \underline{a} ] ^{h} ] ] @ \underline{a} ] @ \underline{a} ] ^{⊳} ^{⊳} ] ] ⌉]

[Reflexivity →^{stmt} T_{E} ⊢ ∀\underline{a}: [ \underline{a} = \underline{a} ] ]

[Reflexivity →^{tex} “ Reflexivity”]

[Reflexivity →^{pyk} “sequent reflexivity”]

Reflexivity_{1}

[Reflexivity_{1} →^{proof} λc.λx.P(⌈T_{E} ⊢ ∀\underline{a}: [ [ HeadPair ≫ [ [ \underline{a} : : \underline{a} ] ^{h} = \underline{a} ] ] ; [ [ [ Transitivity ⊳ [ [ \underline{a} : : \underline{a} ] ^{h} = \underline{a} ] ] ⊳ [ [ \underline{a} : : \underline{a} ] ^{h} = \underline{a} ] ] ≫ [ \underline{a} = \underline{a} ] ] ] ⌉, p_{0}, c)] [Reflexivity_{1} →^{stmt} T_{E} ⊢ ∀\underline{a}: [ \underline{a} = \underline{a} ] ] [Reflexivity_{1} →^{tex} “ Reflexivity 1”] [Reflexivity_{1} →^{pyk} “tactic reflexivity”]

Commutativity

[Commutativity →^{proof} ⌈T_{E} ⊢ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} = \underline{b} ] ⊢ [ [ Reflexivity^{I}^{⊳} ^{∗}^{⊳} @ \underline{a} ] ; [ [ [ [ Transitivity^{I}^{⊳} ^{∗}^{⊳} @ \underline{a} ] @ \underline{b} ] @ \underline{a} ] ^{⊳} ^{⊳} ] ] ] ⌉] [Commutativity →^{stmt} T_{E} ⊢ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} = \underline{b} ] ⊢ [ \underline{b} = \underline{a} ] ] ] [Commutativity →^{tex} “ Commutativity”] [Commutativity →^{pyk} “sequent commutativity”]

Commutativity_{1}

[Commutativity_{1} →^{proof} λc.λx.P(⌈T_{E} ⊢ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} = \underline{b} ] ⊢ [ [ Reflexivity_{1} ≫ [ \underline{a} = \underline{a} ] ] ; [ [ [ Transitivity ⊳ [ \underline{a} = \underline{b} ] ] ⊳ [ \underline{a} = \underline{a} ] ] ≫ [ \underline{b} = \underline{a} ] ] ] ] ⌉, p_{0}, c)] [Commutativity_{1} →^{stmt} T_{E} ⊢ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} = \underline{b} ] ⊢ [ \underline{b} = \underline{a} ] ] ] [Commutativity_{1} →^{tex} “ Commutativity 1”] [Commutativity_{1} →^{pyk} “tactic commutativity”]

<tactic>

[<tactic> →^{val} ⌈<tactic>⌉] [<tactic> →^{tex} “ {<}tactic{>}”] [<tactic> →^{pyk} “the tactic aspect”]

tactic

[tactic →^{msg} <tactic>]

[tactic →^{tex} “ tactic”]

[tactic →^{pyk} “tactic”]

[∗ =^{tactic} ∗]

[[x =^{tactic} y] →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[[x =^{tactic} y] ¨= [(x)^{p} →^{tactic} y]]⌉)]

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

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

P(∗, ∗, ∗)

[P(t, s, c) →^{val} s!

let_{1}(λd. If(d, t^{h} : : P^{∗}(t^{t}, s, c), U^{M}( [ [ E(d^{3}, T, c) ‘ t ] ‘ s ] ‘ c)), aspect(<tactic>, t, c))]

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

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

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

P^{∗}(∗, ∗, ∗)

[P^{∗}(t, s, c) →^{val} s! [ c!If(t, T, P(t^{h}, s, c) : : P^{∗}(t^{t}, s, c)) ] ]

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

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

)”]

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

p_{0}

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

[p_{0} →^{tex} “

p 0”]

[p_{0} →^{pyk} “proof state”]

conclude_{1}(∗, ∗)

[conclude_{1}(t, c) →^{val} let_{1}(λr. If(r^{c}, error_{2}(⌈“Unification failed”⌉, t), r), conclude_{2}(t^{1}, t^{2}, c))]

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

[conclude_{1}(t, c) →^{pyk} “conclude one ∗ cache ∗ end conclude”]

conclude_{2}(∗, ∗, ∗)

[conclude_{2}(a, t, c) →^{val} t! If(a =^{r} ⌈x ⊳ y⌉, conclude_{2}(a^{1}, a-color(t ⊳ [ a^{2} ] ), c), If(a =^{r} ⌈x ⊳ ⊳ y⌉, conclude_{2}(a^{1}, a-color(t ⊳ ⊳ [ a^{2} ] ), c), If(a =^{r} ⌈x @ y⌉, conclude_{2}(a^{1}, a-color(t @ [ a^{2} ] ), c), If(aspect(<proof>, a, c), error_{2}(⌈“Lemma expected”⌉, a), let_{1}(λd. conclude_{3}(a-color(conclude_{4}(a^{I}^{⊳} ^{∗}^{⊳} , d^{3}^{2})), t, parm(d^{3}^{2}, T, 1), T), aspect(<stmt>, a, c))))))]

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

[conclude_{2}(a, t, c) →^{pyk} “conclude two ∗ proves ∗ cache ∗ end conclude”]

conclude_{3}(∗, ∗, ∗, ∗)

[conclude_{3}(a, t, l, s) →^{val} a! [ t! [ l! [ s!

If(l =^{r} ⌈x ⊢ y⌉, [ [

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

If(l =^{r} ⌈x ⊢⊢ y⌉, [ [

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

If(l =^{r} ⌈∀x: y⌉, [ [

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

let_{1}(λs. If(s^{c}, s, inst(a, s)), unify(l = t, s))))) ] ] ] ]

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

[conclude_{3}(a, t, l, s) →^{pyk} “conclude three ∗ proves ∗ lemma ∗ substitution ∗ end conclude”]

conclude_{4}(∗, ∗)

[conclude_{4}(a, l) →^{val} a! [ l!

If(¬ [ l =^{r} ⌈∀x: y⌉ ] , a,

let_{1}(λv.∀v: conclude_{4}(a @ v, l^{2}), ⌈\underline{∗}⌉^{R} : : [ l^{1} : : T ] )) ] ]

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

[conclude_{4}(a, l) →^{pyk} “conclude four ∗ lemma ∗ end conclude”]

∗ {∗}

[∗ {∗} →^{name} “#1.

\ \{#2.

\}”]

[∗ {∗} →^{tex} “#1.

{#2. }”]

[∗ {∗} →^{pyk} “∗ sub ∗ end sub”]

∗′

[x′ →^{tex} “#1.’”]

[x′ →^{pyk} “∗ prime”]

∗[ ∗]

[a[k] →^{val} assoc_{1}(a, k, k)]

[∗[ ∗] →^{tex} “#1.

{[}#2. {]}”]

[∗[ ∗] →^{pyk} “∗ assoc ∗ end assoc”]

∗[∗→∗]

[a[i→v] →^{val} i^{c} \{ \begin{matrix}v \{ \begin{matrix}array-remove(i, a, 0) \\ array-put(i, v, a, 0) \end{matrix} \\ v!a \end{matrix} ]

[a[i→v] →^{tex} “#1.

[ #2. {\rightarrow} #3. ]”]

[a[i→v] →^{pyk} “∗ set ∗ to ∗ end set”]

∗[∗⇒∗]

[a[i⇒v] →^{val} i^{a} \{ \begin{matrix}a!v \\ a[i^{h}→a[i^{h}][i^{t}⇒v]] \end{matrix} ]

[a[i⇒v] →^{tex} “#1.

[ #2. {\Rightarrow} #3. ]”]

[a[i⇒v] →^{pyk} “∗ set multi ∗ to ∗ end set”]

newline ∗

[newline x →^{name} “ newline\ #1.”]

[newline x →^{val} x^{M}]

[newline x →^{tex} “ \newline #1.”]

[newline x →^{pyk} “newline ∗”]

macro newline ∗

[macro newline x →^{name} “ macro\ newline\ #1.”]

[macro newline x →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[macro newline x ¨= x]⌉)]

[macro newline x →^{tex} “ \newline #1.”]

[macro newline x →^{pyk} “macro newline ∗”]

∗0

[x0 →^{val} T +2∗ x]

[∗0 →^{tex} “#1.

0”]

[∗0 →^{pyk} “∗ bit nil”]

∗1

[x1 →^{val} F +2∗ x]

[∗1 →^{tex} “#1.

1”] [∗1 →^{pyk} “∗ bit one”]

0b

[0b →^{val} 0]

[0b →^{tex} “

0 \mathrm {b}”]

[0b →^{pyk} “binary”]

∗-color(∗)

[a-color(t) →^{val} t^{d} \{ \begin{matrix}[ t^{r} : : [ t^{i} : : [ a^{d} ] ] ] : : [ a-color^{∗}(t^{t}) ] \\ a!t \end{matrix} ]

[x-color(y) →^{tex} “#1. \mbox {-color}( #2. )”]

[x-color(y) →^{pyk} “∗ color ∗ end color”]

∗-color^{∗}(∗)

[a-color^{∗}(t) →^{val} t \{ \begin{matrix}a!T \\ a-color(t^{h}) : : [ a-color^{∗}(t^{t}) ] \end{matrix} ]

[x-color^{∗}(y) →^{tex} “#1. \mbox {-color}ˆ {\ast}( #2. )”]

[x-color^{∗}(y) →^{pyk} “∗ color star ∗ end color”]

∗ ’ ∗

Predef: apply

[∗ ’ ∗ →^{tex} “#1.

\mathbin {\mbox {’}}#2.”]

[∗ ’ ∗ →^{pyk} “∗ apply ∗”]

∗ ‘ ∗

[f ‘ x →^{val} apply(f, x)]

[∗ ‘ ∗ →^{tex} “#1.

\mathbin {\mbox {‘}}#2.”]

[∗ ‘ ∗ →^{pyk} “∗ tagged apply ∗”]

∗^{H}

[x^{H} →^{val} x ’ T]

[∗^{H} →^{tex} “#1.

{}ˆ H”]

[∗^{H} →^{pyk} “∗ raw head”]

∗^{T}

[x^{T} →^{val} x ’ F]

[∗^{T} →^{tex} “#1.

{}ˆ T”]

[∗^{T} →^{pyk} “∗ raw tail”]

∗^{U}

[x^{U} →^{val} if(x^{H}, x^{T}, T)]

[∗^{U} →^{tex} “#1.

{}ˆ U”]

[∗^{U} →^{pyk} “∗ cardinal untag”]

∗^{h}

[x^{h} ⇒^{val} x^{M}^{T}^{H}]

[∗^{h} →^{tex} “#1.

{}ˆ h”]

[∗^{h} →^{pyk} “∗ head”]

∗^{t}

[x^{t} ⇒^{val} if(x^{d}, if(x^{c}, T \underline{˙. .} [ x^{M}^{T}^{T} ] , x^{M}^{T}^{T}), T)]

[∗^{t} →^{tex} “#1.

{}ˆ t”]

[∗^{t} →^{pyk} “∗ tail”]

∗^{s}

[x^{s} ⇒^{val} x^{M}^{T}^{B}]

[∗^{s} →^{tex} “#1.

{}ˆ s”]

[∗^{s} →^{pyk} “∗ is singular”]

∗^{c}

[x^{c} ⇒^{val} if(x, F, x^{M}^{H}^{B})]

[∗^{c} →^{tex} “#1.

{}ˆ c”]

[∗^{c} →^{pyk} “∗ is cardinal”]

∗^{d}

[x^{d} ⇒^{val} x^{M}^{H}^{T}^{H}^{B}]

[∗^{d} →^{tex} “#1.

{}ˆ d”]

[∗^{d} →^{pyk} “∗ is data”]

∗^{a}

[x^{a} →^{val} [ [ ¬ [ x^{d} ] ] ∨ [ x^{c} ] ] ∨ [ x^{s} ] ]

[∗^{a} →^{tex} “#1.

{}ˆ a”]

[∗^{a} →^{pyk} “∗ is atomic”]

∗^{C}

[x^{C} →^{val} if(x, T, x^{H}^{B} \underline{+2∗} [ x^{T}^{C} ] )]

[∗^{C} →^{tex} “#1.

{}ˆ C”]

[∗^{C} →^{pyk} “∗ cardinal retract”]

∗^{M}

[x^{M} ⇒^{val} if(x, T, if(x^{H}, T \underline{˙. .} [ x^{T}^{C} ] , if(x^{H}^{T}^{H}, x^{T}^{H}^{M} \underline{: :} [ x^{T}^{T}^{M} ] , M(x^{T}))))]

[∗^{M} →^{tex} “#1.

{}ˆ M”]

[∗^{M} →^{pyk} “∗ tagged retract”]

∗^{B}

[x^{B} →^{val} if(x, T, F)]

[∗^{B} →^{tex} “#1.

{}ˆ B”]

[∗^{B} →^{pyk} “∗ boolean retract”]

∗^{r}

[x^{r} →^{val} x^{h}^{h}]

[x^{r} →^{tex} “#1.

{}ˆ {r}”]

[x^{r} →^{pyk} “∗ ref”]

∗^{i}

[x^{i} →^{val} x^{h}^{t}^{h}]

[x^{i} →^{tex} “#1.

{}ˆ {i}”]

[x^{i} →^{pyk} “∗ id”]

∗^{d}

[x^{d} →^{val} x^{h}^{t}^{t}]

[x^{d} →^{tex} “#1.

{}ˆ {d}”]

[x^{d} →^{pyk} “∗ debug”]

∗^{R}

[x^{R} →^{val} x^{r} : : [ x^{i} : : T ] ]

[x^{R} →^{tex} “#1.

{}ˆ {R}”]

[x^{R} →^{pyk} “∗ root”]

∗^{0}

[x^{0} →^{val} x^{h}]

[x^{0} →^{tex} “#1.

{}ˆ {0}”]

[x^{0} →^{pyk} “∗ zeroth”]

∗^{1}

[x^{1} →^{val} x^{t}^{0}]

[x^{1} →^{tex} “#1.

{}ˆ {1}”]

[x^{1} →^{pyk} “∗ first”]

∗^{2}

[x^{2} →^{val} x^{t}^{1}]

[x^{2} →^{tex} “#1.

{}ˆ {2}”]

[x^{2} →^{pyk} “∗ second”]

∗^{3}

[x^{3} →^{val} x^{t}^{2}]

[x^{3} →^{tex} “#1.

{}ˆ {3}”]

[x^{3} →^{pyk} “∗ third”]

∗^{4}

[x^{4} →^{val} x^{t}^{3}]

[x^{4} →^{tex} “#1.

{}ˆ {4}”]

[x^{4} →^{pyk} “∗ fourth”]

∗^{5}

[x^{5} →^{val} x^{t}^{4}]

[x^{5} →^{tex} “#1.

{}ˆ {5}”]

[x^{5} →^{pyk} “∗ fifth”]

∗^{6}

[x^{6} →^{val} x^{t}^{5}]

[x^{6} →^{tex} “#1.

{}ˆ {6}”]

[x^{6} →^{pyk} “∗ sixth”]

∗^{7}

[x^{7} →^{val} x^{t}^{6}]

[x^{7} →^{tex} “#1.

{}ˆ {7}”]

[x^{7} →^{pyk} “∗ seventh”]

∗^{8}

[x^{8} →^{val} x^{t}^{7}]

[x^{8} →^{tex} “#1.

{}ˆ {8}”]

[x^{8} →^{pyk} “∗ eighth”]

∗^{9}

[x^{9} →^{val} x^{t}^{8}]

[x^{9} →^{tex} “#1.

{}ˆ {9}”]

[x^{9} →^{pyk} “∗ ninth”]

∗^{E}

[x^{E} →^{val} x =^{r} ⌈xy⌉]

[x^{E} →^{tex} “#1.

{} ˆ { E }”]

[x^{E} →^{pyk} “∗ is error”]

∗^{V}

[t^{V} →^{val} t =^{r} ⌈\underline{a}⌉]

[t^{V} →^{tex} “#1.

{} ˆ {\cal V}”]

[t^{V} →^{pyk} “∗ is metavar”]

∗^{C}

[t^{C} →^{val} If(t^{V}, F, t^{t}^{C^{∗}})]

[t^{C} →^{tex} “#1.

{} ˆ {\cal C}”]

[t^{C} →^{pyk} “∗ is metaclosed”]

∗^{C^{∗}}

[t^{C^{∗}} →^{val} If(t, T, If(t^{h}^{C}, t^{t}^{C^{∗}}, F))]

[t^{C^{∗}} →^{tex} “#1.

{} ˆ {{\cal C} ˆ { \ast }}”]

[t^{C^{∗}} →^{pyk} “∗ is metaclosed star”]

∗ · ∗

[x · y →^{val} If(x^{c} ∧ [ y^{c} ] , x ·_{0} y, T)]

[x · y →^{tex} “#1.

\cdot #2.”]

[x · y →^{pyk} “∗ times ∗”]

∗ ·_{0} ∗

[x ·_{0} y →^{val} y^{s} \{ \begin{matrix}x!0 \\ y^{h} \{ \begin{matrix}T +2∗ [ x ·_{0} [ y^{t} ] ] \\ (T +2∗ [ x ·_{0} [ y^{t} ] ] )^{M} +_{0} x \end{matrix} \end{matrix} ]

[x ·_{0} y →^{tex} “#1.

\cdot 0 #2.”]

[x ·_{0} y →^{pyk} “∗ times zero ∗”]

∗ + ∗

[x + y →^{val} If(x^{c} ∧ [ y^{c} ] , x +_{0} y, T)]

[x + y →^{tex} “#1.

+ #2.”]

[x + y →^{pyk} “∗ plus ∗”]

∗ +_{0} ∗

[x +_{0} y →^{val} x^{s} \{ \begin{matrix}y \\ y^{s} \{ \begin{matrix}x \\ x^{h} \{ \begin{matrix}y^{h} \{ \begin{matrix}T +2∗ [ x^{t} +_{0} [ y^{t} ] ] \\ F +2∗ [ x^{t} +_{0} [ y^{t} ] ] \end{matrix} \\ y^{h} \{ \begin{matrix}F +2∗ [ x^{t} +_{0} [ y^{t} ] ] \\ T +2∗ [ x^{t} +_{1} [ y^{t} ] ] \end{matrix} \end{matrix} \end{matrix} \end{matrix} ]

[x +_{0} y →^{tex} “#1.

\mathop{+ 0} #2.”]

[x +_{0} y →^{pyk} “∗ plus zero ∗”]

∗ +_{1} ∗

[x +_{1} y →^{val} x^{s} \{ \begin{matrix}y +_{0} 1 \\ y^{s} \{ \begin{matrix}x +_{0} 1 \\ x^{h} \{ \begin{matrix}y^{h} \{ \begin{matrix}F +2∗ [ x^{t} +_{0} [ y^{t} ] ] \\ T +2∗ [ x^{t} +_{1} [ y^{t} ] ] \end{matrix} \\ y^{h} \{ \begin{matrix}T +2∗ [ x^{t} +_{1} [ y^{t} ] ] \\ F +2∗ [ x^{t} +_{1} [ y^{t} ] ] \end{matrix} \end{matrix} \end{matrix} \end{matrix} ]

[x +_{1} y →^{tex} “#1.

\mathop{+ 1} #2.”]

[x +_{1} y →^{pyk} “∗ plus one ∗”]

∗ − ∗

[x − y →^{val} If(x^{c} ∧ [ y^{c} ] , If(x < y, 0, x −_{0} y), T)]

[x − y →^{tex} “#1.

- #2.”]

[x − y →^{pyk} “∗ minus ∗”]

∗ −_{0} ∗

[x −_{0} y →^{val} y^{s} \{ \begin{matrix}x \\ x^{h} \{ \begin{matrix}y^{h} \{ \begin{matrix}T +2∗ [ x^{t} −_{0} [ y^{t} ] ] \\ F +2∗ [ x^{t} −_{1} [ y^{t} ] ] \end{matrix} \\ y^{h} \{ \begin{matrix}F +2∗ [ x^{t} −_{0} [ y^{t} ] ] \\ T +2∗ [ x^{t} −_{0} [ y^{t} ] ] \end{matrix} \end{matrix} \end{matrix} ]

[x −_{0} y →^{tex} “#1.

\mathop{- 0} #2.”]

[x −_{0} y →^{pyk} “∗ minus zero ∗”]

∗ −_{1} ∗

[x −_{1} y →^{val} y^{s} \{ \begin{matrix}x −_{0} 1 \\ x^{h} \{ \begin{matrix}y^{h} \{ \begin{matrix}F +2∗ [ x^{t} −_{1} [ y^{t} ] ] \\ T +2∗ [ x^{t} −_{1} [ y^{t} ] ] \end{matrix} \\ y^{h} \{ \begin{matrix}T +2∗ [ x^{t} −_{0} [ y^{t} ] ] \\ F +2∗ [ x^{t} −_{1} [ y^{t} ] ] \end{matrix} \end{matrix} \end{matrix} ]

[x −_{1} y →^{tex} “#1.

\mathop{- 1} #2.”]

[x −_{1} y →^{pyk} “∗ minus one ∗”]

∗ ∪ {∗}

[x ∪ {y} →^{val} If(y ∈_{t} x, x, y : : x)]

[x ∪ {y} →^{tex} “#1.

\cup \{ #2. \}”]

[x ∪ {y} →^{pyk} “∗ term plus ∗ end plus”]

∗ ∪ ∗

[x ∪ y →^{val} If(x^{a}, y, [ x^{t} ∪ y ] ∪ {x^{h}})]

[x ∪ y →^{tex} “#1.

\cup #2.”]

[x ∪ y →^{pyk} “∗ term union ∗”]

∗\{∗}

[x\{y} →^{val} If(x^{a}, y!∅, If(y =^{t} [ x^{h} ] , x^{t}, x^{h} : : [ x^{t}\{y} ] ))]

[x\{y} →^{tex} “#1.

\backslash \{ #2.

[x\{y} →^{pyk} “∗ term minus ∗ end minus”]

∗ ˙. . ∗

[y ˙. . z ⇒^{val} λx.if(x, y, z)]

[∗ ˙. . ∗ →^{tex} “#1.

\mathrel { \dot { . \, . } }#2.”]

[∗ ˙. . ∗ →^{pyk} “∗ raw pair ∗”]

∗ \underline{˙. .} ∗

[x \underline{˙. .} y →^{val} x : [ y : [ x ˙. . y ] ] ]

[∗ \underline{˙. .} ∗ →^{tex} “#1.

\mathrel { \underline { \dot { . \, . } } }#2.”]

[∗ \underline{˙. .} ∗ →^{pyk} “∗ eager pair ∗”]

∗ \underline{: :} ∗

[x \underline{: :} y →^{val} (\underline{0} \underline{˙. .} [ \underline{0} \underline{˙. .} T ] )^{I} \underline{˙. .} [ x \underline{˙. .} y ] ]

[∗ \underline{: :} ∗ →^{tex} “#1.

\mathrel { \underline { : \, : } }#2.”]

[∗ \underline{: :} ∗ →^{pyk} “∗ tagged pair ∗”]

∗ \underline{+2∗} ∗

[x \underline{+2∗} y →^{val} if(x, if(y, T, x \underline{˙. .} y), x \underline{˙. .} y)]

[∗ \underline{+2∗} ∗ →^{tex} “#1.

\mathrel { \underline { {+} 2 \ast } }#2.”]

[∗ \underline{+2∗} ∗ →^{pyk} “∗ untagged double ∗”]

∗ : : ∗

[x : : y ⇒^{val} x^{M} \underline{: :} [ y^{M} ] ]

[x : : y →^{tex} “#1.

\mathrel { : \, : }#2.”]

[∗ : : ∗ →^{pyk} “∗ pair ∗”]

∗ +2∗ ∗

[x +2∗ y ⇒^{val} T \underline{˙. .} [ x^{B} \underline{˙. .} [ y^{U}^{C} ] ] ]

[∗ +2∗ ∗ →^{tex} “#1.

\mathrel { {+} 2 \ast }#2.”]

[∗ +2∗ ∗ →^{pyk} “∗ double ∗”]

∗, ∗

[x, y →^{tex} “#1.

, \linebreak [0] #2.”]

[x, y →^{pyk} “∗ comma ∗”]

∗ ≈^{B} ∗

[x ≈^{B} y →^{val} x \{ \begin{matrix}If(y, T, F) \\ If(y, F, T) \end{matrix} ]

[∗ ≈^{B} ∗ →^{tex} “#1.

\stackrel {B}{\approx }#2.”]

[∗ ≈^{B} ∗ →^{pyk} “∗ boolean equal ∗”]

∗ ≈^{D} ∗

[x ≈^{D} y →^{val} x^{c} \{ \begin{matrix}If(y^{c}, x ≈^{C} y, F) \\ If(y^{c}, F, x ≈^{P} y) \end{matrix} ]

[∗ ≈^{D} ∗ →^{tex} “#1.

\stackrel {D}{\approx }#2.”] [∗ ≈^{D} ∗ →^{pyk} “∗ data equal ∗”]

∗ ≈^{C} ∗

[x ≈^{C} y →^{val} x^{s} \{ \begin{matrix}If(y^{s}, T, F) \\ If(y^{s}, F, [ x^{h} ≈^{B} [ y^{h} ] ] ∧ [ x^{t} ≈^{C} [ y^{t} ] ] ) \end{matrix} ]

[∗ ≈^{C} ∗ →^{tex} “#1.

\stackrel {C}{\approx }#2.”]

[∗ ≈^{C} ∗ →^{pyk} “∗ cardinal equal ∗”]

∗ ≈^{P} ∗

[x ≈^{P} y →^{val} x^{s} \{ \begin{matrix}If(y^{s}, T, F) \\ If(y^{s}, F, [ x^{h} ≈ [ y^{h} ] ] ∧ [ x^{t} ≈ [ y^{t} ] ] ) \end{matrix} ]

[∗ ≈^{P} ∗ →^{tex} “#1.

\stackrel {P}{\approx }#2.”]

[∗ ≈^{P} ∗ →^{pyk} “∗ peano equal ∗”]

∗ ≈ ∗

[x ≈ y ⇒^{val} x^{d} \{ \begin{matrix}If(y^{d}, x ≈^{D} y, F) \\ If(y^{d}, F, T) \end{matrix} ]

[∗ ≈ ∗ →^{tex} “#1.

\approx #2.”]

[∗ ≈ ∗ →^{pyk} “∗ tagged equal ∗”]

∗ = ∗

[∗ = ∗ →^{tex} “#1.

=#2.”]

[∗ = ∗ →^{pyk} “∗ math equal ∗”]

∗ →^{+} ∗

[∗ →^{+} ∗ →^{tex} “#1.

\stackrel {+}{\rightarrow }#2.”]

[∗ →^{+} ∗ →^{pyk} “∗ reduce to ∗”]

∗ =^{t} ∗

[x =^{t} y →^{val} If(x =^{r} y, x^{t} =^{t^{∗}} [ y^{t} ] , F)]

[∗ =^{t} ∗ →^{tex} “#1.

\stackrel {t}{=}#2.”]

[∗ =^{t} ∗ →^{pyk} “∗ term equal ∗”]

∗ =^{t^{∗}} ∗

[x =^{t^{∗}} y →^{val} x^{a} \{ \begin{matrix}If(y^{a}, T, F) \\ If(y^{a}, F, If(x^{h} =^{t} [ y^{h} ] , x^{t} =^{t^{∗}} [ y^{t} ] , F)) \end{matrix} ]

[∗ =^{t^{∗}} ∗ →^{tex} “#1.

\stackrel {tˆ ∗}{=}#2.”]

[∗ =^{t^{∗}} ∗ →^{pyk} “∗ term list equal ∗”]

∗ =^{r} ∗

[x =^{r} y →^{val} If(x^{r} ≈ [ y^{r} ] , x^{i} ≈ [ y^{i} ] , F)]

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

\stackrel{r}{=} #2.”]

[x =^{r} y →^{pyk} “∗ term root equal ∗”]

∗ ∈_{t} ∗

[x ∈_{t} y →^{val} If(y^{a}, x!F, If(x =^{t} [ y^{h} ] , T, x ∈_{t} [ y^{t} ] ))]

[x ∈_{t} y →^{tex} “#1.

\in t #2.”]

[x ∈_{t} y →^{pyk} “∗ term in ∗”]

∗ ⊆_{T} ∗

[x ⊆_{T} y →^{val} If(x^{a}, y!T, If(x^{h} ∈_{t} y, x^{t} ⊆_{T} y, F))]

[x ⊆_{T} y →^{tex} “#1.

\subseteq T #2.”]

[x ⊆_{T} y →^{pyk} “∗ term subset ∗”]

∗ =^{T} ∗

[x =^{T} y →^{val} If(x ⊆_{T} y, y ⊆_{T} x, F)]

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

\stackrel{T}{=} #2.”]

[x =^{T} y →^{pyk} “∗ term set equal ∗”]

∗ =^{s} ∗

[x =^{s} y →^{val} If(¬ [ x^{2} =^{t} [ y^{2} ] ] , F, If(x^{0} =^{T} [ y^{0} ] , x^{1} =^{T} [ y^{1} ] , F))]

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

\stackrel{s}{=} #2.”]

[x =^{s} y →^{pyk} “∗ sequent equal ∗”]

∗ free in ∗

[v free in t →^{val}

If(v =^{t} t, T,

If(¬ [ t =^{r} ⌈∀∗: ∗⌉ ] , v free in^{∗} [ t^{t} ] , If(v =^{t} [ t^{1} ] , F, v free in [ t^{2} ] )))]

[x free in y →^{tex} “#1. \mathrel {free\ in} #2.”]

[v free in t →^{pyk} “∗ free in ∗”]

∗ free in^{∗} ∗

[v free in^{∗} t →^{val} If(t, v!F, If(v free in [ t^{h} ] , T, v free in^{∗} [ t^{t} ] ))] [x free in^{∗} y →^{tex} “#1. \mathrel {free\ in}ˆ {\ast} #2.”]

[v free in^{∗} t →^{pyk} “∗ free in star ∗”]

∗ free for ∗ in ∗

[a free for x in b →^{val} a! [ x! If(b^{V}, T, If(¬ [ b =^{r} ⌈∀∗: ∗⌉ ] , a free for^{∗} x in [ b^{t} ] ,

If(x =^{t} [ b^{1} ] , T,

If(¬ [ x free in [ b^{2} ] ] , T, If(b^{1} free in a, F, [ a ] free for x in [ b^{2} ] ))))) ] ]

[a free for x in b →^{tex} “#1. \mathrel {free\ for} #2. \mathrel {in} #3.”]

[a free for x in b →^{pyk} “∗ free for ∗ in ∗”]

∗ free for^{∗} ∗ in ∗

[a free for^{∗} x in b →^{val} If(b, a! [ x!T ] , If(a free for x in [ b^{h} ] , a free for^{∗} x in [ b^{t} ] , F))]

[a free for^{∗} x in b →^{tex} “#1. \mathrel {free\ for}ˆ {\ast} #2. \mathrel {in} #3.”]

[a free for^{∗} ∗ in b →^{pyk} “∗ free for star ∗ in ∗”]

∗ ∈_{c} ∗

[x ∈_{c} y →^{val} [ y =^{r} ⌈x ∧_{c} y⌉ ] \{ \begin{matrix}If(x ∈_{c} [ y^{1} ] , T, x ∈_{c} [ y^{2} ] ) \\ x =^{t} y \end{matrix} ]

[x ∈_{c} y →^{tex} “#1.

\in c #2.”]

[x ∈_{c} y →^{pyk} “∗ claim in ∗”]

∗ < ∗

[x < y →^{val} If(x^{c} ∧ [ y^{c} ] , x <′ y, F)]

[x < y →^{tex} “#1.

< #2.”]

[x < y →^{pyk} “∗ less ∗”]

∗ <′ ∗

[x <′ y →^{val} y^{s} \{ \begin{matrix}x!F \\ x^{s} \{ \begin{matrix}T \\ x^{h} \{ \begin{matrix}y^{h} \{ \begin{matrix}x^{t} <′ [ y^{t} ] \\ x^{t} ≤′ [ y^{t} ] \end{matrix} \\ y^{h} \{ \begin{matrix}x^{t} <′ [ y^{t} ] \\ x^{t} <′ [ y^{t} ] \end{matrix} \end{matrix} \end{matrix} \end{matrix} ]

[x <′ y →^{tex} “#1.

<’ #2.”]

[x <′ y →^{pyk} “∗ less zero ∗”]

∗ ≤′ ∗

[x ≤′ y →^{val} x^{s} \{ \begin{matrix}y!T \\ y^{s} \{ \begin{matrix}F \\ x^{h} \{ \begin{matrix}y^{h} \{ \begin{matrix}x^{t} ≤′ [ y^{t} ] \\ x^{t} ≤′ [ y^{t} ] \end{matrix} \\ y^{h} \{ \begin{matrix}x^{t} <′ [ y^{t} ] \\ x^{t} ≤′ [ y^{t} ] \end{matrix} \end{matrix} \end{matrix} \end{matrix} ]

[x ≤′ y →^{tex} “#1.

\le’ #2.”]

[x ≤′ y →^{pyk} “∗ less one ∗”]

¬∗

[¬x →^{val} If(x, F, T)]

[¬∗ →^{tex} “

{\neg }#1.”]

[¬∗ →^{pyk} “not ∗”]

∗ ∧ ∗

[x ∧ y →^{val} x \{ \begin{matrix}If(y, T, F) \\ If(y, F, F) \end{matrix} ]

[∗ ∧ ∗ →^{tex} “#1.

\wedge #2.”]

[∗ ∧ ∗ →^{pyk} “∗ and ∗”]

∗ ¨∧ ∗

[x ¨∧ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ¨∧ y ¨= If(x, y, F)]⌉)]

[x ¨∧ y →^{tex} “#1.

\mathrel{\ddot{\wedge}} #2.”]

[x ¨∧ y →^{pyk} “∗ macro and ∗”]

∗ ˜∧ ∗

[x ˜∧ y →^{val} if(x, y, x)]

[x ˜∧ y →^{tex} “#1.

\mathrel{\tilde{\wedge}} #2.”]

[x ˜∧ y →^{pyk} “∗ simple and ∗”]

∗ ∧_{c} ∗

[x ∧_{c} y →^{val} λt.λc. [ [ [ x ’ t ] ’ c ] ˜∧ [ [ y ’ t ] ’ c ] ] ]

[x ∧_{c} y →^{tex} “#1.

\wedge c #2.”]

[x ∧_{c} y →^{pyk} “∗ claim and ∗”]

∗ ∨ ∗

[x ∨ y →^{val} x \{ \begin{matrix}If(y, T, T) \\ If(y, T, F) \end{matrix} ]

[∗ ∨ ∗ →^{tex} “#1.

\vee #2.”]

[∗ ∨ ∗ →^{pyk} “∗ or ∗”]

∗ ∥ ∗

[∗ ∥ ∗ →^{tex} “#1.

\parallel #2.”] [∗ ∥ ∗ →^{pyk} “∗ parallel ∗”]

∗ ¨∨ ∗

[x ¨∨ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ¨∨ y ¨= If(x, T, y)]⌉)]

[x ¨∨ y →^{tex} “#1.

\mathrel{\ddot{\vee}} #2.”] [x ¨∨ y →^{pyk} “∗ macro or ∗”]

∗ ¨⇒ ∗

[x ¨⇒ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ¨⇒ y ¨= If(x, y, T)]⌉)]

[x ¨⇒ y →^{tex} “#1.

\mathrel{\ddot{\Rightarrow}} #2.”] [x ¨⇒ y →^{pyk} “∗ macro imply ∗”]

∗ : ∗

[x : y →^{val} if(x, y, y)]

[∗ : ∗ →^{tex} “#1.

:#2.”] [∗ : ∗ →^{pyk} “∗ guard ∗”]

∗!∗

[x!y ⇒^{val} If(x, y, y)]

[∗!∗ →^{tex} “#1.

!#2.”] [∗!∗ →^{pyk} “∗ tagged guard ∗”]

∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix}

[x \{ \begin{matrix}y \\ z \end{matrix} ⇒^{val} If(x, y, z)]

[∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix} →^{tex} “#1.

\left\{\protect \begin {array}{l}#2. \\#3. \protect \end {array}\right.”]

[∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix} →^{pyk} “∗ select ∗ else ∗ end select”]

λ ∗ .∗

Predef: lambda

[λ ∗ .∗ →^{tex} “

\lambda #1. .#2.”]

[λ ∗ .∗ →^{pyk} “lambda ∗ dot ∗”]

Λ∗

[Λx ⇒^{val} M(λu.U(x ’ M(u)))]

[Λ∗ →^{tex} “

\Lambda #1.”]

[Λ∗ →^{pyk} “tagging ∗”]

if ∗ then ∗ else ∗

[if x then y else z →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[if x then y else z ¨= If(x, y, z)]⌉)]

[if x then y else z →^{tex} “ {\bf if} \ #1. \ {\bf then} \ #2. \ {\bf else} \ #3.”] [if x then y else z →^{pyk} “open if ∗ then ∗ else ∗”]

let ∗ = ∗ in ∗

[let x = y in z →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[let x = y in z ¨= let_{1}(λx.z, y)]⌉)]

[let x = y in z →^{tex} “ \mathbf{let\ } #1. = #2. \mathbf{\ in\ } #3.”]

[let x = y in z →^{pyk} “let ∗ be ∗ in ∗”]

let ∗ ¨= ∗ in ∗

[let x ¨= y in z →^{macro} λt.λs.λc. M̃(t^{3}, s, c[t^{1}^{r} : : [ "codex" : : [ t^{1}^{r} : : [ t^{1}^{i} : : [ 0 : : [ "macro" : : T ] ] ] ] ] ⇒M̃_{3}(t)])]

[let x ¨= y in z →^{tex} “ \mathbf{let\ } #1. \mathrel{\ddot{=}} #2. \mathrel{\ in\ } #3.”]

[let x ¨= y in z →^{pyk} “let ∗ abbreviate ∗ in ∗”]

∗^{I}

[x^{I} →^{val} ⌈x^{I}⌉^{R} : : [ x : : T ] ]

[x^{I} →^{tex} “#1.

{} ˆ { I }”]

[x^{I} →^{pyk} “∗ init”]

∗^{⊳}

[x^{⊳} →^{val} ⌈x^{⊳} ⌉^{R} : : [ x : : T ] ]

[x^{⊳} →^{tex} “#1.

{} ˆ { \rhd }”]

[x^{⊳} →^{pyk} “∗ modus”]

∗^{V}

[x^{V} →^{val} ⌈x^{V}⌉^{R} : : [ x : : T ] ]

[x^{V} →^{tex} “#1.

{} ˆ { V } ”] [x^{V} →^{pyk} “∗ verify”]

∗^{+}

[x^{+} →^{val} ⌈x^{+}⌉^{R} : : [ x : : T ] ]

[x^{+} →^{tex} “#1.

{} ˆ { + } ”] [x^{+} →^{pyk} “∗ curry plus”]

∗^{−}

[x^{−} →^{val} ⌈x^{−}⌉^{R} : : [ x : : T ] ]

[x^{−} →^{tex} “#1.

{} ˆ { - } ”] [x^{−} →^{pyk} “∗ curry minus”]

∗^{∗}

[x^{∗} →^{val} ⌈x^{∗}⌉^{R} : : [ x : : T ] ]

[x^{∗} →^{tex} “#1.

{} ˆ { \ast } ”] [x^{∗} →^{pyk} “∗ dereference”]

∗ @ ∗

[x @ y →^{val} ⌈x @ y⌉^{R} : : [ x : : [ y : : T ] ] ]

[x @ y →^{tex} “#1.

\mathop {\char64} #2.”]

[x @ y →^{pyk} “∗ at ∗”]

∗ ⊳ ∗

[x ⊳ y →^{val} ⌈x ⊳ y⌉^{R} : : [ x : : [ y : : T ] ] ]

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

\rhd #2.”] [x ⊳ y →^{pyk} “∗ modus ponens ∗”]

∗ ⊳ ⊳ ∗

[x ⊳ ⊳ y →^{val} ⌈x ⊳ ⊳ y⌉^{R} : : [ x : : [ y : : T ] ] ]

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

\mathrel {\makebox [0mm][l]{$\rhd $}\, {\rhd }} #2.”] [x ⊳ ⊳ y →^{pyk} “∗ modus probans ∗”]

∗ ≫ ∗

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

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

\gg #2.”] [x ≫ y →^{pyk} “∗ conclude ∗”]

∗ ⊢ ∗

[x ⊢ y →^{val} ⌈x ⊢ y⌉^{R} : : [ x : : [ y : : T ] ] ]

[x ⊢ y →^{tex} “#1.

\vdash #2.”] [x ⊢ y →^{pyk} “∗ infer ∗”]

∗ ⊢⊢ ∗

[x ⊢⊢ y →^{val} ⌈x ⊢⊢ y⌉^{R} : : [ x : : [ y : : T ] ] ]

[x ⊢⊢ y →^{tex} “#1.

\mathrel {\makebox [0mm][l]{$\vdash $}\, {\vdash }} #2.”] [x ⊢⊢ y →^{pyk} “∗ endorse ∗”]

∗ i.e. ∗

[x i.e. y →^{val} ⌈x i.e. y⌉^{R} : : [ x : : [ y : : T ] ] ]

[x i.e. y →^{tex} “#1.

\mathrel {i.e.} #2.”]

[x i.e. y →^{pyk} “∗ id est ∗”]

∀∗: ∗

[∀x: y →^{val} ⌈∀x: y⌉^{R} : : [ x : : [ y : : T ] ] ]

[∀x: y →^{tex} “

\forall #1. \colon #2.”]

[∀x: y →^{pyk} “all ∗ indeed ∗”]

∗ ⊕ ∗

[x ⊕ y →^{val} ⌈x ⊕ y⌉^{R} : : [ x : : [ y : : T ] ] ]

[x ⊕ y →^{tex} “#1.

\mathrel {\oplus} #2.”]

[x ⊕ y →^{pyk} “∗ rule plus ∗”]

∗; ∗

[x; y →^{val} ⌈x; y⌉^{R} : : [ x : : [ y : : T ] ] ]

[x; y →^{tex} “#1.

; #2.”]

[x; y →^{pyk} “∗ cut ∗”]

∗ proves ∗

[p proves t →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[p proves t ¨= proof(⌈p⌉, ⌈t⌉, self)]⌉)]

[p proves t →^{tex} “#1. \ proves\ #2.”] [x proves y →^{pyk} “∗ proves ∗”]

∗ proof of ∗ : ∗

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

[t proof of s : p →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[t proof of s : p ¨= [Proof of s: λc.λx.P(⌈t ⊢ p⌉, p_{0}, c)]]⌉)]

[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 l : p →^{pyk} “∗ proof of ∗ reads ∗”]

Line ∗ : ∗ ≫ ∗; ∗

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

[Line l : a ≫ i; p →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Line l : a ≫ i; p ¨= ( [ a ≫ i ] ; let l ¨= i in p)]⌉)]

[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 →^{pyk} “line ∗ because ∗ indeed ∗ end line ∗”]

Last line ∗ ≫ ∗ □

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

[Last line a ≫ i □ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Last line a ≫ i □ ¨= (a ≫ i)]⌉)]

[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 □ →^{pyk} “because ∗ indeed ∗ qed”]

Line ∗ : Premise ≫ ∗; ∗

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

[Line l : Premise ≫ i; p →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Line l : Premise ≫ i; p ¨= (i ⊢ let l ¨= i in p)]⌉)]

[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 →^{pyk} “line ∗ premise ∗ end line ∗”]

Line ∗ : Side-condition ≫ ∗; ∗

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

[Line l : Side-condition ≫ i; p →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Line l : Side-condition ≫ i; p ¨= (i ⊢⊢ let l ¨= i in p)]⌉)]

[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 →^{pyk} “line ∗ side condition ∗ end line ∗”]

Arbitrary ≫ ∗; ∗

[Arbitrary ≫ i; p →^{name} “ Arbitrary \gg #1. ; #2.”]

[Arbitrary ≫ i; p →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Arbitrary ≫ i; p ¨= (∀i: p)]⌉)]

[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 →^{pyk} “arbitrary ∗ end line ∗”]

Local ≫ ∗ = ∗; ∗

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

[Local ≫ a = i; p →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Local ≫ a = i; p ¨= (let a ¨= i in p)]⌉)]

[Local ≫ a = 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]{$Local{}\gg{}$}% \quad% \parbox[t]{0.4\textwidth}{$#1. = #2. $\hfill\makebox[0mm][l]{\quad ; }}#3.”]

[Local ≫ u = v; p →^{pyk} “locally define ∗ as ∗ end line ∗”]

∗&∗

[∗&∗ →^{name} “#1.

\& #2.”]

[∗&∗ →^{tex} “#1.

&#2.”]

[∗&∗ →^{pyk} “∗ tab ∗”]

∗\\∗

[∗\\∗ →^{name} “#1.

\backslash \backslash #2.”]

[∗\\∗ →^{tex} “#1.

\\ #2.”]

[∗\\∗ →^{pyk} “∗ row

∗”]

The pyk compiler, version 0.grue.20050603 by Klaus Grue GRD-2005-06-22.UTC:06:58:05.413682 = MJD-53543.TAI:06:58:37.413682 = LGT-4626140317413682e-6