Logiweb codex of opgave

Up Help

S, Neg, MP, Gen, Ded, S1, S2, S3, S4, S5, S6, S7, S8, S9, Prop 3.2a, Prop 3.2b, Prop 3.2c, Prop 3.2d, Prop 3.2e, Prop 3.2f, Prop 3.2g, Prop 3.2h, opgave, \overline{0}, \overline{1}, \overline{2}, \overline{3}, \overline{4}, \overline{5}, \overline{6}, \overline{7}, \overline{8}, \overline{9}, \overline{n}, rule div, R, R1, R2, R3, R4, R5, R6, Con1, Con2, Con, Dis1, Dis2, Lem1.11c, Cor1.10a, Cor1.10b, Lem1.11a, Lem1.11b, H3, Prop3.2c′, S1′′, Neg′, Repetition′, Lem1.11e, Lem1.11d, Prop3.2b′, H10, H11, Lem1.11g, MT, S10, Prop 3.2, Prop 3.2i, Prop 3.2j_{1}, Prop 3.2j_{2}, Prop 3.2j, Prop 3.2k_{1}, Prop 3.2k_{2}, Prop 3.2k, Prop 3.2l_{1}, Prop 3.2l_{2}, Prop 3.2l, Prop 3.2m_{1}, Prop 3.2m_{2}, Prop 3.2m, Prop 3.2n_{1}, Prop 3.2n_{2}, Prop 3.2n, Prop 3.2o, Prop 3.4, Prop 3.4a_{1}, Prop 3.4a_{2}, Prop 3.4a, Prop 3.4b, Prop 3.4c_{1}, Prop 3.4c_{2}, Prop 3.4c, Prop 3.4d_{1}, Prop 3.4d_{2}, Prop 3.4d, Prop 3.5, Prop 3.5a, Prop 3.5b, Prop 3.5c, Prop 3.5d_{1}, Prop 3.5d_{2}, Prop 3.5d, Prop 3.5e_{1}, Prop 3.5e_{2}, Prop 3.5e, Prop 3.5f_{1}, Prop 3.5f_{2}, Prop 3.5f, Prop 3.5g_{1}, Prop 3.5g_{4}, Prop 3.5g_{2}, Prop 3.5g_{3}, Prop 3.5g, Prop 3.5h_{1}, Prop 3.5h_{2}, Prop 3.5h, Prop 3.5i_{1}, Prop 3.5i_{2}, Prop 3.5i, Prop 3.5j_{1}, Prop 3.5j_{2}, Prop 3.5j, Prop 3.7, Prop 3.7a, Prop 3.7b, Prop 3.7c, Prop 3.7d, Prop 3.7e, Prop 3.7f, Prop 3.7g, Prop 3.7g′, Prop 3.7h, Prop 3.7i, Prop 3.7j, Prop 3.7k, Prop 3.7k′, Prop 3.7l, Prop 3.7l′, Prop 3.7m, Prop 3.7n, Prop 3.7o, Prop 3.7p, Prop 3.7q, Prop 3.7r, Prop 3.7s, Prop 3.7t, Prop 3.7u, Prop 3.7u′, Prop 3.7v, Prop 3.7w, Prop 3.7x, Prop 3.7x′, Prop 3.7y, Prop 3.7y′, Prop 3.7z, Prop 3.7z′, Prop 3.10, Prop 3.10a, Prop 3.10b, Prop 3.10c, Prop 3.10d, Prop 3.10e, Prop 3.10f, Prop 3.10g, Prop 3.10h, Prop 3.11, ∗ < ∗, ∗ ≤ ∗, ∗ ≮ ∗, ∗ > ∗, ∗ ≥ ∗, ∗ ≯ ∗,

∗ ≠ ∗, ∗ ∧ ∗, ∗ ∨ ∗, ∃∗: ∗, ∗ | ∗, ∗ …,

S

[S →^{stmt} x]

Neg

[Neg →^{proof} Rule tactic]

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

MP

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

Gen

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

Ded

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

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}]

S2

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

S3

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

S4

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

S5

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

S6

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

S7

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

S8

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

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}]

Prop 3.2a

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

Prop 3.2b

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

Prop 3.2c

[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.2d

[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.2e

[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.2f

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

Prop 3.2g

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

Prop 3.2h

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

opgave

[opgave →^{prio} Preassociative [opgave], [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}(∗, ∗)], [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}(∗)], [\overline{0}], [\overline{1}], [\overline{2}], [\overline{3}], [\overline{4}], [\overline{5}], [\overline{6}], [\overline{7}], [\overline{8}], [\overline{9}], [\overline{n}], [rule div], [R], [R1], [R2], [R3], [R4], [R5], [R6], [Con1], [Con2], [Con], [Dis1], [Dis2], [Lem1.11c], [Cor1.10a], [Cor1.10b], [Lem1.11a], [Lem1.11b], [H3], [Prop3.2c′], [S1′′], [Neg′], [Repetition′], [Lem1.11e], [Lem1.11d], [Prop3.2b′], [H10], [H11], [Lem1.11g], [MT], [S10], [Prop 3.2], [Prop 3.2i], [Prop 3.2j_{1}], [Prop 3.2j_{2}], [Prop 3.2j], [Prop 3.2k_{1}], [Prop 3.2k_{2}], [Prop 3.2k], [Prop 3.2l_{1}], [Prop 3.2l_{2}], [Prop 3.2l], [Prop 3.2m_{1}], [Prop 3.2m_{2}], [Prop 3.2m], [Prop 3.2n_{1}], [Prop 3.2n_{2}], [Prop 3.2n], [Prop 3.2o], [Prop 3.4], [Prop 3.4a_{1}], [Prop 3.4a_{2}], [Prop 3.4a], [Prop 3.4b], [Prop 3.4c_{1}], [Prop 3.4c_{2}], [Prop 3.4c], [Prop 3.4d_{1}], [Prop 3.4d_{2}], [Prop 3.4d], [Prop 3.5], [Prop 3.5a], [Prop 3.5b], [Prop 3.5c], [Prop 3.5d_{1}], [Prop 3.5d_{2}], [Prop 3.5d], [Prop 3.5e_{1}], [Prop 3.5e_{2}], [Prop 3.5e], [Prop 3.5f_{1}], [Prop 3.5f_{2}], [Prop 3.5f], [Prop 3.5g_{1}], [Prop 3.5g_{4}], [Prop 3.5g_{2}], [Prop 3.5g_{3}], [Prop 3.5g], [Prop 3.5h_{1}], [Prop 3.5h_{2}], [Prop 3.5h], [Prop 3.5i_{1}], [Prop 3.5i_{2}], [Prop 3.5i], [Prop 3.5j_{1}], [Prop 3.5j_{2}], [Prop 3.5j], [Prop 3.7], [Prop 3.7a], [Prop 3.7b], [Prop 3.7c], [Prop 3.7d], [Prop 3.7e], [Prop 3.7f], [Prop 3.7g], [Prop 3.7g′], [Prop 3.7h], [Prop 3.7i], [Prop 3.7j], [Prop 3.7k], [Prop 3.7k′], [Prop 3.7l], [Prop 3.7l′], [Prop 3.7m], [Prop 3.7n], [Prop 3.7o], [Prop 3.7p], [Prop 3.7q], [Prop 3.7r], [Prop 3.7s], [Prop 3.7t], [Prop 3.7u], [Prop 3.7u′], [Prop 3.7v], [Prop 3.7w], [Prop 3.7x], [Prop 3.7x′], [Prop 3.7y], [Prop 3.7y′], [Prop 3.7z], [Prop 3.7z′], [Prop 3.10], [Prop 3.10a], [Prop 3.10b], [Prop 3.10c], [Prop 3.10d], [Prop 3.10e], [Prop 3.10f], [Prop 3.10g], [Prop 3.10h], [Prop 3.11]; 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] ∗], [∗\\∗], [∗ | ∗], [∗ …]; ]

[opgave →^{pyk} “opgave”]

\overline{0}

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

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

\overline{0}”]

[\overline{0} →^{pyk} “numeral zero”]

\overline{1}

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

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

\overline{1}”]

[\overline{1} →^{pyk} “numeral one”]

\overline{2}

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

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

\overline{2}”]

[\overline{2} →^{pyk} “numeral two”]

\overline{3}

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

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

\overline{3}”] [\overline{3} →^{pyk} “numeral three”]

\overline{4}

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

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

