Logiweb codex of check

Up Help

X, check, [∗ =^{∘} ∗], RootVisible(∗), A, R, C, T, L, \{∗\}, \overline{∗}, 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, ⟨∗≡ ∗ | ∗:=∗⟩, ⟨∗≡^{0} ∗ | ∗:=∗⟩, ⟨∗≡^{1} ∗ | ∗:=∗⟩, ⟨∗≡^{∗} ∗ | ∗:=∗⟩, Ded(∗, ∗), Ded_{0}(∗, ∗), Ded_{1}(∗, ∗, ∗), Ded_{2}(∗, ∗, ∗), Ded_{3}(∗, ∗, ∗, ∗), Ded_{4}(∗, ∗, ∗, ∗), Ded_{4}^{∗}(∗, ∗, ∗, ∗), Ded_{5}(∗, ∗, ∗), Ded_{6}(∗, ∗, ∗, ∗), Ded_{6}^{∗}(∗, ∗, ∗, ∗), Ded_{7}(∗), Ded_{8}(∗, ∗), Ded_{8}^{∗}(∗, ∗), S, Neg, MP, Gen, Ded, S1, S2, S3, S4, S5, S6, S7, S8, S9, Repetition, A1′, A2′, A4′, A5′, Prop 3.2a, Prop 3.2b, Prop 3.2c, Prop 3.2d, Prop 3.2e_{1}, Prop 3.2e_{2}, Prop 3.2e, Prop 3.2f_{1}, Prop 3.2f_{2}, Prop 3.2f, Prop 3.2g_{1}, Prop 3.2g_{2}, Prop 3.2g, Prop 3.2h_{1}, Prop 3.2h_{2}, Prop 3.2h, Block_{1}(∗, ∗, ∗), Block_{2}(∗), ∗^{hide}, MacroIndent(∗), ∗′, ∗ = ∗, ∗ ≠ ∗, ∗^{var}, ∗#^{0}∗, ∗#^{1}∗, ∗#^{∗}∗, ∃∗: ∗, ∀∗: ∗, ∀_{obj}∗: ∗,

∗ ⇒ ∗, ∗ ⇔ ∗, ∗#∗, ∗ ⊵ ∗, Π∗: ∗, Begin ∗; ∗ : End; ∗, Last block line ∗ ≫ ∗;, Arbitrary ≫ ∗; ∗, ∗ | ∗, →, ∗\\∗,

X

[X →^{stmt} x]

check

