Logiweb codex of check

Up Help

x, y, check, parm(∗, ∗, ∗), parm^{∗}(∗, ∗, ∗), inst(∗, ∗), inst^{∗}(∗, ∗), occur(∗, ∗), occur^{∗}(∗, ∗), circular(∗ = ∗, ∗), circular^{∗}(∗ = ∗, ∗), unify(∗ = ∗, ∗), unify^{∗}(∗ = ∗, ∗), unify_{2}(∗ = ∗, ∗), L_{a}, L_{b}, L_{c}, L_{d}, L_{e}, L_{f}, L_{g}, L_{h}, L_{i}, L_{j}, L_{k}, L_{l}, L_{m}, L_{n}, L_{o}, L_{p}, L_{q}, L_{r}, L_{s}, L_{t}, L_{u}, L_{v}, L_{w}, L_{x}, L_{y}, L_{z}, L_{A}, L_{B}, L_{C}, L_{D}, L_{E}, L_{F}, L_{G}, L_{H}, L_{I}, L_{J}, L_{K}, L_{L}, L_{M}, L_{N}, L_{O}, L_{P}, L_{Q}, L_{R}, L_{S}, L_{T}, L_{U}, L_{V}, L_{W}, L_{X}, L_{Y}, L_{Z}, L_{?}, Reflexivity, Reflexivity_{1}, Commutativity, <tactic>, tactic, [∗ =^{tactic} ∗], P(∗, ∗, ∗), P^{∗}(∗, ∗, ∗), p_{0}, conclude_{1}(∗, ∗), conclude_{2}(∗, ∗, ∗), conclude_{3}(∗, ∗, ∗, ∗), ∗ ⊳ ∗, ∗ ⊳ ⊳ ∗, ∗ ≫ ∗, ∗ proof of ∗ : ∗, Line ∗ : ∗ ≫ ∗; ∗, Last line ∗ ≫ ∗, Line ∗ : Premise ≫ ∗; ∗, Line ∗ : Side-condition ≫ ∗; ∗, Arbitrary ≫ ∗; ∗, Local ≫ ∗ = ∗; ∗,

x

[x →^{tactic} y]

y

[y →^{proof} λc.λx.P(⌈x ⊢ z⌉, p_{0}, c)]

check

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

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

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

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

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

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

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

[check →^{pyk} “check”]

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}, s[t], 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) →^{val} If(u^{c}, t ≈ u, occur^{∗}(t, u^{t}))]

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

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

occur^{∗}(∗, ∗)

[occur^{∗}(t, u) →^{val} t!If(u^{a}, F, If(occur(t, u^{h}), T, occur^{∗}(t, u^{t})))]

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

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

circular(∗ = ∗, ∗)

[circular(t = u, s) →^{val} s!If(u^{c}, If(t ≈ u, T, occur(t, s[u])), circular^{∗}(t = u^{t}, s))]

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

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

circular^{∗}(∗ = ∗, ∗)

[circular^{∗}(t = u, s) →^{val} t! [ s!If(u^{a}, F, If(circular(t = u^{h}, s), T, circular^{∗}(t = u^{t}, s))) ] ]

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

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

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(circular(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} “reflexivity lemma”]

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} “reflexivity lemma one”]

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} “commutativity lemma”]

<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^{I}^{⊳} ^{∗}^{⊳} , 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^{⊳} , 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”]

∗ ⊳ ∗

[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 ∗”]

∗ 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 ∗ cut ∗”]

Last line ∗ ≫ ∗

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

[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 ∗ cut ∗”]

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 ∗ cut ∗”]

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 ∗ cut ∗”]

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

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

The pyk compiler, version 0.grue.20050502+ by Klaus Grue GRD-2005-05-26.UTC:06:49:32.964854 = MJD-53516.TAI:06:50:04.964854 = LGT-4623807004964854e-6