\overline{4}”] [\overline{4} →^{pyk} “numeral four”]

\overline{5}

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

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

\overline{5}”] [\overline{5} →^{pyk} “numeral five”]

\overline{6}

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

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

\overline{6}”] [\overline{6} →^{pyk} “numeral six”]

\overline{7}

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

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

\overline{7}”] [\overline{7} →^{pyk} “numeral seven”]

\overline{8}

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

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

\overline{8}”] [\overline{8} →^{pyk} “numeral eight”]

\overline{9}

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

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

\overline{9}”] [\overline{9} →^{pyk} “numeral nine”]

\overline{n}

[\overline{n} →^{tex} “

\overline{n}”] [\overline{n} →^{pyk} “numeral n”]

rule div

[rule div →^{pyk} “rule div”]

R

[R →^{tex} “

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

R1

[R1 →^{tex} “

R1”] [R1 →^{pyk} “rule r one”]

R2

[R2 →^{tex} “

R2”]

[R2 →^{pyk} “rule r two”]

R3

[R3 →^{tex} “

R3”]

[R3 →^{pyk} “rule r three”]

R4

[R4 →^{tex} “

R4”]

[R4 →^{pyk} “rule r four”]

R5

[R5 →^{tex} “

R5”]

[R5 →^{pyk} “rule r five”]

R6

[R6 →^{tex} “

R6”]

[R6 →^{pyk} “rule r six”]

Con1

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

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

[Con1 →^{tex} “

Con1”]

[Con1 →^{pyk} “conjel1”]

Con2

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

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

[Con2 →^{tex} “

Con2”]

[Con2 →^{pyk} “conjel2”]

Con

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

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

[Con →^{tex} “

Con”]

[Con →^{pyk} “conjin”]

Dis1

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

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

[Dis1 →^{tex} “

Dis1”]

[Dis1 →^{pyk} “disjin1”]

Dis2

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

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

[Dis2 →^{tex} “

Dis2”]

[Dis2 →^{pyk} “disjin2”]

Lem1.11c

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

[Lem1.11c →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⇒ \underline{a} ⇒ \underline{b}]

[Lem1.11c →^{tex} “

Lem 1.11c”]

[Lem1.11c →^{pyk} “t one”]

Cor1.10a

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

[Cor1.10a →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⊢ \underline{b} ⇒ \underline{c} ⊢ \underline{a} ⇒ \underline{c}]

[Cor1.10a →^{tex} “

Cor 1.10a”]

[Cor1.10a →^{pyk} “h zero a”]

Cor1.10b

[Cor1.10b →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{b} ⊢ A2′ ≫ \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{a} ⇒ \underline{b} ⇒ \underline{a} ⇒ \underline{c}; MP ⊳ \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}; A1′ ≫ \underline{b} ⇒ \underline{a} ⇒ \underline{b}; MP ⊳ \underline{b} ⇒ \underline{a} ⇒ \underline{b} ⊳ \underline{b} ≫ \underline{a} ⇒ \underline{b}; MP ⊳ \underline{a} ⇒ \underline{b} ⇒ \underline{a} ⇒ \underline{c} ⊳ \underline{a} ⇒ \underline{b} ≫ \underline{a} ⇒ \underline{c}⌉, p_{0}, c)]

[Cor1.10b →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{b} ⊢ \underline{a} ⇒ \underline{c}]

[Cor1.10b →^{tex} “

Cor 1.10b”]

[Cor1.10b →^{pyk} “h zero b”]

Lem1.11a

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

[Lem1.11a →^{stmt} S ⊢ ∀\underline{a}: ¬¬\underline{a} ⇒ \underline{a}]

[Lem1.11a →^{tex} “

Lem 1.11a”]

[Lem1.11a →^{pyk} “h one”]

Lem1.11b

[Lem1.11b →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: Neg′ ≫ ¬¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬¬¬\underline{a} ⇒ \underline{a} ⇒ ¬¬\underline{a}; Lem1.11a ≫ ¬¬¬\underline{a} ⇒ ¬\underline{a}; MP ⊳ ¬¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬¬¬\underline{a} ⇒ \underline{a} ⇒ ¬¬\underline{a} ⊳ ¬¬¬\underline{a} ⇒ ¬\underline{a} ≫ ¬¬¬\underline{a} ⇒ \underline{a} ⇒ ¬¬\underline{a}; A1′ ≫ \underline{a} ⇒ ¬¬¬\underline{a} ⇒ \underline{a}; Cor1.10a ⊳ \underline{a} ⇒ ¬¬¬\underline{a} ⇒ \underline{a} ⊳ ¬¬¬\underline{a} ⇒ \underline{a} ⇒ ¬¬\underline{a} ≫ \underline{a} ⇒ ¬¬\underline{a}⌉, p_{0}, c)]

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

[Lem1.11b →^{tex} “

Lem 1.11b”]

[Lem1.11b →^{pyk} “h two”]

H3

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

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

[H3 →^{tex} “

H3”]

[H3 →^{pyk} “h three”]

Prop3.2c′

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

[Prop3.2c′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⇒ \underline{b} = \underline{c} ⇒ \underline{a} = \underline{c}]

[Prop3.2c′ →^{tex} “ Prop 3.2c’”]

[Prop3.2c′ →^{pyk} “h four”]

S1′′

[S1′′ →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{c} ⊢ S1 ⊳ \underline{a} = \underline{b} ⊳ \underline{a} = \underline{c} ≫ \underline{b} = \underline{c}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \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}⌉, p_{0}, c)]

[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} “h four mark”]

Neg′

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

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

[Neg′ →^{tex} “

Neg’”]

[Neg′ →^{pyk} “h five”]

Repetition′

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

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

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

[Repetition′ →^{pyk} “h six”]

Lem1.11e

[Lem1.11e →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ Lem1.11a ≫ ¬¬\underline{a} ⇒ \underline{a}; Cor1.10a ⊳ ¬¬\underline{a} ⇒ \underline{a} ⊳ \underline{a} ⇒ \underline{b} ≫ ¬¬\underline{a} ⇒ \underline{b}; Lem1.11b ≫ \underline{b} ⇒ ¬¬\underline{b}; Cor1.10a ⊳ ¬¬\underline{a} ⇒ \underline{b} ⊳ \underline{b} ⇒ ¬¬\underline{b} ≫ ¬¬\underline{a} ⇒ ¬¬\underline{b}; Lem1.11d ≫ ¬¬\underline{a} ⇒ ¬¬\underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a}; MP ⊳ ¬¬\underline{a} ⇒ ¬¬\underline{b} ⇒ ¬\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}⌉, p_{0}, c)]

[Lem1.11e →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a}]

[Lem1.11e →^{tex} “

Lem 1.11e”]

[Lem1.11e →^{pyk} “h seven”]

Lem1.11d

[Lem1.11d →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⊢ Neg′ ≫ ¬\underline{b} ⇒ ¬\underline{a} ⇒ ¬\underline{b} ⇒ \underline{a} ⇒ \underline{b}; A1′ ≫ \underline{a} ⇒ ¬\underline{b} ⇒ \underline{a}; MP ⊳ ¬\underline{b} ⇒ ¬\underline{a} ⇒ ¬\underline{b} ⇒ \underline{a} ⇒ \underline{b} ⊳ ¬\underline{b} ⇒ ¬\underline{a} ≫ ¬\underline{b} ⇒ \underline{a} ⇒ \underline{b}; Cor1.10a ⊳ \underline{a} ⇒ ¬\underline{b} ⇒ \underline{a} ⊳ ¬\underline{b} ⇒ \underline{a} ⇒ \underline{b} ≫ \underline{a} ⇒ \underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⊢ \underline{a} ⇒ \underline{b} ≫ ¬\underline{b} ⇒ ¬\underline{a} ⇒ \underline{a} ⇒ \underline{b}⌉, p_{0}, c)]

[Lem1.11d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⇒ \underline{a} ⇒ \underline{b}]

[Lem1.11d →^{tex} “

Lem 1.11d”]

[Lem1.11d →^{pyk} “h eight”]

Prop3.2b′

[Prop3.2b′ →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ Prop 3.2b ⊳ \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}⌉, p_{0}, c)]

[Prop3.2b′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⇒ \underline{b} = \underline{a}]

[Prop3.2b′ →^{tex} “ Prop 3.2b’”]

[Prop3.2b′ →^{pyk} “h nine”]

H10

