Logiweb codex of ijcar

Up Help

ijcar, [∗ =^{∘} ∗], 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 ≫ ∗; ∗, ∗ | ∗, →, ∗\\∗,

ijcar

[ijcar →^{prio} Preassociative [ijcar], [ijcar 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 [∗ then ∗], [∗[ ∗]∗]; Preassociative [∗&∗], [→]; Preassociative [∗\\∗], [∗\\∗]; ]

[ijcar →^{pyk} “ijcar”]

[∗ =^{∘} ∗]

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

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

RootVisible(∗)

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

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

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

A

[A →^{tex} “

A”]

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

R

[R →^{tex} “

R”]

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

C

[C →^{tex} “

C”]

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

T

[T →^{tex} “

T”]

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

[L →^{tex} “

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

{∗}

[{x} →^{tex} “

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

\overline{∗}

[\overline{x} →^{tex} “\overline\{#1.\}”] [\overline{x} →^{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 ”]

[⟨x≡y|z:=u⟩ →^{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 ”]

[⟨x≡^{0}y|z:=u⟩ →^{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 ”]

[⟨x≡^{1}y|z:=u⟩ →^{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.

[⟨x≡^{∗}y|z:=u⟩ →^{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(x, y) →^{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}(x, y) →^{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}(x, y, z) →^{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}(x, y, z) →^{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}(x, y, z, u) →^{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}(x, y, z, u) →^{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}^{∗}(x, y, z, u) →^{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}(x, y, z) →^{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}(p, c, e, b) →^{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}^{∗}(p, c, e, b) →^{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}(p) →^{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}(p, b) →^{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}^{∗}(p, b) →^{pyk} “deduction eight ∗ bound ∗ end deduction”]

S

[S →^{tex} “

S”]

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

Neg

[Neg →^{tex} “

Neg”]

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

MP

[MP →^{tex} “

MP”]

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

Gen

[Gen →^{tex} “

Gen”]

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

Ded

[Ded →^{tex} “

Ded”]

[Ded →^{pyk} “deduction”]

S1

[S1 →^{tex} “

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

S2

[S2 →^{tex} “

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

S3

[S3 →^{tex} “

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

S4

[S4 →^{tex} “

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

S5

[S5 →^{tex} “

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

S6

[S6 →^{tex} “

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

S7

[S7 →^{tex} “

S7”]

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

S8

[S8 →^{tex} “

S8”]

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

S9

[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}(t, s, c) →^{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}(b) →^{pyk} “block two ∗ end block”]

∗^{hide}

Predef: hide

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

[x^{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(x) →^{pyk} “macro indent ∗”]

∗′

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

{}’”]

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

∗ = ∗

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

= #2.”]

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

∗ ≠ ∗

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

\neq #2.”]

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

∗^{var}

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

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

{}ˆ {var}”]

[x^{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.”]

[x#^{0}y →^{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.”]

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

∗#^{∗}∗

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

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

\#.ˆ ∗#2.”]

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

∃∗: ∗

[∃x: y →^{tex} “

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

[∃x: y →^{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.”]

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

∀_{obj}∗: ∗

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

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

∗ ⇒ ∗

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

\Rightarrow #2.”]

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

∗ ⇔ ∗

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

\Leftrightarrow #2.”]

[x ⇔ y →^{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.”]

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

∗ ⊵ ∗

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

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

\unrhd #2.”]

[x ⊵ y →^{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.”]

[Πx: y →^{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 b; l : End; p →^{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 l ≫ i ; →^{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 ≫ i; p →^{pyk} “any term ∗ end line ∗”]

∗ | ∗

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

\mathrel{|} #2.”]

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

→

[→→^{tex} “

\rightarrow ”]

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

∗\\∗

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

\backslash \backslash #2.”]

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

\\{}#2.”]

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

The pyk compiler, version 0.grue.20060417 by Klaus Grue GRD-2006-05-26.UTC:13:59:58.555187 = MJD-53881.TAI:14:00:31.555187 = LGT-4655368831555187e-6