[check →^{prio} Preassociative [check], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [ $ ∗ $ ], [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̃^{∗}(∗, ∗, ∗)], [(∗)], [(∗)], [display(∗)], [statement(∗)], [[∗]^{·}], [[∗]^{−}], [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}(∗, ∗)], [[∗ =^{∘} ∗]], [RootVisible(∗)], [A], [R], [C], [T], [L], [\{∗\}], [\overline{∗}], [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], [⟨∗≡ ∗ | ∗:=∗⟩], [⟨∗≡^{0} ∗ | ∗:=∗⟩], [⟨∗≡^{1} ∗ | ∗:=∗⟩], [⟨∗≡^{∗} ∗ | ∗:=∗⟩], [Ded(∗, ∗)], [Ded_{0}(∗, ∗)], [Ded_{1}(∗, ∗, ∗)], [Ded_{2}(∗, ∗, ∗)], [Ded_{3}(∗, ∗, ∗, ∗)], [Ded_{4}(∗, ∗, ∗, ∗)], [Ded_{4}^{∗}(∗, ∗, ∗, ∗)], [Ded_{5}(∗, ∗, ∗)], [Ded_{6}(∗, ∗, ∗, ∗)], [Ded_{6}^{∗}(∗, ∗, ∗, ∗)], [Ded_{7}(∗)], [Ded_{8}(∗, ∗)], [Ded_{8}^{∗}(∗, ∗)], [S], [Neg], [MP], [Gen], [Ded], [S1], [S2], [S3], [S4], [S5], [S6], [S7], [S8], [S9], [Repetition], [A1′], [A2′], [A4′], [A5′], [Prop 3.2a], [Prop 3.2b], [Prop 3.2c], [Prop 3.2d], [Prop 3.2e_{1}], [Prop 3.2e_{2}], [Prop 3.2e], [Prop 3.2f_{1}], [Prop 3.2f_{2}], [Prop 3.2f], [Prop 3.2g_{1}], [Prop 3.2g_{2}], [Prop 3.2g], [Prop 3.2h_{1}], [Prop 3.2h_{2}], [Prop 3.2h], [Block_{1}(∗, ∗, ∗)], [Block_{2}(∗)]; Preassociative [∗ {∗}], [∗/indexintro(∗, ∗, ∗, ∗)], [∗/intro(∗, ∗, ∗)], [∗/bothintro(∗, ∗, ∗, ∗, ∗)], [∗/nameintro(∗, ∗, ∗, ∗)], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]], [∗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^{∗}}], [∗^{hide}]; 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 ∗], [MacroIndent(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗′]; 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} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗], [∗ = ∗], [∗ ≠ ∗], [∗^{var}], [∗#^{0}∗], [∗#^{1}∗], [∗#^{∗}∗]; Preassociative [¬∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗]; Preassociative [∃∗: ∗], [∀∗: ∗], [∀_{obj}∗: ∗]; Postassociative [∗ ¨⇒ ∗], [∗ ⇒ ∗], [∗ ⇔ ∗]; Postassociative [∗ : ∗], [∗ spy ∗], [∗!∗]; Preassociative

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

Preassociative [λ ∗ .∗], [Λ ∗ .∗], [Λ∗], [if ∗ then ∗ else ∗], [let ∗ = ∗ in ∗], [let ∗ ¨= ∗ in ∗]; Preassociative [∗#∗]; 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 ≫ ∗ = ∗; ∗], [Begin ∗; ∗ : End; ∗], [Last block line ∗ ≫ ∗; ], [Arbitrary ≫ ∗; ∗]; Postassociative [∗ | ∗]; Postassociative [∗ , ∗], [∗[ ∗]∗]; Preassociative [∗&∗], [→]; Preassociative [∗\\∗], [∗ linebreak[4] ∗], [∗\\∗]; ]

[check →^{pyk} “check”]

[∗ =^{∘} ∗]

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

[[x =^{∘} y] →^{tex} “

[#1/tex name/tex. \stackrel {\circ}{=}#2. ]”] [[∗ =^{∘} ∗] →^{pyk} “general macro define " as " end define”]

RootVisible(∗)

[RootVisible(x) →^{name} “ RootVisible(#1. )”]

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

[RootVisible(∗) →^{pyk} “make root visible " end visible”]

A

[A →^{tex} “

A”]

[A →^{pyk} “sequent example axiom”]

R

[R →^{tex} “

R”]

[R →^{pyk} “sequent example rule”]

C

[C →^{tex} “

C”]

[C →^{pyk} “sequent example contradiction”]

T

[T →^{tex} “

T”]

[T →^{pyk} “sequent example theory”]

[L →^{tex} “

L”] [L →^{pyk} “sequent example lemma”]

{∗}

[{x} →^{tex} “

\{#1. \}”] [{∗} →^{pyk} “set " end set”]

\overline{∗}

[\overline{x} →^{tex} “\overline\{#1.\}”] [\overline{∗} →^{pyk} “object var " end var”]

a

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

[a →^{tex} “

\mathit{a}”] [a →^{pyk} “object a”]

b

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

[b →^{tex} “

\mathit{b}”] [b →^{pyk} “object b”]

c

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

[c →^{tex} “

\mathit{c}”]

[c →^{pyk} “object c”]

d

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

[d →^{tex} “

\mathit{d}”]

[d →^{pyk} “object d”]

e

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

[e →^{tex} “

\mathit{e}”]

[e →^{pyk} “object e”]

f

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

[f →^{tex} “

\mathit{f}”]

[f →^{pyk} “object f”]

g

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

[g →^{tex} “

\mathit{g}”]

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

h

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

[h →^{tex} “

\mathit{h}”] [h →^{pyk} “object h”]

i

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

[i →^{tex} “

\mathit{i}”] [i →^{pyk} “object i”]

j

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

[j →^{tex} “

\mathit{j}”] [j →^{pyk} “object j”]

k

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

[k →^{tex} “

\mathit{k}”] [k →^{pyk} “object k”]

l

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

[l →^{tex} “

\mathit{l}”] [l →^{pyk} “object l”] [m →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[m ¨= \overline{m}]⌉)]

[m →^{tex} “

\mathit{m}”] [m →^{pyk} “object m”]

n

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

[n →^{tex} “

\mathit{n}”] [n →^{pyk} “object n”]

o

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

[o →^{tex} “

\mathit{o}”] [o →^{pyk} “object o”]

p

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

[p →^{tex} “

\mathit{p}”] [p →^{pyk} “object p”]

q

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

[q →^{tex} “

\mathit{q}”] [q →^{pyk} “object q”]

r

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

[r →^{tex} “

\mathit{r}”] [r →^{pyk} “object r”]

s

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

[s →^{tex} “

\mathit{s}”] [s →^{pyk} “object s”]

t

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

[t →^{tex} “

\mathit{t}”] [t →^{pyk} “object t”]

u

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

[u →^{tex} “

\mathit{u}”] [u →^{pyk} “object u”]

v

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

[v →^{tex} “

\mathit{v}”] [v →^{pyk} “object v”]

w

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

[w →^{tex} “

\mathit{w}”]

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

x

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

[x →^{tex} “

\mathit{x}”]

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

y

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

[y →^{tex} “

\mathit{y}”]

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

z

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

[z →^{tex} “

\mathit{z}”]

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

⟨∗≡ ∗ | ∗:=∗⟩

[⟨a≡b|x:=t⟩ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[⟨a≡b|x:=t⟩ ¨= ⟨⌈a⌉≡^{0}⌈b⌉|⌈x⌉:=⌈t⌉⟩]⌉)]

[⟨x≡y|z:=u⟩ →^{tex} “

\langle #1. {\equiv} #2. | #3.

{:=} #4. \rangle ”]

[⟨∗≡ ∗ | ∗:=∗⟩ →^{pyk} “sub " is " where " is " end sub”]

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

[⟨a≡^{0}b|x:=t⟩ →^{val} λc.x^{var} ∧ ⟨a≡^{1}b|x:=t⟩]

[⟨x≡^{0}y|z:=u⟩ →^{tex} “

\langle #1. {\equiv}ˆ 0 #2. | #3. {:=} #4. \rangle ”]

[⟨∗≡^{0} ∗ | ∗:=∗⟩ →^{pyk} “sub zero " is " where " is " end sub”]

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

[⟨a≡^{1}b|x:=t⟩ →^{val} a!x!t! If(If(b =^{r} ⌈∀_{obj}u: v⌉, b^{1} =^{t} x, F), a =^{t} b, If(b^{var} ∧ b =^{t} x, a =^{t} t, If( a =^{r} b, ⟨a^{t}≡^{∗}b^{t}|x:=t⟩, F)))]

[⟨x≡^{1}y|z:=u⟩ →^{tex} “

\langle #1. {\equiv}ˆ 1 #2. | #3. {:=} #4. \rangle ”]

[⟨∗≡^{1} ∗ | ∗:=∗⟩ →^{pyk} “sub one " is " where " is " end sub”]

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

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

[⟨x≡^{∗}y|z:=u⟩ →^{tex} “

\langle #1. {\equiv}ˆ ∗ #2. | #3.

[⟨∗≡^{∗} ∗ | ∗:=∗⟩ →^{pyk} “sub star " is " where " is " end sub”]

Ded(∗, ∗)

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

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

[Ded(∗, ∗) →^{pyk} “deduction " conclude " end deduction”]

Ded_{0}(∗, ∗)

[Ded_{0}(p, c) →^{val} c!If(Ded_{8}(p, T), Ded_{1}(Ded_{7}(p), c, T), F)]

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

[Ded_{0}(∗, ∗) →^{pyk} “deduction zero " conclude " end deduction”]

Ded_{1}(∗, ∗, ∗)

[Ded_{1}(p, c, s) →^{val} If(c =^{r} ⌈x ⊢⊢ y⌉, Ded_{1}(p, c^{2}, c^{1} : : s), Ded_{2}(p, c, s))]

[Ded_{1}(x, y, z) →^{tex} “ Ded 1(#1. , #2. , #3. )”]

[Ded_{1}(∗, ∗, ∗) →^{pyk} “deduction one " conclude " condition " end deduction”]

Ded_{2}(∗, ∗, ∗)

[Ded_{2}(p, c, s) →^{val} s!p =^{r} ⌈x ⊢ y⌉ ∧ c =^{r} ⌈x ⇒

y⌉ \{ \begin{matrix}Ded_{3}(p^{1}, c^{1}, s, T) ∧ Ded_{2}(p^{2}, c^{2}, s) \\ Ded_{4}(p, c, s, Ded_{6}(p, c, T, T)) \end{matrix} ]

[Ded_{2}(x, y, z) →^{tex} “ Ded 2(#1. , #2. , #3. )”]

[Ded_{2}(∗, ∗, ∗) →^{pyk} “deduction two " conclude " condition " end deduction”]

Ded_{3}(∗, ∗, ∗, ∗)

[Ded_{3}(p, c, s, b) →^{val} If(¬c =^{r} ⌈∀_{obj}x: y⌉, Ded_{4}(p, c, s, b), If(p =^{r} ⌈∀_{obj}x: y⌉ ∧ p^{1} =^{t} c^{1}, Ded_{4}(p, c, s, b), Ded_{3}(p, c^{2}, s, c^{1} : : c^{1} : : b)))]

[Ded_{3}(x, y, z, u) →^{tex} “ Ded 3(#1. , #2. , #3. , #4. )”]

[Ded_{3}(∗, ∗, ∗, ∗) →^{pyk} “deduction three " conclude " condition " bound " end deduction”]

Ded_{4}(∗, ∗, ∗, ∗)

[Ded_{4}(p, c, s, b) →^{val} s!b!If(p =^{r} ⌈\overline{x}⌉, lookup(p, b, T) =^{t} c, If(¬p =^{r} c, F, If(p =^{r} ⌈∀_{obj}x: y⌉, p^{1} =^{t} c^{1} ∧ Ded_{4}(p^{2}, c^{2}, s, p^{1} : : p^{1} : : b), If(¬p =^{r} ⌈\underline{x}⌉, Ded_{4}^{∗}(p^{t}, c^{t}, s, b), p^{1} =^{t} c^{1} ∧ Ded_{5}(p, s, b)))))]

[Ded_{4}(x, y, z, u) →^{tex} “ Ded 4(#1. , #2. , #3. , #4. )”]

[Ded_{4}(∗, ∗, ∗, ∗) →^{pyk} “deduction four " conclude " condition " bound " end deduction”]

Ded_{4}^{∗}(∗, ∗, ∗, ∗)

[Ded_{4}^{∗}(p, c, s, b) →^{val} c!s!b!If(p, T, Ded_{4}(p^{h}, c^{h}, s, b) ∧ Ded_{4}^{∗}(p^{t}, c^{t}, s, b))]

[Ded_{4}^{∗}(x, y, z, u) →^{tex} “ Ded 4ˆ ∗(#1. , #2. , #3. , #4. )”]

[Ded_{4}^{∗}(∗, ∗, ∗, ∗) →^{pyk} “deduction four star " conclude " condition " bound " end deduction”]

Ded_{5}(∗, ∗, ∗)

[Ded_{5}(p, s, b) →^{val} p!s!If(b, T, ⌈⌈x⌉#^{0}⌈y⌉⌉^{h} : : ⌈⌈∗⌉⌉^{h} : : b^{h}^{h} : : T : : ⌈⌈x⌉⌉^{h} : : p : : T : : T ∈_{t} s ∧ Ded_{5}(p, s, b^{t}))]

[Ded_{5}(x, y, z) →^{tex} “ Ded 5(#1. , #2. , #3. )”]

[Ded_{5}(∗, ∗, ∗) →^{pyk} “deduction five " condition " bound " end deduction”]

Ded_{6}(∗, ∗, ∗, ∗)

[Ded_{6}(p, c, e, b) →^{val} p!c!b!e!If(p =^{r} ⌈\overline{x}⌉, p ∈_{t} e \{ \begin{matrix}b \\ p : : c : : b \end{matrix} , If(¬p =^{r} c, T,

If(p =^{r} ⌈\underline{a}⌉, b, If(p =^{r} ⌈∀_{obj}x: y⌉, Ded_{6}(p^{2}, c^{2}, c^{1} : : e, b), Ded_{6}^{∗}(p^{t}, c^{t}, e, b)))))]

[Ded_{6}(p, c, e, b) →^{tex} “ Ded 6(#1. , #2. , #3. , #4. )”]

[Ded_{6}(∗, ∗, ∗, ∗) →^{pyk} “deduction six " conclude " exception " bound " end deduction”]

Ded_{6}^{∗}(∗, ∗, ∗, ∗)

[Ded_{6}^{∗}(p, c, e, b) →^{val} p!c!b!e!If(p, b, Ded_{6}^{∗}(p^{t}, c^{t}, e, Ded_{6}(p^{h}, c^{h}, e, b)))]

[Ded_{6}^{∗}(p, c, e, b) →^{tex} “ Ded 6ˆ ∗(#1. , #2. , #3. , #4. )”]

[Ded_{6}^{∗}(∗, ∗, ∗, ∗) →^{pyk} “deduction six star " conclude " exception " bound " end deduction”]

Ded_{7}(∗)

[Ded_{7}(p) →^{val} p =^{r} ⌈∀x: y⌉ \{ \begin{matrix}Ded_{7}(p^{2}) \\ p \end{matrix} ]

[Ded_{7}(p) →^{tex} “

Ded 7(#1. )”]

[Ded_{7}(∗) →^{pyk} “deduction seven " end deduction”]

Ded_{8}(∗, ∗)

[Ded_{8}(p, b) →^{val} If(p =^{r} ⌈∀x: y⌉, Ded_{8}(p^{2}, p^{1} : : b), If(p =^{r} ⌈\underline{a}⌉, p ∈_{t} b, Ded_{8}^{∗}(p^{t}, b)))]

[Ded_{8}(p, b) →^{tex} “ Ded 8(#1. , #2. )”]

[Ded_{8}(∗, ∗) →^{pyk} “deduction eight " bound " end deduction”]

Ded_{8}^{∗}(∗, ∗)

[Ded_{8}^{∗}(p, b) →^{val} b!If(p, T, If(Ded_{8}(p^{h}, b), Ded_{8}^{∗}(p^{t}, b), F))]

[Ded_{8}^{∗}(p, b) →^{tex} “ Ded 8ˆ ∗(#1.

, #2. )”]

[Ded_{8}^{∗}(∗, ∗) →^{pyk} “deduction eight star " bound " end deduction”]

S

[S →^{stmt} ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′ ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ \underline{a} ⊢ \underline{b} ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ \underline{a}′ = \underline{b}′ ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a}′ = \underline{b}′ ⊢ \underline{a} = \underline{b} ⊕ ∀\underline{a}: ∀\underline{b}: λx.Ded_{0}(⌈\underline{a}⌉, ⌈\underline{b}⌉) ⊢⊢ \underline{a} ⊢ \underline{b} ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a} ⊕ ∀\underline{a}: \underline{a} + 0 = \underline{a} ⊕ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⊢ ¬\underline{b} ⇒ \underline{a} ⊢ \underline{b} ⊕ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{a} = \underline{c} ⊢ \underline{b} = \underline{c} ⊕ ∀\underline{x}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ⟨⌈\underline{b}⌉≡^{0}⌈\underline{a}⌉|⌈\underline{x}⌉:=⌈0⌉⟩ ⊢⊢ ⟨⌈\underline{c}⌉≡^{0}⌈\underline{a}⌉|⌈\underline{x}⌉:=⌈\underline{x}′⌉⟩ ⊢⊢ \underline{b} ⊢ \underline{a} ⇒ \underline{c} ⊢ \underline{a} ⊕ ∀\underline{a}: ¬0 = \underline{a}′ ⊕ ∀\underline{x}: ∀\underline{a}: \underline{a} ⊢ ∀_{obj}\underline{x}: \underline{a} ⊕ ∀\underline{a}: \underline{a} · 0 = 0]

[S →^{tex} “

S”]

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

Neg

[Neg →^{proof} Rule tactic]

[Neg →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⊢ ¬\underline{b} ⇒ \underline{a} ⊢ \underline{b}]

[Neg →^{tex} “

Neg”]

[Neg →^{pyk} “double negation”]

MP

[MP →^{proof} Rule tactic]

[MP →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ \underline{a} ⊢ \underline{b}]

[MP →^{tex} “

MP”]

[MP →^{pyk} “rule mp”]

Gen

[Gen →^{proof} Rule tactic] [Gen →^{stmt} S ⊢ ∀\underline{x}: ∀\underline{a}: \underline{a} ⊢ ∀_{obj}\underline{x}: \underline{a}]

[Gen →^{tex} “

Gen”] [Gen →^{pyk} “rule gen”]

Ded

[Ded →^{proof} Rule tactic] [Ded →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: λx.Ded_{0}(⌈\underline{a}⌉, ⌈\underline{b}⌉) ⊢⊢ \underline{a} ⊢ \underline{b}]

[Ded →^{tex} “

Ded”] [Ded →^{pyk} “deduction”]

S1

[S1 →^{proof} Rule tactic] [S1 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{a} = \underline{c} ⊢ \underline{b} = \underline{c}]

[S1 →^{tex} “

S1”] [S1 →^{pyk} “axiom s one”]

S2

[S2 →^{proof} Rule tactic] [S2 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ \underline{a}′ = \underline{b}′]

[S2 →^{tex} “

S2”] [S2 →^{pyk} “axiom s two”]

S3

[S3 →^{proof} Rule tactic] [S3 →^{stmt} S ⊢ ∀\underline{a}: ¬0 = \underline{a}′]

[S3 →^{tex} “

S3”] [S3 →^{pyk} “axiom s three”]

S4

[S4 →^{proof} Rule tactic] [S4 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}′ = \underline{b}′ ⊢ \underline{a} = \underline{b}]

[S4 →^{tex} “

S4”] [S4 →^{pyk} “axiom s four”]

S5

[S5 →^{proof} Rule tactic] [S5 →^{stmt} S ⊢ ∀\underline{a}: \underline{a} + 0 = \underline{a}]

[S5 →^{tex} “

S5”] [S5 →^{pyk} “axiom s five”]

S6

[S6 →^{proof} Rule tactic] [S6 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′]

[S6 →^{tex} “

S6”] [S6 →^{pyk} “axiom s six”]

S7

[S7 →^{proof} Rule tactic] [S7 →^{stmt} S ⊢ ∀\underline{a}: \underline{a} · 0 = 0]

[S7 →^{tex} “

S7”]

[S7 →^{pyk} “axiom s seven”]

S8

[S8 →^{proof} Rule tactic]

[S8 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a}]

[S8 →^{tex} “

S8”]

[S8 →^{pyk} “axiom s eight”]

S9

[S9 →^{proof} Rule tactic]

[S9 →^{stmt} S ⊢ ∀\underline{x}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ⟨⌈\underline{b}⌉≡^{0}⌈\underline{a}⌉|⌈\underline{x}⌉:=⌈0⌉⟩ ⊢⊢ ⟨⌈\underline{c}⌉≡^{0}⌈\underline{a}⌉|⌈\underline{x}⌉:=⌈\underline{x}′⌉⟩ ⊢⊢ \underline{b} ⊢

\underline{a} ⇒ \underline{c} ⊢ \underline{a}]

[S9 →^{tex} “

S9”]

[S9 →^{pyk} “axiom s nine”]

Repetition

[Repetition →^{proof} λc.λx.⌈S ⊢ ∀\underline{a}: \underline{a}^{I}⌉]

[Repetition →^{stmt} S ⊢ ∀\underline{a}: \underline{a} ⊢ \underline{a}]

[Repetition →^{tex} “ Repetition”]

[Repetition →^{pyk} “repetition”]

A1′

[A1′ →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ \underline{b} ⊢ Repetition ⊳ \underline{a} ≫ \underline{a}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ \underline{b} ⊢ \underline{a} ≫ \underline{a} ⇒ \underline{b} ⇒ \underline{a}⌉, p_{0}, c)] [A1′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⇒ \underline{a}]

[A1′ →^{tex} “

A1’”]

[A1′ →^{pyk} “lemma a one”]

A2′

[A2′ →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{a} ⇒ \underline{b} ⊢ \underline{a} ⊢ MP⊳\underline{a} ⇒ \underline{b}⊳\underline{a} ≫ \underline{b}; MP⊳\underline{a} ⇒ \underline{b} ⇒ \underline{c}⊳\underline{a} ≫ \underline{b} ⇒ \underline{c}; MP⊳\underline{b} ⇒ \underline{c}⊳\underline{b} ≫ \underline{c}; Ded⊳∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{a} ⇒ \underline{b} ⊢ \underline{a} ⊢ \underline{c} ≫ \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{a} ⇒ \underline{b} ⇒ \underline{a} ⇒ \underline{c}⌉, p_{0}, c)]

[A2′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{a} ⇒ \underline{b} ⇒ \underline{a} ⇒ \underline{c}]

[A2′ →^{tex} “

A2’”]

[A2′ →^{pyk} “lemma a two”]

A4′

[A4′ →^{proof} λc.λx.P(⌈S ⊢ \overline{x} + \overline{y} = \overline{y} + \overline{x} ⊢ Repetition ⊳ \overline{x} + \overline{y} = \overline{y} + \overline{x} ≫ \overline{x} + \overline{y} = \overline{y} + \overline{x}; Ded ⊳ \overline{x} + \overline{y} = \overline{y} + \overline{x} ⊢ \overline{x} + \overline{y} = \overline{y} + \overline{x} ≫ ∀_{obj}\overline{x}: ∀_{obj}\overline{y}: \overline{x} + \overline{y} = \overline{y} + \overline{x} ⇒ 2 + 3 = 3 + 2⌉, p_{0}, c)]

[A4′ →^{stmt} S ⊢ ∀_{obj}\overline{x}: ∀_{obj}\overline{y}: \overline{x} + \overline{y} = \overline{y} + \overline{x} ⇒ 2 + 3 = 3 + 2]

[A4′ →^{tex} “

A4’”]

[A4′ →^{pyk} “lemma a four”]

A5′

[A5′ →^{proof} λc.λx.P(⌈S ⊢ 2 + 3 = 5 ⇒ 2 + 3 + \overline{x} = 5 + \overline{x} ⊢ 2 + 3 = 5 ⊢ MP ⊳ 2 + 3 = 5 ⇒ 2 + 3 + \overline{x} = 5 + \overline{x} ⊳ 2 + 3 = 5 ≫ 2 + 3 + \overline{x} = 5 + \overline{x}; Gen ⊳ 2 + 3 + \overline{x} = 5 + \overline{x} ≫ ∀_{obj}\overline{x}: 2 + 3 + \overline{x} = 5 + \overline{x}; Ded ⊳ 2 + 3 = 5 ⇒ 2 + 3 + \overline{x} = 5 + \overline{x} ⊢ 2 + 3 = 5 ⊢ ∀_{obj}\overline{x}: 2 + 3 + \overline{x} = 5 + \overline{x} ≫ ∀_{obj}\overline{x}: 2 + 3 = 5 ⇒ 2 + 3 + \overline{x} = 5 + \overline{x} ⇒ 2 + 3 = 5 ⇒ ∀_{obj}\overline{x}: 2 + 3 + \overline{x} = 5 + \overline{x}⌉, p_{0}, c)]

[A5′ →^{stmt} S ⊢ ∀_{obj}\overline{x}: 2 + 3 = 5 ⇒ 2 + 3 + \overline{x} = 5 + \overline{x} ⇒ 2 + 3 = 5 ⇒ ∀_{obj}\overline{x}: 2 + 3 + \overline{x} = 5 + \overline{x}]

[A5′ →^{tex} “

A5’”]

[A5′ →^{pyk} “lemma a five”]

Prop 3.2a

[Prop 3.2a →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: S5 ≫ \underline{a} + 0 = \underline{a}; S1 ⊳ \underline{a} + 0 = \underline{a} ⊳ \underline{a} + 0 = \underline{a} ≫ \underline{a} = \underline{a}⌉, p_{0}, c)]

[Prop 3.2a →^{stmt} S ⊢ ∀\underline{a}: \underline{a} = \underline{a}]

[Prop 3.2a →^{tex} “ Prop\ 3.2a”]

[Prop 3.2a →^{pyk} “prop three two a”]

Prop 3.2b

[Prop 3.2b →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ Prop 3.2a ≫ \underline{a} = \underline{a}; S1 ⊳ \underline{a} = \underline{b} ⊳ \underline{a} = \underline{a} ≫ \underline{b} = \underline{a}⌉, p_{0}, c)]

[Prop 3.2b →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ \underline{b} = \underline{a}]

[Prop 3.2b →^{tex} “ Prop\ 3.2b”]

[Prop 3.2b →^{pyk} “prop three two b”]

Prop 3.2c

[Prop 3.2c →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{b} = \underline{c} ⊢ Prop 3.2b ⊳ \underline{a} = \underline{b} ≫ \underline{b} = \underline{a}; S1 ⊳ \underline{b} = \underline{a} ⊳ \underline{b} = \underline{c} ≫ \underline{a} = \underline{c}⌉, p_{0}, c)]

[Prop 3.2c →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{b} = \underline{c} ⊢ \underline{a} = \underline{c}]

[Prop 3.2c →^{tex} “ Prop\ 3.2c”]

[Prop 3.2c →^{pyk} “prop three two c”]

Prop 3.2d

[Prop 3.2d →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{c} ⊢ \underline{b} = \underline{c} ⊢ Prop 3.2b ⊳ \underline{b} = \underline{c} ≫ \underline{c} = \underline{b}; Prop 3.2c ⊳ \underline{a} = \underline{c} ⊳ \underline{c} = \underline{b} ≫ \underline{a} = \underline{b}⌉, p_{0}, c)]

[Prop 3.2d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{c} ⊢ \underline{b} = \underline{c} ⊢ \underline{a} = \underline{b}]

[Prop 3.2d →^{tex} “ Prop\ 3.2d”]

[Prop 3.2d →^{pyk} “prop three two d”]

Prop 3.2e_{1}

[Prop 3.2e_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ S5 ≫ \underline{a}+0 = \underline{a}; Prop 3.2c⊳ \underline{a}+0 = \underline{a}⊳\underline{a} = \underline{b} ≫ \underline{a}+0 = \underline{b}; S5 ≫ \underline{b}+0 = \underline{b}; Prop 3.2d⊳\underline{a}+0 = \underline{b}⊳\underline{b}+0 = \underline{b} ≫ \underline{a}+0 = \underline{b}+0; Ded⊳∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ \underline{a}+0 = \underline{b}+0 ≫ \underline{a} = \underline{b} ⇒ \underline{a}+0 = \underline{b}+0⌉, p_{0}, c)]

[Prop 3.2e_{1} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⇒ \underline{a} + 0 = \underline{b} + 0]

[Prop 3.2e_{1} →^{tex} “ Prop\ 3.2e 1”]

[Prop 3.2e_{1} →^{pyk} “prop three two e one”]

Prop 3.2e_{2}

[Prop 3.2e_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⊢ \underline{a} = \underline{b} ⊢ MP ⊳ \underline{a} = \underline{b} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⊳ \underline{a} = \underline{b} ≫ \underline{a} + \underline{c} = \underline{b} + \underline{c}; S2 ⊳ \underline{a} + \underline{c} = \underline{b} + \underline{c} ≫ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′; S6 ≫ \underline{a} + \underline{c}′ = \underline{a} + \underline{c}′; Prop 3.2c ⊳ \underline{a} + \underline{c}′ = \underline{a} + \underline{c}′ ⊳ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′ ≫ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′; S6 ≫ \underline{b} + \underline{c}′ = \underline{b} + \underline{c}′; Prop 3.2d ⊳ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′ ⊳ \underline{b} + \underline{c}′ = \underline{b} + \underline{c}′ ≫ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⊢ \underline{a} = \underline{b} ⊢ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′ ≫ \underline{a} = \underline{b} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} = \underline{b} ⇒ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′⌉, p_{0}, c)]

[Prop 3.2e_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} = \underline{b} ⇒ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′]

[Prop 3.2e_{2} →^{tex} “ Prop\ 3.2e 2”]

[Prop 3.2e_{2} →^{pyk} “prop three two e two”]

Prop 3.2e

[Prop 3.2e →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ Prop 3.2e_{1} ≫ \overline{x} = \overline{y} ⇒ \overline{x} + 0 = \overline{y} + 0; Prop 3.2e_{2} ≫ \overline{x} = \overline{y} ⇒ \overline{x} + \overline{z} = \overline{y} + \overline{z} ⇒ \overline{x} = \overline{y} ⇒ \overline{x} + \overline{z}′ = \overline{y} + \overline{z}′; S9 @ \overline{z} ⊳ \overline{x} = \overline{y} ⇒ \overline{x} + 0 = \overline{y} + 0 ⊳ \overline{x} = \overline{y} ⇒ \overline{x} + \overline{z} = \overline{y} + \overline{z} ⇒ \overline{x} = \overline{y} ⇒ \overline{x} + \overline{z}′ = \overline{y} + \overline{z}′ ≫ \overline{x} = \overline{y} ⇒ \overline{x} + \overline{z} = \overline{y} + \overline{z}; Ded ⊳ \overline{x} = \overline{y} ⇒ \overline{x} + \overline{z} = \overline{y} + \overline{z} ≫ \underline{a} = \underline{b} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c}; MP ⊳ \underline{a} = \underline{b} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⊳ \underline{a} = \underline{b} ≫ \underline{a} + \underline{c} = \underline{b} + \underline{c}⌉, p_{0}, c)]

[Prop 3.2e →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{a} + \underline{c} = \underline{b} + \underline{c}]

[Prop 3.2e →^{tex} “ Prop\ 3.2e”]

[Prop 3.2e →^{pyk} “prop three two e”]

Prop 3.2f_{1}

[Prop 3.2f_{1} →^{proof} λc.λx.P(⌈S ⊢ S5 ≫ 0 + 0 = 0; Prop 3.2b ⊳ 0 + 0 = 0 ≫ 0 = 0 + 0⌉, p_{0}, c)]

[Prop 3.2f_{1} →^{stmt} S ⊢ 0 = 0 + 0]

[Prop 3.2f_{1} →^{tex} “ Prop\ 3.2f 1”]

[Prop 3.2f_{1} →^{pyk} “prop three two f one”]

Prop 3.2f_{2}

[Prop 3.2f_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{a}: \underline{a} = 0 + \underline{a} ⊢ S2 ⊳ \underline{a} = 0 + \underline{a} ≫ \underline{a}′ = 0 + \underline{a}′; S6 ≫ 0 + \underline{a}′ = 0 + \underline{a}′; Prop 3.2d ⊳ \underline{a}′ = 0 + \underline{a}′ ⊳ 0 + \underline{a}′ = 0 + \underline{a}′ ≫ \underline{a}′ = 0 + \underline{a}′; Ded ⊳ ∀\underline{a}: \underline{a} = 0 + \underline{a} ⊢ \underline{a}′ = 0 + \underline{a}′ ≫ \underline{a} = 0 + \underline{a} ⇒ \underline{a}′ = 0 + \underline{a}′⌉, p_{0}, c)]

[Prop 3.2f_{2} →^{stmt} S ⊢ ∀\underline{a}: \underline{a} = 0 + \underline{a} ⇒ \underline{a}′ = 0 + \underline{a}′]

[Prop 3.2f_{2} →^{tex} “ Prop\ 3.2f 2”]

[Prop 3.2f_{2} →^{pyk} “prop three two f two”]

Prop 3.2f

[Prop 3.2f →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: Prop 3.2f_{1} ≫ 0 = 0 + 0; Prop 3.2f_{2} ≫ \overline{x} = 0 + \overline{x} ⇒ \overline{x}′ = 0 + \overline{x}′; S9 @ \overline{x} ⊳ 0 = 0 + 0 ⊳ \overline{x} = 0 + \overline{x} ⇒ \overline{x}′ = 0 + \overline{x}′ ≫ \overline{x} = 0 + \overline{x}; Ded ⊳ \overline{x} = 0 + \overline{x} ≫ \underline{a} = 0 + \underline{a}⌉, p_{0}, c)]

[Prop 3.2f →^{stmt} S ⊢ ∀\underline{a}: \underline{a} = 0 + \underline{a}]

[Prop 3.2f →^{tex} “ Prop\ 3.2f”]

[Prop 3.2f →^{pyk} “prop three two f”]

Prop 3.2g_{1}

[Prop 3.2g_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: S5 ≫ \underline{a}′ + 0 = \underline{a}′; S5 ≫ \underline{a} + 0 = \underline{a}; S2 ⊳ \underline{a} + 0 = \underline{a} ≫ \underline{a} + 0′ = \underline{a}′; Prop 3.2d ⊳ \underline{a}′ + 0 = \underline{a}′ ⊳ \underline{a} + 0′ = \underline{a}′ ≫ \underline{a}′ + 0 = \underline{a} + 0′⌉, p_{0}, c)]

[Prop 3.2g_{1} →^{stmt} S ⊢ ∀\underline{a}: \underline{a}′ + 0 = \underline{a} + 0′]

[Prop 3.2g_{1} →^{tex} “ Prop\ 3.2g 1”]

[Prop 3.2g_{1} →^{pyk} “prop three two g one”]

Prop 3.2g_{2}

[Prop 3.2g_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a}′ + \underline{b} = \underline{a} + \underline{b}′ ⊢ S2 ⊳ \underline{a}′ + \underline{b} = \underline{a} + \underline{b}′ ≫ \underline{a}′ + \underline{b}′ = \underline{a} + \underline{b}′′; S6 ≫ \underline{a}′ + \underline{b}′ = \underline{a}′ + \underline{b}′; Prop 3.2c ⊳ \underline{a}′ + \underline{b}′ = \underline{a}′ + \underline{b}′ ⊳ \underline{a}′ + \underline{b}′ = \underline{a} + \underline{b}′′ ≫ \underline{a}′ + \underline{b}′ = \underline{a} + \underline{b}′′; S6 ≫ \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′; S2 ⊳ \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′ ≫ \underline{a} + \underline{b}′′ = \underline{a} + \underline{b}′′; Prop 3.2d ⊳ \underline{a}′ + \underline{b}′ = \underline{a} + \underline{b}′′ ⊳ \underline{a} + \underline{b}′′ = \underline{a} + \underline{b}′′ ≫ \underline{a}′ + \underline{b}′ = \underline{a} + \underline{b}′′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a}′ + \underline{b} = \underline{a} + \underline{b}′ ⊢ \underline{a}′ + \underline{b}′ = \underline{a} + \underline{b}′′ ≫ \underline{a}′ + \underline{b} = \underline{a} + \underline{b}′ ⇒ \underline{a}′ + \underline{b}′ = \underline{a} + \underline{b}′′⌉, p_{0}, c)]

[Prop 3.2g_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}′ + \underline{b} = \underline{a} + \underline{b}′ ⇒ \underline{a}′ + \underline{b}′ = \underline{a} + \underline{b}′′]

[Prop 3.2g_{2} →^{tex} “ Prop\ 3.2g 2”]

[Prop 3.2g_{2} →^{pyk} “prop three two g two”]

Prop 3.2g

[Prop 3.2g →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: Prop 3.2g_{1} ≫ \overline{x}′ + 0 = \overline{x} + 0′; Prop 3.2g_{2} ≫ \overline{x}′ + \overline{y} = \overline{x} + \overline{y}′ ⇒ \overline{x}′ + \overline{y}′ = \overline{x} + \overline{y}′′; S9 @ \overline{y} ⊳ \overline{x}′ + 0 = \overline{x} + 0′ ⊳ \overline{x}′ + \overline{y} = \overline{x} + \overline{y}′ ⇒ \overline{x}′ + \overline{y}′ = \overline{x} + \overline{y}′′ ≫ \overline{x}′ + \overline{y} = \overline{x} + \overline{y}′; Ded ⊳ \overline{x}′ + \overline{y} = \overline{x} + \overline{y}′ ≫ \underline{a}′ + \underline{b} = \underline{a} + \underline{b}′⌉, p_{0}, c)]

[Prop 3.2g →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}′ + \underline{b} = \underline{a} + \underline{b}′] [Prop 3.2g →^{tex} “ Prop\ 3.2g”]

[Prop 3.2g →^{pyk} “prop three two g”]

Prop 3.2h_{1}

[Prop 3.2h_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: S5 ≫ \underline{a} + 0 = \underline{a}; Prop 3.2f ≫ \underline{a} = 0 + \underline{a}; Prop 3.2c ⊳ \underline{a} + 0 = \underline{a} ⊳ \underline{a} = 0 + \underline{a} ≫ \underline{a} + 0 = 0 + \underline{a}⌉, p_{0}, c)]

[Prop 3.2h_{1} →^{stmt} S ⊢ ∀\underline{a}: \underline{a} + 0 = 0 + \underline{a}]

[Prop 3.2h_{1} →^{tex} “ Prop\ 3.2h 1”]

[Prop 3.2h_{1} →^{pyk} “prop three two h one”]

Prop 3.2h_{2}

[Prop 3.2h_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = \underline{b} + \underline{a} ⊢ S2 ⊳ \underline{a} + \underline{b} = \underline{b}+\underline{a} ≫ \underline{a}+\underline{b}′ = \underline{b}+\underline{a}′; S6 ≫ \underline{a}+\underline{b}′ = \underline{a}+\underline{b}′; Prop 3.2c⊳\underline{a}+\underline{b}′ = \underline{a}+\underline{b}′ ⊳\underline{a}+\underline{b}′ = \underline{b} + \underline{a}′ ≫ \underline{a} + \underline{b}′ = \underline{b} + \underline{a}′; Prop 3.2g ≫ \underline{b}′ + \underline{a} = \underline{b} + \underline{a}′; Prop 3.2d ⊳ \underline{a} + \underline{b}′ = \underline{b} + \underline{a}′ ⊳ \underline{b}′ + \underline{a} = \underline{b} + \underline{a}′ ≫ \underline{a} + \underline{b}′ = \underline{b}′ + \underline{a}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = \underline{b} + \underline{a} ⊢ \underline{a} + \underline{b}′ = \underline{b}′ + \underline{a} ≫ \underline{a} + \underline{b} = \underline{b} + \underline{a} ⇒ \underline{a} + \underline{b}′ = \underline{b}′ + \underline{a}⌉, p_{0}, c)]

[Prop 3.2h_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = \underline{b} + \underline{a} ⇒ \underline{a} + \underline{b}′ = \underline{b}′ + \underline{a}]

[Prop 3.2h_{2} →^{tex} “ Prop\ 3.2h 2”]

[Prop 3.2h_{2} →^{pyk} “prop three two h two”]

Prop 3.2h

[Prop 3.2h →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: Prop 3.2h_{1} ≫ \overline{x} + 0 = 0 + \overline{x}; Prop 3.2h_{2} ≫ \overline{x} + \overline{y} = \overline{y} + \overline{x} ⇒ \overline{x} + \overline{y}′ = \overline{y}′ + \overline{x}; S9 @ \overline{y} ⊳ \overline{x} + 0 = 0 + \overline{x} ⊳ \overline{x} + \overline{y} = \overline{y} + \overline{x} ⇒ \overline{x} + \overline{y}′ = \overline{y}′ + \overline{x} ≫ \overline{x} + \overline{y} = \overline{y} + \overline{x}; Ded ⊳ \overline{x} + \overline{y} = \overline{y} + \overline{x} ≫ \underline{a} + \underline{b} = \underline{b} + \underline{a}⌉, p_{0}, c)]

[Prop 3.2h →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = \underline{b} + \underline{a}]

[Prop 3.2h →^{tex} “ Prop\ 3.2h”]

[Prop 3.2h →^{pyk} “prop three two h”]

Block_{1}(∗, ∗, ∗)

[Block_{1}(t, s, c) →^{val} t!s!c!let_{1}(λb.let_{1}(λx.let_{1}(λq.let_{1}(λq.Q̃(t, ⌈b; q⌉, ⌈b⌉ : : b : : ⌈q⌉ : : q : : T), M̃(q, s, c)), Q̃(t, ⌈let l ¨= x in p⌉, ⌈l⌉ : : t^{2} : : ⌈p⌉ : : t^{3} : : ⌈x⌉ : : x : : T)), Block_{2}(b)), M̃(t^{1}, s, c))]

[Block_{1}(t, s, c) →^{tex} “ Block 1(#1. , #2. , #3. )”]

[Block_{1}(∗, ∗, ∗) →^{pyk} “block one " state " cache " end block”]

Block_{2}(∗)

[Block_{2}(b) →^{val} If(b =^{r} ⌈x ⊢ y⌉, Q̃(b, ⌈x ⊢ y⌉, ⌈x⌉ : : b^{1} : : ⌈y⌉ : : Block_{2}(b^{2}) : : T), If(b =^{r} ⌈x ⊢⊢ y⌉, Q̃(b, ⌈x ⊢⊢ y⌉, ⌈x⌉ : : b^{1} : : ⌈y⌉ : : Block_{2}(b^{2}) : : T), If(b =^{r} ⌈∀x: y⌉, Q̃(b, ⌈∀x: y⌉, ⌈x⌉ : : b^{1} : : ⌈y⌉ : : Block_{2}(b^{2}) : : T), If(b =^{r} ⌈x; y⌉, Block_{2}(b^{2}),

If(b =^{r} ⌈x ≫ y⌉, b^{2}, ⊥ ⊥)))))]

[Block_{2}(b) →^{tex} “ Block 2(#1. )”]

[Block_{2}(∗) →^{pyk} “block two " end block”]

∗^{hide}

Predef: hide

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

[∗^{hide} →^{pyk} “" hide”]

MacroIndent(∗)

[MacroIndent(x) →^{name} “ MacroIndent(#1. )”]

[MacroIndent(x) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[MacroIndent(x) ¨= x]⌉)] [MacroIndent(x) →^{tex} “ $% \leftskip=1em% $#1.”]

[MacroIndent(∗) →^{pyk} “macro indent "”]

∗′

[x′ →^{tex} “#1.

{}’”]

[∗′ →^{pyk} “" suc”]

∗ = ∗

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

= #2.”]

[∗ = ∗ →^{pyk} “" equal "”]

∗ ≠ ∗

[x ≠ y →^{tex} “#1.

\neq #2.”]

[∗ ≠ ∗ →^{pyk} “" unequal "”]

∗^{var}

[x^{var} →^{val} x =^{r} ⌈\overline{x}⌉]

[x^{var} →^{tex} “#1.

{}ˆ {var}”]

[∗^{var} →^{pyk} “" is object var”]

∗#^{0}∗

[x#^{0}y →^{val} λc.x^{var} ∧ y^{C} ∧ x#^{1}y]

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

\#.ˆ 0#2.”]

[∗#^{0}∗ →^{pyk} “" avoid zero "”]

∗#^{1}∗

[x#^{1}y →^{val} If(y^{var}, ¬x =^{t} y, If(¬y =^{r} ⌈∀_{obj}x: y⌉, x#^{∗}y^{t}, If(x =^{t} y^{1}, T, x#^{1}y^{2})))]

[x#^{1}y →^{tex} “#1.

\#.ˆ 1#2.”]

[∗#^{1}∗ →^{pyk} “" avoid one "”]

∗#^{∗}∗

[x#^{∗}y →^{val} x!If(y, T, If(x#^{1}y^{h}, x#^{∗}y^{t}, F))]

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

\#.ˆ ∗#2.”]

[∗#^{∗}∗ →^{pyk} “" avoid star "”]

∃∗: ∗

[∃x: y →^{tex} “

\exists #1. \colon #2.”]

[∃∗: ∗ →^{pyk} “exist " indeed "”]

∀∗: ∗

[∀x: y →^{macro} λt.λs.λc.M̃(If(¬t^{1} =^{r} ⌈x, y⌉, Q̃(t, ⌈∀_{obj}x: y⌉, ⌈x⌉ : : t^{1} : : ⌈y⌉ : : t^{2} : : T), Q̃(t, ⌈∀_{obj}x: ∀y: z⌉, ⌈x⌉ : : t^{1}^{1} : : ⌈y⌉ : : t^{1}^{2} : : ⌈z⌉ : : t^{2} : : T)), s, c)]

[∀x: y →^{tex} “

\forall #1. \colon #2.”]

[∀∗: ∗ →^{pyk} “for all " indeed "”]

∀_{obj}∗: ∗

[∀_{obj}x: y →^{tex} “ \forall {obj} #1. \colon #2.”]

[∀_{obj}∗: ∗ →^{pyk} “for all objects " indeed "”]

∗ ⇒ ∗

[x ⇒ y →^{tex} “#1.

\Rightarrow #2.”]

[∗ ⇒ ∗ →^{pyk} “" imply "”]

∗ ⇔ ∗

[x ⇔ y →^{tex} “#1.

\Leftrightarrow #2.”]

[∗ ⇔ ∗ →^{pyk} “" if and only if "”]

∗#∗

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

[x#y →^{tex} “#1.

\#.#2.”]

[∗#∗ →^{pyk} “" avoid "”]

∗ ⊵ ∗

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

[x ⊵ y →^{tex} “#1.

\unrhd #2.”]

[∗ ⊵ ∗ →^{pyk} “" object modus ponens "”]

Π∗: ∗

[Πx: y →^{macro} λt.λs.λc.M̃(If(¬t^{1} =^{r} ⌈x, y⌉, Q̃(t, ⌈∀x: y⌉, ⌈x⌉ : : t^{1} : : ⌈y⌉ : : t^{2} : : T), Q̃(t, ⌈∀x: Πy: z⌉, ⌈x⌉ : : t^{1}^{1} : : ⌈y⌉ : : t^{1}^{2} : : ⌈z⌉ : : t^{2} : : T)), s, c)]

[Πx: y →^{tex} “

\Pi #1. \colon #2.”]

[Π∗: ∗ →^{pyk} “for all terms " indeed "”]

Begin ∗; ∗ : End; ∗

[Begin b; l : End; p →^{name} “ Begin \, #1. ; #2. : End ; #3.”]

[Begin b; l : End; p →^{macro} λt.λs.λc.Block_{1}(t, s, c)]

[Begin b; l : End; p →^{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 $:}$Block {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$Begin $\hfill \makebox [0mm][l]{\quad ; }}#1. \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#2. $:}$Block {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$End $\hfill \makebox [0mm][l]{\quad ; }}#3.”]

[Begin ∗; ∗ : End; ∗ →^{pyk} “block " line " end block "”]

Last block line ∗ ≫ ∗;

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

[Last block line a ≫ i ; →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Last block line a ≫ i ; ¨= (a ≫ i)]⌉)]

[Last block 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 ; }}”]

[Last block line ∗ ≫ ∗; →^{pyk} “because " indeed " 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 ≫ ∗; ∗ →^{pyk} “any term " end line "”]

∗ | ∗

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

\mathrel{|} #2.”]

[∗ | ∗ →^{pyk} “" alternative "”]

→

[→→^{tex} “

\rightarrow ”]

[→ →^{pyk} “evaluates to”]

∗\\∗

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

\backslash \backslash #2.”]

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

\\{}#2.”]

[∗\\∗ →^{pyk} “" safe row "”]

The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-05-04.UTC:15:42:31.918490 = MJD-53859.TAI:15:43:04.918490 = LGT-4653474184918490e-6