[H10 →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = \underline{a} ⊢ Prop3.2b′ ≫ \underline{a} = \underline{b} ⇒ \underline{b} = \underline{a}; Lem1.11e ≫ \underline{a} = \underline{b} ⇒ \underline{b} = \underline{a} ⇒ ¬\underline{b} = \underline{a} ⇒ ¬\underline{a} = \underline{b}; MP ⊳ \underline{a} = \underline{b} ⇒ \underline{b} = \underline{a} ⇒ ¬\underline{b} = \underline{a} ⇒ ¬\underline{a} = \underline{b} ⊳ \underline{a} = \underline{b} ⇒ \underline{b} = \underline{a} ≫ ¬\underline{b} = \underline{a} ⇒ ¬\underline{a} = \underline{b}; MP ⊳ ¬\underline{b} = \underline{a} ⇒ ¬\underline{a} = \underline{b} ⊳ ¬\underline{b} = \underline{a} ≫ ¬\underline{a} = \underline{b}⌉, p_{0}, c)]

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

[H10 →^{tex} “

H10”]

[H10 →^{pyk} “h ten”]

H11

[H11 →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} ⇒ \underline{b} ⊢ \underline{a} ⇒ \underline{c} ⊢ \underline{b} ⇒ \underline{c} ⊢ Cor1.10a ⊳ ¬\underline{a} ⇒ \underline{b} ⊳ \underline{b} ⇒ \underline{c} ≫ ¬\underline{a} ⇒ \underline{c}; Lem1.11g ⊳ \underline{a} ⇒ \underline{c} ⊳ ¬\underline{a} ⇒ \underline{c} ≫ \underline{c}⌉, p_{0}, c)]

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

[H11 →^{tex} “

H11”]

[H11 →^{pyk} “h eleven”]

Lem1.11g

[Lem1.11g →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ ¬\underline{a} ⇒ \underline{b} ⊢ Lem1.11e ≫ \underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a}; MP ⊳ \underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a} ⊳ \underline{a} ⇒ \underline{b} ≫ ¬\underline{b} ⇒ ¬\underline{a}; Lem1.11e ≫ ¬\underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬¬\underline{a}; MP ⊳ ¬\underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬¬\underline{a} ⊳ ¬\underline{a} ⇒ \underline{b} ≫ ¬\underline{b} ⇒ ¬¬\underline{a}; Neg ⊳ ¬\underline{b} ⇒ ¬¬\underline{a} ⊳ ¬\underline{b} ⇒ ¬\underline{a} ≫ \underline{b}⌉, p_{0}, c)] [Lem1.11g →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ ¬\underline{a} ⇒ \underline{b} ⊢ \underline{b}]

[Lem1.11g →^{tex} “

Lem 1.11g”]

[Lem1.11g →^{pyk} “h twelwe”]

MT

[MT →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ ¬\underline{b} ⊢ Lem1.11a ≫ ¬¬\underline{a} ⇒ \underline{a}; Cor1.10a ⊳ ¬¬\underline{a} ⇒ \underline{a} ⊳ \underline{a} ⇒ \underline{b} ≫ ¬¬\underline{a} ⇒ \underline{b}; ∀\underline{a}: ∀\underline{b}: ¬¬\underline{a} ⇒ \underline{b} ⊢ ¬\underline{b} ⊢ A1′ ≫ ¬\underline{b} ⇒ ¬¬\underline{a} ⇒ ¬\underline{b}; MP ⊳ ¬\underline{b} ⇒ ¬¬\underline{a} ⇒ ¬\underline{b} ⊳ ¬\underline{b} ≫ ¬¬\underline{a} ⇒ ¬\underline{b}; Neg ⊳ ¬¬\underline{a} ⇒ ¬\underline{b} ⊳ ¬¬\underline{a} ⇒ \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}; MP ⊳ ¬¬\underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a} ⊳ ¬¬\underline{a} ⇒ \underline{b} ≫ ¬\underline{b} ⇒ ¬\underline{a}; MP ⊳ ¬\underline{b} ⇒ ¬\underline{a} ⊳ ¬\underline{b} ≫ ¬\underline{a}⌉, p_{0}, c)]

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

[MT →^{tex} “

MT”]

[MT →^{pyk} “modus tollens”]

S10

[S10 →^{tex} “

S10”]

[S10 →^{pyk} “axiom s ten”]

Prop 3.2

[Prop 3.2 →^{tex} “

Prop\ 3.2”]

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

Prop 3.2i

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

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

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

Prop 3.2j_{1}

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

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

[Prop 3.2j_{1} →^{tex} “ Prop\ 3.2j 1”]

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

Prop 3.2j_{2}

[Prop 3.2j_{2} →^{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{c} ⊢ S6 ≫ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′; S2 ⊳ \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c} ≫ \underline{a} + \underline{b} + \underline{c}′ = \underline{a}+\underline{b}+\underline{c}′; Prop 3.2c⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′ ⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′ ≫ \underline{a}+\underline{b}+\underline{c}′ = \underline{a} + \underline{b} + \underline{c}′; S6 ≫ \underline{b} + \underline{c}′ = \underline{b} + \underline{c}′; Prop 3.2i ⊳ \underline{b} + \underline{c}′ = \underline{b} + \underline{c}′ ≫ \underline{a} + \underline{b} + \underline{c}′ = \underline{a}+\underline{b}+\underline{c}′; S6 ≫ \underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′; Prop 3.2c⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′ ≫ \underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′; Prop 3.2d⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′ ⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a} + \underline{b} + \underline{c}′ ≫ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c} ⊢ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′ ≫ \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c} ⇒ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′⌉, p_{0}, c)]

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

[Prop 3.2j_{2} →^{tex} “ Prop\ 3.2j 2”]

[Prop 3.2j_{2} →^{pyk} “prop three two j two”]

Prop 3.2j

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

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

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

Prop 3.2k_{1}

[Prop 3.2k_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ S7 ≫ \underline{a} · 0 = 0; S7 ≫ \underline{b} · 0 = 0; Prop 3.2a ≫ 0 = 0; Prop 3.2b⊳\underline{b}·0 = 0 ≫ 0 = \underline{b}·0; Prop 3.2c⊳\underline{a}·0 = 0⊳0 = \underline{b}·0 ≫ \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.2k_{1} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⇒ \underline{a} · 0 = \underline{b} · 0]

[Prop 3.2k_{1} →^{tex} “ Prop\ 3.2k 1”]

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

Prop 3.2k_{2}

