Logiweb codex of peano commutativity

Up Help

S′, A1′, A2′, A3′, A4′, A5′, S1′, S2′, S3′, S4′, S5′, S6′, S7′, S8′, S9′, MP′, Gen′, peano commutativity, M Lemma 1.8, M Proposition 3.2(a), M Proposition 3.2(b), M Proposition 3.2(c), M Proposition 3.2(d), M Proposition 3.2(f) (i), M Proposition 3.2(f) (ii), M Proposition 3.2(f), M Proposition 3.2(g) (i), M Proposition 3.2(g) (ii), M Proposition 3.2(g), M Proposition 3.2(h)(i), M Proposition 3.2(h)_{(g)(ii)}, M Proposition 3.2(h)(ii), M Proposition 3.2(h), M Tautology A, M Tautology B,

S′

[S′ →^{stmt} x]

A1′

[A1′ →^{proof} Rule tactic]

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

A2′

[A2′ →^{proof} Rule tactic]

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

A3′

[A3′ →^{proof} Rule tactic]

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

A4′

[A4′ →^{proof} Rule tactic]

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

A5′

[A5′ →^{proof} Rule tactic]

[A5′ →^{stmt} S′ ⊢ ∀\underline{x}: ∀\underline{a}: ∀\underline{b}: [ [ ṅonfree(⌈\underline{x}⌉, ⌈\underline{a}⌉) ] ⊢⊢ [ [ ˙∀\underline{x}: [ \underline{a} ˙⇒ \underline{b} ] ] ˙⇒ [ \underline{a} ˙⇒ ˙∀\underline{x}: \underline{b} ] ] ] ]

S1′

[S1′ →^{proof} Rule tactic]

[S1′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{a} =^{p} \underline{c} ] ˙⇒ [ \underline{b} =^{p} \underline{c} ] ] ] ]

S2′

[S2′ →^{proof} Rule tactic]

[S2′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ \underline{a}′ =^{p} [ \underline{b}′ ] ] ] ]

S3′

[S3′ →^{proof} Rule tactic]

[S3′ →^{stmt} S′ ⊢ ∀\underline{a}: ¬ [ ˙0 =^{p} [ \underline{a}′ ] ] ]

S4′

[S4′ →^{proof} Rule tactic]

[S4′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a}′ =^{p} [ \underline{b}′ ] ] ˙⇒ [ \underline{a} =^{p} \underline{b} ] ] ]

S5′

[S5′ →^{proof} Rule tactic]

[S5′ →^{stmt} S′ ⊢ ∀\underline{a}: [ [ \underline{a} ˙+ ˙0 ] =^{p} \underline{a} ] ]

S6′

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

S7′

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

S8′

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

S9′

[S9′ →^{proof} Rule tactic] [S9′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{x}: [ \underline{b}≡⟨\underline{a}|\underline{x} := ˙0⟩ ⊢⊢ [ \underline{c}≡⟨\underline{a}|\underline{x} := \underline{x}′⟩ ⊢⊢ [ \underline{b} ˙⇒ [ [ ˙∀\underline{x}: [ \underline{a} ˙⇒ \underline{c} ] ] ˙⇒ ˙∀\underline{x}: \underline{a} ] ] ] ] ]

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} ⊢ ˙∀\underline{x}: \underline{a} ] ]

peano commutativity

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

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