[Prop 3.2k_{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}; S8 ≫ \underline{a} · \underline{c}′ = \underline{a} · \underline{c} + \underline{a}; S8 ≫ \underline{b} · \underline{c}′ = \underline{b} · \underline{c} + \underline{b}; Prop 3.2e ⊳ \underline{a} · \underline{c} = \underline{b} · \underline{c} ≫ \underline{a} · \underline{c} + \underline{a} = \underline{b} · \underline{c} + \underline{a}; Prop 3.2i ⊳ \underline{a} = \underline{b} ≫ \underline{b} · \underline{c} + \underline{a} = \underline{b} · \underline{c} + \underline{b}; Prop 3.2c ⊳ \underline{a} · \underline{c} + \underline{a} = \underline{b} · \underline{c} + \underline{a} ⊳ \underline{b} · \underline{c} + \underline{a} = \underline{b} · \underline{c} + \underline{b} ≫ \underline{a} · \underline{c} + \underline{a} = \underline{b}·\underline{c}+\underline{b}; Prop 3.2c⊳\underline{a}·\underline{c}′ = \underline{a}·\underline{c}+\underline{a}⊳\underline{a}·\underline{c}+\underline{a} = \underline{b}·\underline{c}+\underline{b} ≫ \underline{a}·\underline{c}′ = \underline{b}·\underline{c}+\underline{b}; Prop 3.2d⊳ \underline{a} · \underline{c}′ = \underline{b} · \underline{c} + \underline{b} ⊳ \underline{b} · \underline{c}′ = \underline{b} · \underline{c} + \underline{b} ≫ \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.2k_{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.2k_{2} →^{tex} “ Prop\ 3.2k 2”]

[Prop 3.2k_{2} →^{pyk} “prop three two k two”]

Prop 3.2k

[Prop 3.2k →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ Prop 3.2k_{1} ≫ \overline{x} = \overline{y} ⇒ \overline{x} · 0 = \overline{y} · 0; Prop 3.2k_{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.2k →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{a} · \underline{c} = \underline{b} · \underline{c}]

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

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

Prop 3.2l_{1}

[Prop 3.2l_{1} →^{tex} “ Prop\ 3.2l 1”]

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

Prop 3.2l_{2}

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

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

[Prop 3.2l_{2} →^{tex} “ Prop\ 3.2l 2”]

[Prop 3.2l_{2} →^{pyk} “prop three two l two”]

Prop 3.2l

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

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

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

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

Prop 3.2m_{1}

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

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

[Prop 3.2m_{1} →^{tex} “ Prop\ 3.2m 1”]

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

Prop 3.2m_{2}

[Prop 3.2m_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ⊢ S8 ≫ \underline{a}′ · \underline{b}′ = \underline{a}′ · \underline{b} + \underline{a}′; Prop 3.2e ⊳ \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ≫ \underline{a}′ · \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{b} + \underline{a}′; S6 ≫ \underline{b} + \underline{a}′ = \underline{b} + \underline{a}′; Prop 3.2g ≫ \underline{b}′ + \underline{a} = \underline{b} + \underline{a}′; Prop 3.2d ⊳ \underline{b} + \underline{a}′ = \underline{b} + \underline{a}′ ⊳ \underline{b}′ + \underline{a} = \underline{b} + \underline{a}′ ≫ \underline{b} + \underline{a}′ = \underline{b}′ + \underline{a}; Prop 3.2h ≫ \underline{b}′ + \underline{a} = \underline{a} + \underline{b}′; Prop 3.2c ⊳ \underline{b} + \underline{a}′ = \underline{b}′ + \underline{a} ⊳ \underline{b}′ + \underline{a} = \underline{a} + \underline{b}′ ≫ \underline{b} + \underline{a}′ = \underline{a} + \underline{b}′; Prop 3.2i ⊳ \underline{b} + \underline{a}′ = \underline{a} + \underline{b}′ ≫ \underline{a} · \underline{b} + \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{a} + \underline{b}′; Prop 3.2j ≫ \underline{a} · \underline{b} + \underline{a} + \underline{b}′ = \underline{a} · \underline{b} + \underline{a} + \underline{b}′; Prop 3.2d ⊳ \underline{a} · \underline{b} + \underline{b} + \underline{a}′ = \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{b}+\underline{a}′ = \underline{a}·\underline{b}+\underline{a}+\underline{b}′; S8 ≫ \underline{a}·\underline{b}′ = \underline{a}·\underline{b}+\underline{a}; Prop 3.2e⊳\underline{a}·\underline{b}′ = \underline{a}·\underline{b}+\underline{a} ≫ \underline{a}·\underline{b}′+\underline{b}′ = \underline{a}·\underline{b}+\underline{a}+\underline{b}′; Prop 3.2d⊳\underline{a}·\underline{b}+\underline{b}+\underline{a}′ = \underline{a} · \underline{b} + \underline{a} + \underline{b}′ ⊳ \underline{a} · \underline{b}′ + \underline{b}′ = \underline{a} · \underline{b} + \underline{a} + \underline{b}′ ≫ \underline{a} · \underline{b} + \underline{b} + \underline{a}′ = \underline{a} · \underline{b}′ + \underline{b}′; Prop 3.2j ≫ \underline{a} · \underline{b} + \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{b} + \underline{a}′; Prop 3.2c ⊳ \underline{a}′ · \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}′ ≫ \underline{a}′ · \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{b} + \underline{a}′; Prop 3.2c ⊳ \underline{a}′ · \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}′ ·\underline{b}+\underline{a}′ = \underline{a}·\underline{b}′ +\underline{b}′; Prop 3.2c⊳\underline{a}′ ·\underline{b}′ = \underline{a}′ · \underline{b} + \underline{a}′ ⊳ \underline{a}′ · \underline{b} + \underline{a}′ = \underline{a} · \underline{b}′ + \underline{b}′ ≫ \underline{a}′ · \underline{b}′ = \underline{a} · \underline{b}′ + \underline{b}′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ⊢ \underline{a}′ · \underline{b}′ = \underline{a} · \underline{b}′ + \underline{b}′ ≫ \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ⇒ \underline{a}′ · \underline{b}′ = \underline{a} · \underline{b}′ + \underline{b}′⌉, p_{0}, c)]

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

[Prop 3.2m_{2} →^{tex} “ Prop\ 3.2m 2”]

[Prop 3.2m_{2} →^{pyk} “prop three two m two”]

Prop 3.2m

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

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

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

Prop 3.2n_{1}

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

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

[Prop 3.2n_{1} →^{tex} “ Prop\ 3.2n 1”]

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

Prop 3.2n_{2}

[Prop 3.2n_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = \underline{b} · \underline{a} ⊢ S8 ≫ \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a}; Prop 3.2e ⊳ \underline{a} · \underline{b} = \underline{b} · \underline{a} ≫ \underline{a} · \underline{b} + \underline{a} = \underline{b} · \underline{a} + \underline{a}; Prop 3.2m ≫ \underline{b}′ · \underline{a} = \underline{b}·\underline{a}+\underline{a}; Prop 3.2b⊳\underline{b}′·\underline{a} = \underline{b}·\underline{a}+\underline{a} ≫ \underline{b}·\underline{a}+\underline{a} = \underline{b}′·\underline{a}; Prop 3.2c⊳\underline{a}·\underline{b}+\underline{a} = \underline{b}·\underline{a}+\underline{a}⊳ \underline{b}·\underline{a}+\underline{a} = \underline{b}′·\underline{a} ≫ \underline{a}·\underline{b}+\underline{a} = \underline{b}′·\underline{a}; Prop 3.2c⊳\underline{a}·\underline{b}′ = \underline{a}·\underline{b}+\underline{a}⊳\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.2n_{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.2n_{2} →^{tex} “ Prop\ 3.2n 2”]

[Prop 3.2n_{2} →^{pyk} “prop three two n two”]

Prop 3.2n

[Prop 3.2n →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: Prop 3.2n_{1} ≫ \overline{x} · 0 = 0 · \overline{x}; Prop 3.2n_{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.2n →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = \underline{b} · \underline{a}]

[Prop 3.2n →^{tex} “ Prop\ 3.2n”] [Prop 3.2n →^{pyk} “prop three two n”]

Prop 3.2o

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

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

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

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

Prop 3.4

[Prop 3.4 →^{tex} “

Prop\ 3.4”]

[Prop 3.4 →^{pyk} “prop three four”]

Prop 3.4a_{1}

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

[Prop 3.4a_{1} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} + 0 = \underline{a} · \underline{b} + \underline{a} · 0]

[Prop 3.4a_{1} →^{tex} “ Prop\ 3.4a 1”]

[Prop 3.4a_{1} →^{pyk} “prop three four a one”]

Prop 3.4a_{2}

[Prop 3.4a_{2} →^{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} · \underline{c} ⊢ S6 ≫ \underline{b} + \underline{c}′ = \underline{b} + \underline{c}′; Prop 3.2o ⊳ \underline{b} + \underline{c}′ = \underline{b} + \underline{c}′ ≫ \underline{a} · \underline{b} + \underline{c}′ = \underline{a} · \underline{b} + \underline{c}′; S8 ≫ \underline{a} · \underline{b} + \underline{c}′ = \underline{a}·\underline{b}+\underline{c}+\underline{a}; Prop 3.2e⊳\underline{a}·\underline{b}+\underline{c} = \underline{a}·\underline{b}+\underline{a}·\underline{c} ≫ \underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}; Prop 3.2j ≫ \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}; Prop 3.2c⊳\underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}⊳\underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a} ≫ \underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}; S8 ≫ \underline{a}·\underline{c}′ = \underline{a}·\underline{c}+\underline{a}; Prop 3.2i⊳\underline{a}·\underline{c}′ = \underline{a}·\underline{c}+\underline{a} ≫ \underline{a}·\underline{b}+\underline{a}·\underline{c}′ = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}; Prop 3.2d⊳\underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}⊳\underline{a}·\underline{b}+\underline{a}·\underline{c}′ = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a} ≫ \underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}′; Prop 3.2c⊳\underline{a}·\underline{b}+\underline{c}′ = \underline{a}·\underline{b}+\underline{c}+\underline{a}⊳\underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a} · \underline{b} + \underline{a} · \underline{c}′ ≫ \underline{a} · \underline{b} + \underline{c}′ = \underline{a} · \underline{b} + \underline{a} · \underline{c}′; Prop 3.2c ⊳ \underline{a} · \underline{b} + \underline{c}′ = \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}′; 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}′ ≫ \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)]

[Prop 3.4a_{2} →^{stmt} S ⊢ ∀\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}′]

[Prop 3.4a_{2} →^{tex} “ Prop\ 3.4a 2”]

[Prop 3.4a_{2} →^{pyk} “prop three four a two”]

Prop 3.4a

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

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

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

[Prop 3.4a →^{pyk} “prop three four a”]

Prop 3.4b

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

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

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

[Prop 3.4b →^{pyk} “prop three four b”]

Prop 3.4c_{1}

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

[Prop 3.4c_{1} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} · 0 = \underline{a} · \underline{b} · 0]

[Prop 3.4c_{1} →^{tex} “ Prop\ 3.4c 1”]

[Prop 3.4c_{1} →^{pyk} “prop three four c one”]

Prop 3.4c_{2}

[Prop 3.4c_{2} →^{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{c} ⊢ S8 ≫ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b}; Prop 3.2e ⊳ \underline{a} · \underline{b} · \underline{c} = \underline{a} · \underline{b} · \underline{c} ≫ \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b}; Prop 3.2c ⊳ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} ⊳ \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} ≫ \underline{a}·\underline{b}·\underline{c}′ = \underline{a}·\underline{b}·\underline{c}+\underline{a}·\underline{b}; Prop 3.4a ≫ \underline{a}·\underline{b}·\underline{c}+\underline{b} = \underline{a}·\underline{b}·\underline{c}+\underline{a}·\underline{b}; Prop 3.2d⊳\underline{a}·\underline{b}·\underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} ⊳ \underline{a} · \underline{b} · \underline{c} + \underline{b} = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} ≫ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{b}; S8 ≫ \underline{b} · \underline{c}′ = \underline{b} · \underline{c} + \underline{b}; Prop 3.2o ⊳ \underline{b} · \underline{c}′ = \underline{b} · \underline{c} + \underline{b} ≫ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{b}; Prop 3.2d ⊳ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{b} ⊳ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{b} ≫ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c}′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · \underline{b} · \underline{c} = \underline{a} · \underline{b} · \underline{c} ⊢ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c}′ ≫ \underline{a} · \underline{b} · \underline{c} = \underline{a} · \underline{b} · \underline{c} ⇒ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c}′⌉, p_{0}, c)]

[Prop 3.4c_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · \underline{b} · \underline{c} = \underline{a} · \underline{b} · \underline{c} ⇒ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c}′]

[Prop 3.4c_{2} →^{tex} “ Prop\ 3.4c 2”]

[Prop 3.4c_{2} →^{pyk} “prop three four c two”]

Prop 3.4c

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

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

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

[Prop 3.4c →^{pyk} “prop three four c”]

Prop 3.4d_{1}

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

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

[Prop 3.4d_{1} →^{tex} “ Prop\ 3.4d 1”]

[Prop 3.4d_{1} →^{pyk} “prop three four d one”]

Prop 3.4d_{2}

[Prop 3.4d_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} = \underline{b} ⊢ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′ ⊢ S6 ≫ \underline{a} + \underline{c}′ = \underline{a} + \underline{c}′; S6 ≫ \underline{b} + \underline{c}′ = \underline{b} + \underline{c}′; S1 ⊳ \underline{a} + \underline{c}′ = \underline{a} + \underline{c}′ ⊳ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′ ≫ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′; Prop 3.2c ⊳ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′ ⊳ \underline{b} + \underline{c}′ = \underline{b}+\underline{c}′ ≫ \underline{a}+\underline{c}′ = \underline{b}+\underline{c}′; S4⊳\underline{a}+\underline{c}′ = \underline{b}+\underline{c}′ ≫ \underline{a}+\underline{c} = \underline{b}+\underline{c}; MP⊳\underline{a}+\underline{c} = \underline{b}+\underline{c} ⇒ \underline{a} = \underline{b} ⊳ \underline{a} + \underline{c} = \underline{b} + \underline{c} ≫ \underline{a} = \underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \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}′ ⇒ \underline{a} = \underline{b}⌉, p_{0}, c)]

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

[Prop 3.4d_{2} →^{tex} “ Prop\ 3.4d 2”]

[Prop 3.4d_{2} →^{pyk} “prop three four d two”]

Prop 3.4d

[Prop 3.4d →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: Prop 3.4d_{1} ≫ \overline{x} + 0 = \overline{y} + 0 ⇒ \overline{x} = \overline{y}; Prop 3.4d_{2} ≫ \overline{x}+\overline{z} = \overline{y} +\overline{z} ⇒ \overline{x} = \overline{y} ⇒ \overline{x}+\overline{z}′ = \overline{y} +\overline{z}′ ⇒ \overline{x} = \overline{y}; S9 @ \overline{z}⊳\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} ⇒ \overline{x} = \overline{y}; Ded ⊳ \overline{x} + \overline{z} = \overline{y} + \overline{z} ⇒ \overline{x} = \overline{y} ≫ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} = \underline{b}⌉, p_{0}, c)]

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

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

[Prop 3.4d →^{pyk} “prop three four d”]

Prop 3.5

[Prop 3.5 →^{tex} “

Prop\ 3.5”]

[Prop 3.5 →^{pyk} “prop three five”]

Prop 3.5a

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

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

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

[Prop 3.5a →^{pyk} “prop three five a”]

Prop 3.5b

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

[Prop 3.5b →^{stmt} S ⊢ ∀\underline{a}: \underline{a} · 0′ = \underline{a}]

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

[Prop 3.5b →^{pyk} “prop three five b”]

Prop 3.5c

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

[Prop 3.5c →^{stmt} S ⊢ ∀\underline{a}: \underline{a} · 0′′ = \underline{a} + \underline{a}] [Prop 3.5c →^{tex} “ Prop\ 3.5c”]

[Prop 3.5c →^{pyk} “prop three five c”]

Prop 3.5d_{1}

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

[Prop 3.5d_{1} →^{stmt} S ⊢ ∀\underline{a}: \underline{a} + 0 = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬0 = 0]

[Prop 3.5d_{1} →^{tex} “ Prop\ 3.5d 1”]

[Prop 3.5d_{1} →^{pyk} “prop three five d one”]

Prop 3.5d_{2}

[Prop 3.5d_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b}′ = 0 ⊢ S3 ≫ ¬0 = \underline{a} + \underline{b}′; Prop3.2b′ ≫ \underline{a} + \underline{b}′ = 0 ⇒ 0 = \underline{a} + \underline{b}′; Lem1.11e ≫ \underline{a} + \underline{b}′ = 0 ⇒ 0 = \underline{a} + \underline{b}′ ⇒ ¬0 = \underline{a} + \underline{b}′ ⇒ ¬\underline{a} + \underline{b}′ = 0; MP ⊳ \underline{a} + \underline{b}′ = 0 ⇒ 0 = \underline{a} + \underline{b}′ ⇒ ¬0 = \underline{a} + \underline{b}′ ⇒ ¬\underline{a} + \underline{b}′ = 0 ⊳ \underline{a} + \underline{b}′ = 0 ⇒ 0 = \underline{a} + \underline{b}′ ≫ ¬0 = \underline{a} + \underline{b}′ ⇒ ¬\underline{a} + \underline{b}′ = 0; MP ⊳ ¬0 = \underline{a} + \underline{b}′ ⇒ ¬\underline{a} + \underline{b}′ = 0 ⊳ ¬0 = \underline{a} + \underline{b}′ ≫ ¬\underline{a} + \underline{b}′ = 0; S6 ≫ \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′; S1′′ ≫ \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′ ⇒ \underline{a} + \underline{b}′ = 0 ⇒ \underline{a} + \underline{b}′ = 0; H3 ⊳ \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′ ⇒ \underline{a} + \underline{b}′ = 0 ⇒ \underline{a} + \underline{b}′ = 0 ⊳ \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′ ⊳ ¬\underline{a} + \underline{b}′ = 0 ≫ ¬\underline{a} + \underline{b}′ = 0; Lem1.11c ≫ ¬\underline{a} + \underline{b}′ = 0 ⇒ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0; MP ⊳ ¬\underline{a} + \underline{b}′ = 0 ⇒ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0 ⊳ ¬\underline{a} + \underline{b}′ = 0 ≫ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0; MP ⊳ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0 ⊳ \underline{a} + \underline{b}′ = 0 ≫ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b}′ = 0 ⊢ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0 ≫ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ⊢ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0 ≫ \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ⇒ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0⌉, p_{0}, c)]