[S_{1}^{∀}(∗, ∗, ∗, ∗)], [S^{;}(∗, ∗)], [S_{1}^{;}(∗, ∗, ∗)], [S_{2}^{;}(∗, ∗, ∗, ∗)], [T (∗)], [claims(∗, ∗, ∗)], [claims_{2}(∗, ∗, ∗)], [<proof>], [proof], [[Lemma ∗: ∗]], [[Proof of ∗: ∗]], [[∗ lemma ∗: ∗]], [[∗ antilemma ∗: ∗]], [[∗ rule ∗: ∗]], [[∗ antirule ∗: ∗]], [verifier], [V_{1}(∗)], [V_{2}(∗, ∗)], [V_{3}(∗, ∗, ∗, ∗)], [V_{4}(∗, ∗)], [V_{5}(∗, ∗, ∗, ∗)], [V_{6}(∗, ∗, ∗, ∗)], [V_{7}(∗, ∗, ∗, ∗)], [Cut(∗, ∗)], [Head_{⊕}(∗)], [Tail_{⊕}(∗)], [rule_{1}(∗, ∗)], [rule(∗, ∗)], [Rule tactic], [Plus(∗, ∗)], [[Theory ∗]], [theory_{2}(∗, ∗)], [theory_{3}(∗, ∗)], [theory_{4}(∗, ∗, ∗)], [HeadNil′′], [HeadPair′′], [Transitivity′′], [Contra′′], [HeadNil], [HeadPair], [Transitivity], [Contra], [T_{E}], [ragged right], [ragged right expansion ], [parm(∗, ∗, ∗)], [parm^{∗}(∗, ∗, ∗)], [inst(∗, ∗)], [inst^{∗}(∗, ∗)], [occur(∗, ∗, ∗)], [occur^{∗}(∗, ∗, ∗)], [unify(∗ = ∗, ∗)], [unify^{∗}(∗ = ∗, ∗)], [unify_{2}(∗ = ∗, ∗)], [L_{a}], [L_{b}], [L_{c}], [L_{d}], [L_{e}], [L_{f}], [L_{g}], [L_{h}], [L_{i}], [L_{j}], [L_{k}], [L_{l}], [L_{m}], [L_{n}], [L_{o}], [L_{p}], [L_{q}], [L_{r}], [L_{s}], [L_{t}], [L_{u}], [L_{v}], [L_{w}], [L_{x}], [L_{y}], [L_{z}], [L_{A}], [L_{B}], [L_{C}], [L_{D}], [L_{E}], [L_{F}], [L_{G}], [L_{H}], [L_{I}], [L_{J}], [L_{K}], [L_{L}], [L_{M}], [L_{N}], [L_{O}], [L_{P}], [L_{Q}], [L_{R}], [L_{S}], [L_{T}], [L_{U}], [L_{V}], [L_{W}], [L_{X}], [L_{Y}], [L_{Z}], [L_{?}], [Reflexivity], [Reflexivity_{1}], [Commutativity], [Commutativity_{1}], [<tactic>], [tactic], [[∗ =^{tactic} ∗]], [P(∗, ∗, ∗)], [P^{∗}(∗, ∗, ∗)], [p_{0}], [conclude_{1}(∗, ∗)], [conclude_{2}(∗, ∗, ∗)], [conclude_{3}(∗, ∗, ∗, ∗)], [conclude_{4}(∗, ∗)], [peano], [˙0], [˙1], [˙2], [ȧ], [ḃ], [ċ], [ḋ], [ė], [ḟ], [ġ], [ḣ], [i̇], [j̇], [k̇], [l̇], [ṁ], [ṅ], [ȯ], [ṗ], [q̇], [ṙ], [ṡ], [ṫ], [u̇], [v̇], [ẇ], [ẋ], [ẏ], [ż], [ṅonfree(∗, ∗)], [ṅonfree^{∗}(∗, ∗)], [ḟree⟨∗|∗ := ∗⟩], [ḟree^{∗}⟨∗|∗ := ∗⟩], [∗≡⟨∗|∗ := ∗⟩], [∗≡⟨^{∗}∗|∗ := ∗⟩], [S], [A1], [A2], [A3], [A4], [A5], [S1], [S2], [S3], [S4], [S5], [S6], [S7], [S8], [S9], [MP], [Gen], [L3.2(a)], [S′], [A1′], [A2′], [A3′], [A4′], [A5′], [S1′], [S2′], [S3′], [S4′], [S5′], [S6′], [S7′], [S8′], [S9′], [MP′], [Gen′], [L3.2(a)′], [M1.7], [MP′_{h}], [Hypothesize], [Gen′_{h}], [M3.2(a)], [M3.2(a)_{h}], [M3.2(b)_{h}], [M3.1(S1′)_{h}], [M3.2(c)_{h}], [M3.1(S2′)_{h}], [M3.1(S5′)_{h}], [M3.1(S6′)_{h}], [M3.2(f)], [M Lemma 1.8], [M Proposition 3.2(a)], [M Proposition 3.2(b)], [M Proposition 3.2(c)], [M Proposition 3.2(d)], [M Proposition 3.2(f) (i)], [M Proposition 3.2(f) (ii)], [M Proposition 3.2(f)], [M Proposition 3.2(g) (i)], [M Proposition 3.2(g) (ii)], [M Proposition 3.2(g)], [M Proposition 3.2(h)(i)], [M Proposition 3.2(h)_{(g)(ii)}], [M Proposition 3.2(h)(ii)], [M Proposition 3.2(h)], [M Tautology A], [M Tautology B]; Preassociative [∗ {∗}], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]], [˙∗]; Preassociative [“ ∗ ”], [], [(∗)^{t}], [string(∗) + ∗], [string(∗) ++ ∗], [ ∗], [ ∗], [!∗], [”∗], [#∗], [$∗], [%∗], [&∗], [’∗], [(∗], [)∗], [∗∗], [+∗], [, ∗], [-∗], [.∗], [/∗], [0∗], [1∗], [2∗], [3∗], [4∗], [5∗], [6∗], [7∗], [8∗], [9∗], [:∗], [; ∗], [<∗], [=∗], [>∗], [?∗], [@∗], [A∗], [B∗], [C∗], [D∗], [E∗], [F∗], [G∗], [H∗], [I∗], [J∗], [K∗], [L∗], [M∗], [N∗], [O∗], [P∗], [Q∗], [R∗], [S∗], [T∗], [U∗], [V∗], [W∗], [X∗], [Y∗], [Z∗], [[∗], [\∗], []∗], [ˆ ∗], [ ∗], [‘∗], [a∗], [b∗], [c∗], [d∗], [e∗], [f∗], [g∗], [h∗], [i∗], [j∗], [k∗], [l∗], [m∗], [n∗], [o∗], [p∗], [q∗], [r∗], [s∗], [t∗], [u∗], [v∗], [w∗], [x∗], [y∗], [z∗], [{∗], [|∗], [}∗], [˜ ∗], [Preassociative ∗; ∗], [Postassociative ∗; ∗], [[∗], ∗], [priority ∗ end], [newline ∗], [macro newline ∗]; Preassociative [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗^{H}], [∗^{T}], [∗^{U}], [∗^{h}], [∗^{t}], [∗^{s}], [∗^{c}], [∗^{d}], [∗^{a}], [∗^{C}], [∗^{M}], [∗^{B}], [∗^{r}], [∗^{i}], [∗^{d}], [∗^{R}], [∗^{0}], [∗^{1}], [∗^{2}], [∗^{3}], [∗^{4}], [∗^{5}], [∗^{6}], [∗^{7}], [∗^{8}], [∗^{9}], [∗^{E}], [∗^{V}], [∗^{C}], [∗^{C^{∗}}], [∗′]; Preassociative [∗ · ∗], [∗ ·_{0} ∗], [∗ ˙· ∗]; Preassociative [∗ + ∗], [∗ +_{0} ∗], [∗ +_{1} ∗], [∗ − ∗], [∗ −_{0} ∗], [∗ −_{1} ∗], [∗ ˙+ ∗]; Preassociative [∗ ∪ {∗}], [∗ ∪ ∗], [∗\{∗}]; Postassociative [∗ ˙. . ∗], [∗ \underline{˙. .} ∗], [∗ \underline{: :} ∗], [∗ \underline{+2∗} ∗], [∗ : : ∗], [∗ +2∗ ∗]; Postassociative [∗, ∗]; Preassociative

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

[∗ ∈_{t} ∗], [∗ ⊆_{T} ∗], [∗ =^{T} ∗], [∗ =^{s} ∗], [∗ free in ∗], [∗ free in^{∗} ∗], [∗ free for ∗ in ∗],

[∗ free for^{∗} ∗ in ∗], [∗ ∈_{c} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗], [∗ =^{p} ∗], [∗^{P}];

Preassociative [¬∗], [ ˙¬ ∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗], [∗ ˙∧ ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗], [∗ ˙∨ ∗]; Preassociative [ ˙∀∗: ∗], [ ˙∃∗: ∗]; Postassociative [∗ ¨⇒ ∗], [∗ ˙⇒ ∗], [∗ ˙⇔ ∗]; Postassociative [∗ : ∗], [∗!∗]; Preassociative

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

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

[peano commutativity →^{pyk} “peano commutativity”]

M Lemma 1.8

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

[M Lemma 1.8 →^{stmt} S′ ⊢ ∀\underline{b}: [ \underline{b} ˙⇒ \underline{b} ] ]

[M Lemma 1.8 →^{tex} “M\ Lemma\ 1.8”]

[M Lemma 1.8 →^{pyk} “mendelson lemma one eight”]

M Proposition 3.2(a)

[M Proposition 3.2(a) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: [ [ S5′ ≫ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ] ; [ [ S1′ ≫ [ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ˙⇒ [ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ˙⇒ [ \underline{t} =^{p} \underline{t} ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ˙⇒ [ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ˙⇒ [ \underline{t} =^{p} \underline{t} ] ] ] ] ⊳ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ] ≫ [ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ˙⇒ [ \underline{t} =^{p} \underline{t} ] ] ] ; [ [ [ MP′ ⊳ [ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ˙⇒ [ \underline{t} =^{p} \underline{t} ] ] ] ⊳ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ] ≫ [ \underline{t} =^{p} \underline{t} ] ] ] ] ] ⌉, p_{0}, c)]