[Prop 3.5d_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ⇒ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0]

[Prop 3.5d_{2} →^{tex} “ Prop\ 3.5d 2”]

[Prop 3.5d_{2} →^{pyk} “prop three five d two”]

Prop 3.5d

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

[Prop 3.5d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0]

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

[Prop 3.5d →^{pyk} “prop three five d”]

Prop 3.5e_{1}

[Prop 3.5e_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{a}: ¬0 = 0 ⊢ Prop 3.2a ≫ 0 = 0; Lem1.11c ≫ ¬0 = 0 ⇒ 0 = 0 ⇒ \underline{a} · 0 = 0 ⇒ \underline{a} = 0; MP ⊳ ¬0 = 0 ⇒ 0 = 0 ⇒ \underline{a} · 0 = 0 ⇒ \underline{a} = 0 ⊳ ¬0 = 0 ≫ 0 = 0 ⇒ \underline{a} · 0 = 0 ⇒ \underline{a} = 0; MP ⊳ 0 = 0 ⇒ \underline{a} · 0 = 0 ⇒ \underline{a} = 0 ⊳ 0 = 0 ≫ \underline{a} · 0 = 0 ⇒ \underline{a} = 0; Ded ⊳ ∀\underline{a}: ¬0 = 0 ⊢ \underline{a} · 0 = 0 ⇒ \underline{a} = 0 ≫ ¬0 = 0 ⇒ \underline{a} · 0 = 0 ⇒ \underline{a} = 0⌉, p_{0}, c)]

[Prop 3.5e_{1} →^{stmt} S ⊢ ∀\underline{a}: ¬0 = 0 ⇒ \underline{a} · 0 = 0 ⇒ \underline{a} = 0]

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

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

Prop 3.5e_{2}

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

[Prop 3.5e_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = 0 ⇒ \underline{a} · \underline{b} = 0 ⇒ \underline{a} = 0 ⇒ ¬\underline{b}′ = 0 ⇒ \underline{a} · \underline{b}′ = 0 ⇒ \underline{a} = 0]

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

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

Prop 3.5e

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

[Prop 3.5e →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = 0 ⇒ \underline{a} · \underline{b} = 0 ⇒ \underline{a} = 0]

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

[Prop 3.5e →^{pyk} “prop three five e”]

Prop 3.5f_{1}

[Prop 3.5f_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{a}: \underline{a} + 0 = 0′ ⊢ S5 ≫ \underline{a} + 0 = \underline{a}; S1 ⊳ \underline{a} + 0 = \underline{a} ⊳ \underline{a} + 0 = 0′ ≫ \underline{a} = 0′; Prop 3.2a ≫ 0 = 0; Con ⊳ \underline{a} = 0′ ⊳ 0 = 0 ≫ ¬\underline{a} = 0′ ⇒ ¬0 = 0; Dis2 ⊳ ¬\underline{a} = 0′ ⇒ ¬0 = 0 ≫ ¬¬\underline{a} = 0 ⇒ ¬0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0; Ded ⊳ ∀\underline{a}: \underline{a} + 0 = 0′ ⊢ ¬¬\underline{a} = 0 ⇒ ¬0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0 ≫ \underline{a} + 0 = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0⌉, p_{0}, c)]

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

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

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

Prop 3.5f_{2}

[Prop 3.5f_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0 ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b}′ = 0′ ⊢ S6 ≫ \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′; S1 ⊳ \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′ ⊳ \underline{a} + \underline{b}′ = 0′ ≫ \underline{a} + \underline{b}′ = 0′; S4 ⊳ \underline{a} + \underline{b}′ = 0′ ≫ \underline{a} + \underline{b} = 0; Prop 3.5d ≫ \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0; MP ⊳ \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ⊳ \underline{a} + \underline{b} = 0 ≫ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0; Con1 ⊳ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ≫ \underline{a} = 0; Con2 ⊳ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ≫ \underline{b} = 0; S2 ⊳ \underline{b} = 0 ≫ \underline{b}′ = 0′; Con ⊳ \underline{a} = 0 ⊳ \underline{b}′ = 0′ ≫ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′; Dis1 ⊳ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′ ≫ ¬¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b}′ = 0′ ⊢ ¬¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0 ≫ \underline{a} + \underline{b}′ = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0; Ded⊳∀\underline{a}: ∀\underline{b}: \underline{a}+\underline{b} = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0 ⊢ \underline{a} + \underline{b}′ = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0 ≫ \underline{a} + \underline{b} = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0 ⇒ \underline{a} + \underline{b}′ = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0⌉, p_{0}, c)]

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

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

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

Prop 3.5f

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

[Prop 3.5f →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0]

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

[Prop 3.5f →^{pyk} “prop three five f”]

Prop 3.5g_{1}

[Prop 3.5g_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{a}: \underline{a} · 0 = 0′ ⊢ S7 ≫ \underline{a} · 0 = 0; S1 ⊳ \underline{a} · 0 = 0 ⊳ \underline{a} · 0 = 0′ ≫ 0 = 0′; S3 ≫ ¬0 = 0′; Lem1.11c ≫ ¬0 = 0′ ⇒ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0′; MP ⊳ ¬0 = 0′ ⇒ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0′ ⊳ ¬0 = 0′ ≫ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0′; MP ⊳ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0′ ⊳ 0 = 0′ ≫ ¬\underline{a} = 0′ ⇒ ¬0 = 0′; Ded ⊳ ∀\underline{a}: \underline{a} · 0 = 0′ ⊢ ¬\underline{a} = 0′ ⇒ ¬0 = 0′ ≫ \underline{a} · 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0′⌉, p_{0}, c)]

[Prop 3.5g_{1} →^{stmt} S ⊢ ∀\underline{a}: \underline{a} · 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0′]

[Prop 3.5g_{1} →^{tex} “ Prop\ 3.5g 1”] [Prop 3.5g_{1} →^{pyk} “prop three five g one”]

Prop 3.5g_{4}

[Prop 3.5g_{4} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⊢ \underline{a} · \underline{b}′ = 0′ ⊢ S8 ≫ \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a}; S1 ⊳ \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a} ⊳ \underline{a} · \underline{b}′ = 0′ ≫ \underline{a} · \underline{b} + \underline{a} = 0′; Prop 3.5f ≫ \underline{a} · \underline{b} + \underline{a} = 0′ ⇒ ¬¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0; MP ⊳ \underline{a} · \underline{b} + \underline{a} = 0′ ⇒ ¬¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0⊳\underline{a}·\underline{b}+\underline{a} = 0′ ≫ ¬¬\underline{a}·\underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a}·\underline{b} = 0′ ⇒ ¬\underline{a} = 0; Prop 3.5g_{2} ≫ ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; Prop 3.5g_{3} ⊳ \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ≫ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; H11 ⊳ ¬¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⊳ ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ⊳ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ≫ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⊢ \underline{a} · \underline{b}′ = 0′ ⊢ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ≫ \underline{a}·\underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⇒ \underline{a}·\underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′⌉, p_{0}, c)]

[Prop 3.5g_{4} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⇒ \underline{a} · \underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′]

[Prop 3.5g_{4} →^{tex} “ Prop\ 3.5g 4”]

[Prop 3.5g_{4} →^{pyk} “prop three five g two”]

Prop 3.5g_{2}

[Prop 3.5g_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⊢ Con2 ⊳ ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ≫ \underline{a} = 0′; Con1 ⊳ ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ≫ \underline{a} · \underline{b} = 0; S3 ≫ ¬0 = 0′; H10 ⊳ ¬0 = 0′ ≫ ¬0′ = 0; S1′′ ≫ \underline{a} = 0′ ⇒ \underline{a} = 0 ⇒ 0′ = 0; H3 ⊳ \underline{a} = 0′ ⇒ \underline{a} = 0 ⇒ 0′ = 0 ⊳ \underline{a} = 0′ ⊳ ¬0′ = 0 ≫ ¬\underline{a} = 0; Prop 3.2n ≫ \underline{a} · \underline{b} = \underline{b} · \underline{a}; S1 ⊳ \underline{a} · \underline{b} = \underline{b} · \underline{a} ⊳ \underline{a} · \underline{b} = 0 ≫ \underline{b} · \underline{a} = 0; Prop 3.5e ≫ ¬\underline{a} = 0 ⇒ \underline{b} · \underline{a} = 0 ⇒ \underline{b} = 0; MP ⊳ ¬\underline{a} = 0 ⇒ \underline{b} · \underline{a} = 0 ⇒ \underline{b} = 0 ⊳ ¬\underline{a} = 0 ≫ \underline{b} · \underline{a} = 0 ⇒ \underline{b} = 0; MP ⊳ \underline{b} · \underline{a} = 0 ⇒ \underline{b} = 0 ⊳ \underline{b} · \underline{a} = 0 ≫ \underline{b} = 0; S2 ⊳ \underline{b} = 0 ≫ \underline{b}′ = 0′; Con ⊳ \underline{a} = 0′ ⊳ \underline{b}′ = 0′ ≫ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⊢ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ≫ ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′⌉, p_{0}, c)]

[Prop 3.5g_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′]

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

[Prop 3.5g_{2} →^{pyk} “prop three five g three”]

Prop 3.5g_{3}

[Prop 3.5g_{3} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⊢ Con1 ⊳ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ≫ \underline{a} · \underline{b} = 0′; MP ⊳ \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⊳ \underline{a} · \underline{b} = 0′ ≫ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′; Con1 ⊳ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ≫ \underline{a} = 0′; Con2 ⊳ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ≫ \underline{a} = 0; S1 ⊳ \underline{a} = 0 ⊳ \underline{a} = 0′ ≫ 0 = 0′; S3 ≫ ¬0 = 0′; Lem1.11c ≫ ¬0 = 0′ ⇒ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; MP ⊳ ¬0 = 0′ ⇒ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ⊳ ¬0 = 0′ ≫ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; MP ⊳ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ⊳ 0 = 0′ ≫ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⊢ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ≫ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′⌉, p_{0}, c)]

[Prop 3.5g_{3} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⊢ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′]

[Prop 3.5g_{3} →^{tex} “ Prop\ 3.5g 3”]

[Prop 3.5g_{3} →^{pyk} “prop three five g four”]

Prop 3.5g

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

[Prop 3.5g →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′]

[Prop 3.5g →^{tex} “ Prop\ 3.5g”]

[Prop 3.5g →^{pyk} “prop three five g”]

Prop 3.5h_{1}

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

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

Prop 3.5h_{2}

[Prop 3.5h_{2} →^{tex} “ Prop\ 3.5h 2”] [Prop 3.5h_{2} →^{pyk} “prop three five h two”]

Prop 3.5h

[Prop 3.5h →^{stmt} S ⊢ ∀\underline{a}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}\underline{b}: ¬\underline{a} = \underline{b}′] [Prop 3.5h →^{tex} “ Prop\ 3.5h”] [Prop 3.5h →^{pyk} “prop three five h”]

Prop 3.5i_{1}

[Prop 3.5i_{1} →^{tex} “ Prop\ 3.5i 1”] [Prop 3.5i_{1} →^{pyk} “prop three five i one”]

Prop 3.5i_{2}

[Prop 3.5i_{2} →^{tex} “ Prop\ 3.5i 2”] [Prop 3.5i_{2} →^{pyk} “prop three five i two”]

Prop 3.5i

[Prop 3.5i →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{c} = 0 ⇒ \underline{a} · \underline{c} = \underline{b} · \underline{c} ⇒ \underline{a} = \underline{b}] [Prop 3.5i →^{tex} “ Prop\ 3.5i”] [Prop 3.5i →^{pyk} “prop three five i”]

Prop 3.5j_{1}

[Prop 3.5j_{1} →^{tex} “ Prop\ 3.5j 1”] [Prop 3.5j_{1} →^{pyk} “prop three five j one”]

Prop 3.5j_{2}

[Prop 3.5j_{2} →^{tex} “ Prop\ 3.5j 2”] [Prop 3.5j_{2} →^{pyk} “prop three five j two”]

Prop 3.5j

[Prop 3.5j →^{stmt} S ⊢ ∀\underline{a}: ¬\underline{a} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬∀_{obj}\underline{b}: ¬\underline{a} = \underline{b}′′] [Prop 3.5j →^{tex} “ Prop\ 3.5j”] [Prop 3.5j →^{pyk} “prop three five j”]

Prop 3.7

[Prop 3.7 →^{tex} “

Prop\ 3.7”] [Prop 3.7 →^{pyk} “prop three seven”]

Prop 3.7a

[Prop 3.7a →^{stmt} S ⊢ ∀\underline{a}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a}] [Prop 3.7a →^{tex} “ Prop\ 3.7a”] [Prop 3.7a →^{pyk} “prop three seven a”]

Prop 3.7b

[Prop 3.7b →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{c}]

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

[Prop 3.7b →^{pyk} “prop three seven b”]

Prop 3.7c

[Prop 3.7c →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{a}]

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

[Prop 3.7c →^{pyk} “prop three seven c”]

Prop 3.7d

[Prop 3.7d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} + \underline{c} = \underline{b} + \underline{c}]

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

[Prop 3.7d →^{pyk} “prop three seven d”]

Prop 3.7e

[Prop 3.7e →^{stmt} S ⊢ ∀\underline{a}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a} ⇒ \underline{a} = \underline{a}]

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

[Prop 3.7e →^{pyk} “prop three seven e”]

Prop 3.7f

[Prop 3.7f →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c} ⇒ \underline{b} = \underline{c} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{c} ⇒ \underline{a} = \underline{c}]

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

[Prop 3.7f →^{pyk} “prop three seven f”]

Prop 3.7g

[Prop 3.7g →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c}]

[Prop 3.7g →^{tex} “ Prop\ 3.7g”]

[Prop 3.7g →^{pyk} “prop three seven g”]

Prop 3.7g′

[Prop 3.7g′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b}]

[Prop 3.7g′ →^{tex} “ Prop\ 3.7g’”]

[Prop 3.7g′ →^{pyk} “prop three seven g mark”]

Prop 3.7h

[Prop 3.7h →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{c}]

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

[Prop 3.7h →^{pyk} “prop three seven h”]

Prop 3.7i

[Prop 3.7i →^{stmt} S ⊢ ∀\underline{a}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{a} ⇒ 0 = \underline{a}]

[Prop 3.7i →^{tex} “ Prop\ 3.7i”]

[Prop 3.7i →^{pyk} “prop three seven i”]

Prop 3.7j

[Prop 3.7j →^{stmt} S ⊢ ∀\underline{a}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{a}′]

[Prop 3.7j →^{tex} “ Prop\ 3.7j”]

[Prop 3.7j →^{pyk} “prop three seven j”]

Prop 3.7k

[Prop 3.7k →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a}′ = \underline{b} ⇒ \underline{a}′ = \underline{b}]

[Prop 3.7k →^{tex} “ Prop\ 3.7k”]

[Prop 3.7k →^{pyk} “prop three seven k”]

Prop 3.7k′

[Prop 3.7k′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a}′ = \underline{b} ⇒ \underline{a}′ = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b}]

[Prop 3.7k′ →^{tex} “ Prop\ 3.7k’”]

[Prop 3.7k′ →^{pyk} “prop three seven k mark”]

Prop 3.7l

[Prop 3.7l →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b}′] [Prop 3.7l →^{tex} “ Prop\ 3.7l”]

[Prop 3.7l →^{pyk} “prop three seven l”]

Prop 3.7l′

[Prop 3.7l′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b}′ ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b}]

[Prop 3.7l′ →^{tex} “ Prop\ 3.7l’”]

[Prop 3.7l′ →^{pyk} “prop three seven l mark”]

Prop 3.7m

[Prop 3.7m →^{stmt} S ⊢ ∀\underline{a}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a}′]

[Prop 3.7m →^{tex} “ Prop\ 3.7m”]

[Prop 3.7m →^{pyk} “prop three seven m”]

Prop 3.7n

[Prop 3.7n →^{tex} “ Prop\ 3.7n”]

[Prop 3.7n →^{pyk} “prop three seven n”]

Prop 3.7o

[Prop 3.7o →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{a}]

[Prop 3.7o →^{tex} “ Prop\ 3.7o”]

[Prop 3.7o →^{pyk} “prop three seven o”]

Prop 3.7p

[Prop 3.7p →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬\underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{a}]

[Prop 3.7p →^{tex} “ Prop\ 3.7p”]

[Prop 3.7p →^{pyk} “prop three seven p”]

Prop 3.7q

[Prop 3.7q →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{a} ⇒ \underline{b} = \underline{a}]

[Prop 3.7q →^{tex} “ Prop\ 3.7q”]