[M Proposition 3.2(a) →^{stmt} S′ ⊢ ∀\underline{t}: [ \underline{t} =^{p} \underline{t} ] ]

[M Proposition 3.2(a) →^{tex} “M\ Proposition\ 3.2(a)”]

[M Proposition 3.2(a) →^{pyk} “mendelson proposition three two a”]

M Proposition 3.2(b)

[M Proposition 3.2(b) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: ∀\underline{r}: [ [ S1′ ≫ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ [ \underline{t} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ] ; [ [ [ M Tautology A ⊳ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ [ \underline{t} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ] ≫ [ [ \underline{t} =^{p} \underline{t} ] ˙⇒ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ] ; [ [ M Proposition 3.2(a) ≫ [ \underline{t} =^{p} \underline{t} ] ] ; [ [ [ MP′ ⊳ [ [ \underline{t} =^{p} \underline{t} ] ˙⇒ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ] ⊳ [ \underline{t} =^{p} \underline{t} ] ] ≫ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ] ] ] ⌉, p_{0}, c)]

[M Proposition 3.2(b) →^{stmt} S′ ⊢ ∀\underline{t}: ∀\underline{r}: [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ]

[M Proposition 3.2(b) →^{tex} “M\ Proposition\ 3.2(b)”]

[M Proposition 3.2(b) →^{pyk} “mendelson proposition three two b”]

M Proposition 3.2(c)

[M Proposition 3.2(c) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: [ [ S1′ ≫ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ; [ [ M Proposition 3.2(b) ≫ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ; [ [ [ M Tautology B ⊳ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ⊳ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ≫ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ] ] ⌉, p_{0}, c)]

[M Proposition 3.2(c) →^{stmt} S′ ⊢ ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ]

[M Proposition 3.2(c) →^{tex} “M\ Proposition\ 3.2(c)”]

[M Proposition 3.2(c) →^{pyk} “mendelson proposition three two c”]

M Proposition 3.2(d)

[M Proposition 3.2(d) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{r}: ∀\underline{t}: ∀\underline{s}: [ [ M Proposition 3.2(c) ≫ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{t} =^{p} \underline{s} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ; [ [ [ M Tautology A ⊳ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{t} =^{p} \underline{s} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ≫ [ [ \underline{t} =^{p} \underline{s} ] ˙⇒ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ; [ [ M Proposition 3.2(b) ≫ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ; [ [ [ [ M Tautology B ⊳ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ⊳ [ [ \underline{t} =^{p} \underline{s} ] ˙⇒ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ≫ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ; [ [ M Tautology A ⊳ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ≫ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[M Proposition 3.2(d) →^{stmt} S′ ⊢ ∀\underline{r}: ∀\underline{t}: ∀\underline{s}: [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ]

[M Proposition 3.2(d) →^{tex} “M\ Proposition\ 3.2(d)”]

[M Proposition 3.2(d) →^{pyk} “mendelson proposition three two d”]

M Proposition 3.2(f) (i)

[M Proposition 3.2(f) (i) →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S5′ ≫ [ [ ˙0 ˙+ ˙0 ] =^{p} ˙0 ] ] ; [ [ M Proposition 3.2(b) ≫ [ [ [ ˙0 ˙+ ˙0 ] =^{p} ˙0 ] ˙⇒ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ] ] ; [ [ [

MP′ ⊳ [ [ [ ˙0 ˙+ ˙0 ] =^{p} ˙0 ] ˙⇒ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ] ] ⊳ [ [ ˙0 ˙+ ˙0 ] =^{p} ˙0 ] ] ≫ [

˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ] ] ] ⌉, p_{0}, c)]

[M Proposition 3.2(f) (i) →^{stmt} S′ ⊢ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ]

[M Proposition 3.2(f) (i) →^{tex} “M\ Proposition\ 3.2(f)\ (i)”] [M Proposition 3.2(f) (i) →^{pyk} “mendelson proposition three two f i”]

M Proposition 3.2(f) (ii)

[M Proposition 3.2(f) (ii) →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S6′ ≫ [ [ ˙0 ˙+ [ ẋ′ ] ] =^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ] ; [ [ S2′ ≫ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ] ] ; [ [ M Proposition 3.2(d) ≫ [ [ ẋ′ =^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ [

˙0 ˙+ [ ẋ′ ] ] =^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ] ; [ [ [ [

M Tautology B ⊳ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ] ] ⊳

[ [ ẋ′ =^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ [ ˙0 ˙+ [ ẋ′ ] ] =^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [

ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ] ≫ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ [ [ ˙0 ˙+ [ ẋ′ ] ] =^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ] ; [ [ [ M Tautology A ⊳ [

[ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ [ [ ˙0 ˙+ [ ẋ′ ] ] =^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ ẋ′ =^{p} [

˙0 ˙+ [ ẋ′ ] ] ] ] ] ] ≫ [ [ [ ˙0 ˙+ [ ẋ′ ] ] =^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẋ =^{p} [

˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ ˙0 ˙+ [ ẋ′ ] ]

=^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ]

] ⊳ [ [ ˙0 ˙+ [ ẋ′ ] ] =^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ] ≫ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [

ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ; [ [ Gen′ ⊳ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ≫ ˙∀ẋ: [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[M Proposition 3.2(f) (ii) →^{stmt} S′ ⊢ ˙∀ẋ: [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ]

[M Proposition 3.2(f) (ii) →^{tex} “M\ Proposition\ 3.2(f)\ (ii)”]

[M Proposition 3.2(f) (ii) →^{pyk} “mendelson proposition three two f ii”]

M Proposition 3.2(f)

[M Proposition 3.2(f) →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S9′ ≫ [ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ˙⇒ [ [ ˙∀ẋ: [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ˙⇒ ˙∀ẋ: [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ] ] ; [ [ M Proposition 3.2(f) (i) ≫ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ˙⇒ [ [ ˙∀ẋ: [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [

ẋ′ ] ] ] ] ] ˙⇒ ˙∀ẋ: [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ] ] ⊳ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ] ≫ [ [ ˙∀ẋ:

[ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ˙⇒ ˙∀ẋ: [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ] ; [ [ M Proposition 3.2(f) (ii) ≫ ˙∀ẋ: [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ; [ [ [ MP′ ⊳ [ [ ˙∀ẋ: [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ˙⇒ ˙∀ẋ: [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ] ⊳ ˙∀ẋ: [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ≫ ˙∀ẋ: [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ] ] ] ] ⌉, p_{0}, c)] [M Proposition 3.2(f) →^{stmt} S′ ⊢ ˙∀ẋ: [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ]

[M Proposition 3.2(f) →^{tex} “M\ Proposition\ 3.2(f)”]

[M Proposition 3.2(f) →^{pyk} “mendelson proposition three two f”]

M Proposition 3.2(g) (i)

[M Proposition 3.2(g) (i) →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S5′ ≫ [ [ ẋ′ ˙+ ˙0 ] =^{p} [ ẋ′ ] ] ] ; [ [ S5′ ≫ [ [ ẋ ˙+ ˙0 ] =^{p} [ ẋ ] ] ] ; [ [ S2′ ≫ [ [ [ ẋ ˙+ ˙0 ] =^{p} [ ẋ ] ] ˙⇒ [ [ ẋ ˙+ ˙0 ] ′ =^{p} [ ẋ′ ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ ẋ ˙+ ˙0 ] =^{p} [ ẋ ] ] ˙⇒ [ [ ẋ ˙+ ˙0 ] ′ =^{p} [ ẋ′ ] ] ] ] ⊳ [ [ ẋ ˙+ ˙0 ] =^{p} [ ẋ ] ] ] ≫ [ [ ẋ ˙+ ˙0 ] ′ =^{p} [ ẋ′ ] ] ] ; [ [ M Proposition 3.2(d) ≫ [ [ [ ẋ′ ˙+ ˙0 ] =^{p} [ ẋ′ ] ] ˙⇒ [ [ [ ẋ ˙+ ˙0 ] ′ =^{p} [ ẋ′ ] ] ˙⇒ [ [ ẋ′ ˙+ ˙0 ] =^{p} [ [ ẋ ˙+ ˙0 ] ′ ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ ẋ′ ˙+ ˙0 ] =^{p} [ ẋ′ ]

] ˙⇒ [ [ [ ẋ ˙+ ˙0 ] ′ =^{p} [ ẋ′ ] ] ˙⇒ [ [ ẋ′ ˙+ ˙0 ] =^{p} [ [ ẋ ˙+ ˙0 ] ′ ] ] ] ] ] ⊳ [ [

ẋ′ ˙+ ˙0 ] =^{p} [ ẋ′ ] ] ] ≫ [ [ [ ẋ ˙+ ˙0 ] ′ =^{p} [ ẋ′ ] ] ˙⇒ [ [ ẋ′ ˙+ ˙0 ] =^{p} [ [ ẋ ˙+ ˙0 ] ′ ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ ẋ ˙+ ˙0 ] ′ =^{p} [ ẋ′ ] ] ˙⇒ [ [ ẋ′ ˙+ ˙0 ] =^{p} [ [ ẋ ˙+ ˙0 ] ′

] ] ] ] ⊳ [ [ ẋ ˙+ ˙0 ] ′ =^{p} [ ẋ′ ] ] ] ≫ [ [ ẋ′ ˙+ ˙0 ] =^{p} [ [ ẋ ˙+ ˙0 ] ′ ] ] ] ; [ [

Gen′ ⊳ [ [ ẋ′ ˙+ ˙0 ] =^{p} [ [ ẋ ˙+ ˙0 ] ′ ] ] ] ≫ ˙∀ẋ: [ [ ẋ′ ˙+ ˙0 ] =^{p} [ [ ẋ ˙+ ˙0 ] ′ ] ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[M Proposition 3.2(g) (i) →^{stmt} S′ ⊢ ˙∀ẋ: [ [ ẋ′ ˙+ ˙0 ] =^{p} [ [ ẋ ˙+ ˙0 ] ′ ] ] ]

[M Proposition 3.2(g) (i) →^{tex} “M\ Proposition\ 3.2(g)\ (i)”]

[M Proposition 3.2(g) (i) →^{pyk} “mendelson proposition three two g i”]

M Proposition 3.2(g) (ii)

[M Proposition 3.2(g) (ii) →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S6′ ≫ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ′ ˙+ [ ẏ ] ] ′ ] ] ] ; [ [ S2′ ≫ [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ] ] ; [ [ M Proposition 3.2(c) ≫ [ [ [

ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ′ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ [ ẋ′ ˙+ [ ẏ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ]

] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ] ] ] ; [ [ [ M Tautology A ⊳ [

[ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ′ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ [ ẋ′ ˙+ [ ẏ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ]

′′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ] ] ] ≫ [ [ [ ẋ′ ˙+ [ ẏ ] ]

′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ˙⇒ [ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ′ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [

ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ] ] ] ; [ [ [ [ M Tautology B ⊳ [ [ [

ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ]

] ] ⊳ [ [ [ ẋ′ ˙+ [ ẏ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ˙⇒ [ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [

ẋ′ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ] ] ] ≫ [ [ [

ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ′ ˙+ [ ẏ ] ] ′ ]

] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ] ] ] ; [ [ [ M Tautology A ⊳ [

[ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ′ ˙+ [ ẏ ] ]

′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ] ] ] ≫ [ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p}

[ [ ẋ′ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [

ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [

ẋ′ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ]

] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ] ] ] ⊳ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ′ ˙+ [ ẏ ] ] ′ ] ] ] ≫

[ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ]

′′ ] ] ] ] ; [ [ S6′ ≫ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ; [ [ S2′ ≫ [ [

[ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ]

] ] ; [ [ M Proposition 3.2(d) ≫ [ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ˙⇒

[ [ [ ẋ ˙+ [ ẏ′ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ′ ]

] ′ ] ] ] ] ] ; [ [ [ [ M Tautology B ⊳ [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ] ] ⊳ [ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [

ẋ ˙+ [ ẏ ] ] ′′ ] ] ˙⇒ [ [ [ ẋ ˙+ [ ẏ′ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ]

] =^{p} [ [ ẋ ˙+ [ ẏ′ ] ] ′ ] ] ] ] ] ≫ [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒

[ [ [ ẋ ˙+ [ ẏ′ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ′ ]

] ′ ] ] ] ] ] ; [ [ [ M Tautology A ⊳ [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ]

˙⇒ [ [ [ ẋ ˙+ [ ẏ′ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [

ẏ′ ] ] ′ ] ] ] ] ] ≫ [ [ [ ẋ ˙+ [ ẏ′ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ˙⇒ [ [ [ ẋ′ ˙+ [

ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ′ ] ] ′ ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ] ] ⊳ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ≫ [ [ ẋ ˙+ [ ẏ′ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ ẋ ˙+ [ ẏ′ ] ] ′ =^{p} [ [ ẋ ˙+

[ ẏ ] ] ′′ ] ] ˙⇒ [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p}

[ [ ẋ ˙+ [ ẏ′ ] ] ′ ] ] ] ] ] ⊳ [ [ ẋ ˙+ [ ẏ′ ] ] ′ =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′′ ] ] ] ≫ [ [

[ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ′ ] ] ′ ] ]

] ] ; [ [ Gen′ ⊳ [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ′ ] ] ′ ] ] ] ] ≫ ˙∀ẏ: [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [

ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ′ ] ] ′ ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[M Proposition 3.2(g) (ii) →^{stmt} S′ ⊢ ˙∀ẏ: [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ]

˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ′ ] ] ′ ] ] ] ]

[M Proposition 3.2(g) (ii) →^{tex} “M\ Proposition\ 3.2(g)\ (ii)”]

[M Proposition 3.2(g) (ii) →^{pyk} “mendelson proposition three two g ii”]

M Proposition 3.2(g)

[M Proposition 3.2(g) →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S9′ ≫ [ [ ˙∀ẋ: [ [ ẋ′ ˙+ ˙0 ] =^{p} [ [ ẋ ˙+ ˙0 ] ′ ] ] ] ˙⇒ [ [ ˙∀ẏ: [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ′ ] ] ′ ] ] ] ] ˙⇒ ˙∀ẏ: [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ] ] ; [ [ M Proposition 3.2(g) (i) ≫ ˙∀ẋ: [ [ ẋ′ ˙+ ˙0 ] =^{p} [ [ ẋ ˙+ ˙0 ] ′ ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ˙∀ẋ: [ [ ẋ′ ˙+ ˙0 ] =^{p} [ [ ẋ ˙+ ˙0 ] ′ ] ] ] ˙⇒ [ [ ˙∀ẏ: [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ′ ] ] ′ ] ] ] ] ˙⇒ ˙∀ẏ: [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ] ] ⊳ ˙∀ẋ: [ [ ẋ′ ˙+ ˙0 ] =^{p} [ [ ẋ ˙+ ˙0 ] ′ ] ] ] ≫ [ [ ˙∀ẏ: [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ′ ] ] ′ ] ] ] ] ˙⇒ ˙∀ẏ: [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ] ; [ [ M Proposition 3.2(g) (ii) ≫ ˙∀ẏ: [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ′ ] ] ′ ] ] ] ] ; [ [ [ MP′ ⊳ [ [ ˙∀ẏ: [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ′ ] ] ′ ] ] ] ] ˙⇒ ˙∀ẏ: [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ] ⊳ ˙∀ẏ: [ [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ′ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ′ ] ] ′ ] ] ] ] ≫ ˙∀ẏ: [ [ ẋ′ ˙+ [ ẏ ]

] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[M Proposition 3.2(g) →^{stmt} S′ ⊢ ˙∀ẏ: [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ]

[M Proposition 3.2(g) →^{tex} “M\ Proposition\ 3.2(g)”]

[M Proposition 3.2(g) →^{pyk} “mendelson proposition three two g”]

M Proposition 3.2(h)(i)

[M Proposition 3.2(h)(i) →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S5′ ≫ [ [ ẋ ˙+ ˙0 ] =^{p} [ ẋ ] ] ] ; [ [ M Proposition 3.2(f) ≫ ˙∀ẋ: [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ; [ [ [ A4′ @ [ ẋ ] ] ≫ [ [ ˙∀ẋ: [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ˙⇒ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ˙∀ẋ: [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ˙⇒ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ] ⊳ ˙∀ẋ: [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ≫ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ; [ [ M Proposition 3.2(c) ≫ [ [ [ ẋ ˙+ ˙0 ] =^{p}

[ ẋ ] ] ˙⇒ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ] ] ; [ [ [

[ MP′ ⊳ [ [ [ ẋ ˙+ ˙0 ] =^{p} [ ẋ ] ] ˙⇒ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ ˙0 ] =^{p} [

˙0 ˙+ [ ẋ ] ] ] ] ] ] ⊳ [ [ ẋ ˙+ ˙0 ] =^{p} [ ẋ ] ] ] ≫ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [

[ ẋ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ] ⊳ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ≫ [ [ ẋ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ; [ [ Gen′ ⊳ [ [ ẋ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ≫ ˙∀ẋ: [ [ ẋ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[M Proposition 3.2(h)(i) →^{stmt} S′ ⊢ ˙∀ẋ: [ [ ẋ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ]

[M Proposition 3.2(h)(i) →^{tex} “M\ Proposition\ 3.2(h)(i)”] [M Proposition 3.2(h)(i) →^{pyk} “mendelson proposition three two h i”]

M Proposition 3.2(h)_{(g)(ii)}

[M Proposition 3.2(h)_{(g)(ii)} →^{proof} λc.λx.P(⌈S′ ⊢ [ [ ˙∀ẏ: [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ⊢ [ [ [ A4′ @ [ ż ] ] ≫ [ [ ˙∀ẏ: [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ˙⇒ [ [ ẋ′ ˙+ [ ż ] ] =^{p} [ [ ẋ ˙+ [ ż ] ] ′ ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ˙∀ẏ: [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ˙⇒ [ [ ẋ′ ˙+ [ ż ] ] =^{p} [ [ ẋ ˙+ [ ż ] ] ′ ] ] ] ] ⊳ ˙∀ẏ: [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ≫ [ [ ẋ′ ˙+ [ ż ] ] =^{p} [ [ ẋ ˙+ [ ż ] ] ′ ] ] ] ; [ [ [ Gen′ ⊳ [ [ ẋ′ ˙+ [ ż ] ] =^{p} [ [ ẋ ˙+ [ ż ] ] ′ ] ] ] ≫ ˙∀ẋ: [ [ ẋ′ ˙+ [ ż ] ] =^{p} [ [ ẋ ˙+ [ ż ] ] ′ ] ] ] ; [ [ [ A4′ @ [ ẏ ] ] ≫ [ [ ˙∀ẋ:

[ [ ẋ′ ˙+ [ ż ] ] =^{p} [ [ ẋ ˙+ [ ż ] ] ′ ] ] ] ˙⇒ [ [ ẏ′ ˙+ [ ż ] ] =^{p} [ [ ẏ ˙+ [ ż ] ] ′

] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ˙∀ẋ: [ [ ẋ′ ˙+ [ ż ] ] =^{p} [ [ ẋ ˙+ [ ż ] ] ′ ] ] ] ˙⇒ [ [ ẏ′ ˙+ [ ż ] ] =^{p} [ [ ẏ ˙+ [ ż ] ] ′ ] ] ] ] ⊳ ˙∀ẋ: [ [ ẋ′ ˙+ [ ż ] ] =^{p} [ [ ẋ ˙+ [ ż ] ] ′ ] ] ] ≫ [ [ ẏ′ ˙+ [ ż ] ] =^{p} [ [ ẏ ˙+ [ ż ] ] ′ ] ] ] ; [ [ [ Gen′ ⊳ [ [ ẏ′ ˙+ [ ż ] ] =^{p} [ [ ẏ ˙+ [ ż ] ] ′ ] ] ] ≫ ˙∀ż: [ [ ẏ′ ˙+ [ ż ] ] =^{p} [ [ ẏ ˙+ [ ż ] ] ′ ] ] ] ; [ [ [ A4′ @ [ ẋ ] ] ≫ [ [ ˙∀ż: [ [ ẏ′ ˙+ [ ż ] ] =^{p} [ [ ẏ ˙+ [ ż ] ] ′ ] ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ; [ [ [ MP′ ⊳ [ [ ˙∀ż: [ [ ẏ′ ˙+ [ ż ] ] =^{p} [ [ ẏ ˙+ [ ż ] ] ′ ] ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ⊳ ˙∀ż: [ [ ẏ′ ˙+ [ ż ] ] =^{p} [ [ ẏ ˙+ [ ż ] ] ′ ] ] ] ≫ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[M Proposition 3.2(h)_{(g)(ii)} →^{stmt} S′ ⊢ [ [ ˙∀ẏ: [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′

] ] ] ⊢ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ]

[M Proposition 3.2(h)_{(g)(ii)} →^{tex} “M\ Proposition\ 3.2(h) {(g)(ii)}”]

[M Proposition 3.2(h)_{(g)(ii)} →^{pyk} “mendelson proposition three two h g ii”]

M Proposition 3.2(h)(ii)

[M Proposition 3.2(h)(ii) →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S6′ ≫ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ; [ [ M Proposition 3.2(g) ≫ ˙∀ẏ: [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ; [ [ [ M Proposition 3.2(h)_{(g)(ii)} ⊳ ˙∀ẏ: [ [ ẋ′ ˙+ [ ẏ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ≫ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ; [ [ S2′ ≫ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ ] ] ′ =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ; [ [ M Proposition 3.2(c) ≫ [ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ [ ẋ ˙+

[ ẏ ] ] ′ =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ]

; [ [ [ M Tautology A ⊳ [ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ [ ẋ ˙+

[ ẏ ] ] ′ =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ]

≫ [ [ [ ẋ ˙+ [ ẏ ] ] ′ =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ

] ] ′ ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ] ; [ [ [ [

M Tautology B ⊳ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ ] ] ′ =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ⊳ [ [ [ ẋ ˙+ [ ẏ ] ] ′ =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ [ ẋ ˙+ [

ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ]

≫ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ] ; [ [ [ M Tautology A ⊳ [ [

[ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [

[ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ] ≫ [ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ]

] ′ ] ] ˙⇒ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ

] ] ′ ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ˙⇒ [ [

[ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ]

⊳ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ≫ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ; [ [ M Proposition 3.2(d) ≫ [

[ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′

] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ] ; [ [ [ [ M Tautology B ⊳ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ⊳

[ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ]

′ ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ] ≫ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+

[ ẋ ] ] ] ˙⇒ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [

ẏ′ ˙+ [ ẋ ] ] ] ] ] ] ; [ [ [ M Tautology A ⊳ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ]

] ˙⇒ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ]

] ] ] ] ] ≫ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [

[ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒

[ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ] ⊳ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ≫ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ; [ [ Gen′ ⊳ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ≫ ˙∀ẏ: [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ]

=^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[M Proposition 3.2(h)(ii) →^{stmt} S′ ⊢ ˙∀ẏ: [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [

[ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ]

[M Proposition 3.2(h)(ii) →^{tex} “M\ Proposition\ 3.2(h)(ii)”]

[M Proposition 3.2(h)(ii) →^{pyk} “mendelson proposition three two h ii”]

M Proposition 3.2(h)

[M Proposition 3.2(h) →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S9′ ≫ [ [ ˙∀ẋ: [ [ ẋ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ˙⇒ [ [ ˙∀ẏ: [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ˙⇒ ˙∀ẏ: [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ] ] ] ; [ [ M Proposition 3.2(h)(i) ≫ ˙∀ẋ: [ [ ẋ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ˙∀ẋ: [ [ ẋ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ˙⇒ [ [ ˙∀ẏ: [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ˙⇒ ˙∀ẏ: [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ] ] ] ⊳ ˙∀ẋ: [ [ ẋ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ≫ [ [ ˙∀ẏ: [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ˙⇒ ˙∀ẏ: [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ] ] ; [ [ M Proposition 3.2(h)(ii) ≫ ˙∀ẏ: [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ˙∀ẏ: [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ˙⇒ ˙∀ẏ: [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ] ] ⊳ ˙∀ẏ: [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ≫ ˙∀ẏ: [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ] ; [ [ Gen′ ⊳ ˙∀ẏ: [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ] ≫ ˙∀ẋ: ˙∀ẏ: [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[M Proposition 3.2(h) →^{stmt} S′ ⊢ ˙∀ẋ: ˙∀ẏ: [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ]

[M Proposition 3.2(h) →^{tex} “M\ Proposition\ 3.2(h)”]

[M Proposition 3.2(h) →^{pyk} “mendelson proposition three two h”]

M Tautology A

[M Tautology A →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ⊢ [ [ 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{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ˙⇒ [ \underline{b} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ˙⇒ [ \underline{b} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ⊳ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ≫ [ \underline{b} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ; [ [ A2′ ≫ [ [ \underline{b} ˙⇒ [ [

\underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ˙⇒ [ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ˙⇒ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ]

; [ [ [ [ MP′ ⊳ [ [ \underline{b} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ˙⇒ [ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ˙⇒ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ⊳ [ \underline{b} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ≫ [ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ˙⇒ [ \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{c} ] ] ] ] ⊳ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ] ≫ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[M Tautology A →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ⊢ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] [M Tautology A →^{tex} “M\ Tautology\ A”]

[M Tautology A →^{pyk} “mendelson tautology a”]

M Tautology B

[M Tautology B →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{d}: ∀\underline{e}: ∀\underline{f}: [ [ \underline{d} ˙⇒ \underline{e} ] ⊢ [ [ \underline{e} ˙⇒ \underline{f} ] ⊢ [ [ A1′ ≫ [ [ \underline{e} ˙⇒ \underline{f} ] ˙⇒ [ \underline{d} ˙⇒ [ \underline{e} ˙⇒ \underline{f} ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ \underline{e} ˙⇒ \underline{f} ] ˙⇒ [ \underline{d} ˙⇒ [ \underline{e} ˙⇒ \underline{f} ] ] ] ] ⊳ [ \underline{e} ˙⇒ \underline{f} ] ] ≫ [ \underline{d} ˙⇒ [ \underline{e} ˙⇒ \underline{f} ] ] ] ; [ [ A2′ ≫ [ [ \underline{d} ˙⇒ [ \underline{e} ˙⇒ \underline{f} ] ] ˙⇒ [ [ \underline{d} ˙⇒ \underline{e} ] ˙⇒ [ \underline{d} ˙⇒ \underline{f} ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ \underline{d} ˙⇒ [ \underline{e} ˙⇒ \underline{f} ] ] ˙⇒ [ [ \underline{d} ˙⇒ \underline{e} ] ˙⇒ [ \underline{d} ˙⇒ \underline{f} ] ] ] ] ⊳ [ \underline{d} ˙⇒ [ \underline{e} ˙⇒ \underline{f} ] ] ] ≫ [ [ \underline{d} ˙⇒ \underline{e} ] ˙⇒ [ \underline{d} ˙⇒ \underline{f} ] ] ] ; [ [ [ MP′ ⊳ [ [ \underline{d} ˙⇒ \underline{e} ] ˙⇒ [ \underline{d} ˙⇒ \underline{f} ] ] ] ⊳ [ \underline{d} ˙⇒ \underline{e} ] ] ≫ [ \underline{d} ˙⇒ \underline{f} ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[M Tautology B →^{stmt} S′ ⊢ ∀\underline{d}: ∀\underline{e}: ∀\underline{f}: [ [ \underline{d} ˙⇒ \underline{e} ] ⊢ [ [ \underline{e} ˙⇒ \underline{f} ] ⊢ [ \underline{d} ˙⇒ \underline{f} ] ] ] ]

[M Tautology B →^{tex} “M\ Tautology\ B”]

[M Tautology B →^{pyk} “mendelson tautology b”]

The pyk compiler, version 0.grue.20050603 by Klaus Grue GRD-2005-07-03.UTC:14:50:38.354331 = MJD-53554.TAI:14:51:10.354331 = LGT-4627119070354331e-6