[Prop 3.7q →^{pyk} “prop three seven q”]

Prop 3.7r

[Prop 3.7r →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a} + \underline{b} ⇒ \underline{a} = \underline{a} + \underline{b}]

[Prop 3.7r →^{tex} “ Prop\ 3.7r”]

[Prop 3.7r →^{pyk} “prop three seven r”]

Prop 3.7s

[Prop 3.7s →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a} + \underline{b}]

[Prop 3.7s →^{tex} “ Prop\ 3.7s”]

[Prop 3.7s →^{pyk} “prop three seven s”]

Prop 3.7t

[Prop 3.7t →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = 0 ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a} · \underline{b} ⇒ \underline{a} = \underline{a} · \underline{b}] [Prop 3.7t →^{tex} “ Prop\ 3.7t”]

[Prop 3.7t →^{pyk} “prop three seven t”]

Prop 3.7u

[Prop 3.7u →^{stmt} S ⊢ ∀\underline{a}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{a}]

[Prop 3.7u →^{tex} “ Prop\ 3.7u”]

[Prop 3.7u →^{pyk} “prop three seven u”]

Prop 3.7u′

[Prop 3.7u′ →^{stmt} S ⊢ ∀\underline{a}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{a} ⇒ ¬\underline{a} = 0]

[Prop 3.7u′ →^{tex} “ Prop\ 3.7u’”]

[Prop 3.7u′ →^{pyk} “prop three seven u mark”]

Prop 3.7v

[Prop 3.7v →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{a} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0 = \underline{a} · \underline{b}]

[Prop 3.7v →^{tex} “ Prop\ 3.7v”]

[Prop 3.7v →^{pyk} “prop three seven v”]

Prop 3.7w

[Prop 3.7w →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + 0′ = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} · \underline{a}]

[Prop 3.7w →^{tex} “ Prop\ 3.7w”]

[Prop 3.7w →^{pyk} “prop three seven w”]

Prop 3.7x

[Prop 3.7x →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} · \underline{a} = \underline{c} · \underline{a}]

[Prop 3.7x →^{tex} “ Prop\ 3.7x”]

[Prop 3.7x →^{pyk} “prop three seven x”]

Prop 3.7x′

[Prop 3.7x′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} · \underline{a} = \underline{c} · \underline{a} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c}]

[Prop 3.7x′ →^{tex} “ Prop\ 3.7x’”]

[Prop 3.7x′ →^{pyk} “prop three seven x mark”]

Prop 3.7y

[Prop 3.7y →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} = 0 ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c} ⇒ \underline{b} = \underline{c} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} · \underline{a} = \underline{c} · \underline{a} ⇒ \underline{b} · \underline{a} = \underline{c} · \underline{a}]

[Prop 3.7y →^{tex} “ Prop\ 3.7y”]

[Prop 3.7y →^{pyk} “prop three seven y”]

Prop 3.7y′

[Prop 3.7y′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} = 0 ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} · \underline{a} = \underline{c} · \underline{a} ⇒ \underline{b} · \underline{a} = \underline{c} · \underline{a} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{c} ⇒ \underline{b} = \underline{c}]

[Prop 3.7y′ →^{tex} “ Prop\ 3.7y’”]

[Prop 3.7y′ →^{pyk} “prop three seven y mark”]

Prop 3.7z

[Prop 3.7z →^{stmt} S ⊢ ∀\underline{a}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = 0]

[Prop 3.7z →^{tex} “ Prop\ 3.7z”]

[Prop 3.7z →^{pyk} “prop three seven z”]

Prop 3.7z′

[Prop 3.7z′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{b} = \underline{a} ⇒ \underline{b} = \underline{a} ⇒ \underline{a} = \underline{b}]

[Prop 3.7z′ →^{tex} “ Prop\ 3.7z’”]

[Prop 3.7z′ →^{pyk} “prop three seven z mark”]

Prop 3.10

[Prop 3.10 →^{tex} “

Prop\ 3.10”]

[Prop 3.10 →^{pyk} “prop three ten”]

Prop 3.10a

[Prop 3.10a →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{a} = ∀\underline{a}: \underline{a} · z]

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

[Prop 3.10a →^{pyk} “prop three ten a”]

Prop 3.10b

[Prop 3.10b →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{a} = ∀\underline{a}: 0′ · z]

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

[Prop 3.10b →^{pyk} “prop three ten b”]

Prop 3.10c

[Prop 3.10c →^{stmt} S ⊢ ¬∀_{obj}z: ¬0 = ∀\underline{a}: \underline{a} · z]

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

[Prop 3.10c →^{pyk} “prop three ten c”]

Prop 3.10d

[Prop 3.10d →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{c} = ¬∀_{obj}z: ¬\underline{c} ⇒ \underline{a} = ¬∀_{obj}z: ¬\underline{b} ∧ \underline{b} = ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · z · z · z]

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

[Prop 3.10d →^{pyk} “prop three ten d”]

Prop 3.10e

[Prop 3.10e →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{a} = \underline{a} ⇒ \underline{a} = \underline{a} = ∀\underline{a}: ∀\underline{b}: ¬¬\underline{a} = 0 ⇒ ¬\underline{b} · z]

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

[Prop 3.10e →^{pyk} “prop three ten e”]

Prop 3.10f

[Prop 3.10f →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{a} ⇒ \underline{a} = \underline{b} = ¬∀_{obj}z: ¬¬\underline{b} ⇒ ¬\underline{b} = ∀\underline{a}: ∀\underline{b}: \underline{a} · z · z]

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

[Prop 3.10f →^{pyk} “prop three ten f”]

Prop 3.10g

[Prop 3.10g →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{b} · \underline{c} = ¬∀_{obj}z: ¬\underline{b} ⇒ \underline{a} = ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · z · z] [Prop 3.10g →^{tex} “ Prop\ 3.10g”]

[Prop 3.10g →^{pyk} “prop three ten g”]

Prop 3.10h

[Prop 3.10h →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{b} + \underline{c} = ¬∀_{obj}z: ¬\underline{c} ⇒ \underline{a} = ¬∀_{obj}z: ¬\underline{b} ∧ \underline{a} = ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · z · z · z]

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

[Prop 3.10h →^{pyk} “prop three ten h”]

Prop 3.11

[Prop 3.11 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}\underline{c}: ∀_{obj}\underline{d}: ¬¬¬\underline{b} = \underline{a} · \underline{c} + \underline{d} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{d} = \underline{a} ⇒ ¬∀_{obj}\underline{e}: ∀_{obj}\underline{f}: ¬\underline{b} = \underline{a} · \underline{e} + \underline{f} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \underline{f} = \underline{a} ⇒ ¬\underline{c} = \underline{e} ⇒ ¬\underline{d} = \underline{f}]

[Prop 3.11 →^{tex} “

Prop\ 3.11”]

[Prop 3.11 →^{pyk} “prop three eleven”]

∗ < ∗

[x < y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x < y ¨= ∃z: (z ≠ 0 ∧ z + x = y)]⌉)]

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

< #2.”]

[∗ < ∗ →^{pyk} “" ist "”]

∗ ≤ ∗

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

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

\leq #2.”]

[∗ ≤ ∗ →^{pyk} “" istq "”]

∗ ≮ ∗

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

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

\not < #2.”]

[∗ ≮ ∗ →^{pyk} “" inst "”]

∗ > ∗

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

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

> #2.”]

[∗ > ∗ →^{pyk} “" igt "”]

∗ ≥ ∗

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

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

\geq #2.”]

[∗ ≥ ∗ →^{pyk} “" igtq "”]

∗ ≯ ∗

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

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

\not > #2.”]

[∗ ≯ ∗ →^{pyk} “" ingt "”]

∗ ≠ ∗

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

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

\neq #2.”]

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

∗ ∧ ∗

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

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

\wedge #2.”]

[∗ ∧ ∗ →^{pyk} “" and1 "”]

∗ ∨ ∗

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

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

\vee #2.”]

[∗ ∨ ∗ →^{pyk} “" or1 "”]

∃∗: ∗

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

[∃x: y →^{tex} “

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

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

∗ | ∗

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

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

\mathrel{|} #2.”]

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

∗ …

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

\ldots”]

[∗ … →^{pyk} “" ldots”] The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-06-28.UTC:01:17:25.716427 = MJD-53914.TAI:01:17:58.716427 = LGT-4658174278716427e-6