Logiweb codex of logic

Up Help

logic, MP′_{d}, A1′_{i}, Hypothesize, A2′_{i}, A2′_{ii}, MP′_{h}, A2′_{iid}, MP′_{hd}, Mendelson 1.8, Mendelson 1.8_{i}, Repetition, Mendelson 1.47 b, Mendelson 1.47 c, Mendelson 1.47 e, Mendelson 1.11 d, A1′_{ih}, A2′_{ih}, A2′_{iih}, Mendelson 1.47 b_{h}, Mendelson 1.47 c_{h}, Mendelson 1.11 c, Mendelson 1.48 d, Mendelson 1.48 e, Mendelson 1.48 h, Mendelson 1.10 a, Mendelson 1.10 b, S1′_{i}, S1′_{ii}, S2′_{i}, S2′_{ih}, S9′_{ii}, Induction, Mendelson 3.2 a, Mendelson 3.2 b, Mendelson 3.2 b_{i}, Mendelson 3.2 c, Mendelson 3.2 c_{ii}, Mendelson 3.2 c_{iih}, Mendelson 3.2 d, Mendelson 3.2 d_{ii}, Mendelson 3.2 d_{iih}, Mendelson 3.2 f, Mendelson 3.2 f i, Mendelson 3.2 f ii, Mendelson 3.2 g, Mendelson 3.2 g i, Mendelson 3.2 g ii, Mendelson 3.2 h, Mendelson 3.2 h i, Mendelson 3.2 h ii, hyp, instance, conclusion, ∗ ⊵ ∗, ∗ ⊵ ∗ ⊵ ∗, ∗ ⊵_{h} ∗, ∗ ⊵_{h} ∗ ⊵_{h} ∗, Line ∗ : • ∗ ⊵∗ ≫ ∗; ∗, Line ∗ : • ∗ ∘ ⊵ ∗ ≫ ∗; ∗, Line ∗ : • ∗ ⊵ ∗ ∘ ≫ ∗; ∗, Line ∗ : • ∗ ⊵ ∗ ⊵∗ ≫ ∗; ∗, Line ∗ : • Hypothesis ≫ ∗; ∗, Line ∗ : • ∗ ≫ ∗; ∗, Line ∗ : • ∗ ≫ ∗; ∗,

logic

[logic →^{prio} Preassociative [logic], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [math ∗ end math], [flush left [∗]], [x], [y], [z], [[∗ ▷◁ ∗]], [[∗ →^{∗} ∗]], [pyk], [tex], [name], [prio], [∗], [T], [if(∗, ∗, ∗)], [[∗ ⇒^{∗} ∗]], [val], [claim], [⊥], [f(∗)], [(∗)^{I}], [F], [\underline{0}], [\underline{1}], [\underline{2}], [\underline{3}], [\underline{4}], [\underline{5}], [\underline{6}], [\underline{7}], [\underline{8}], [\underline{9}], [0], [1], [2], [3], [4], [5], [6], [7], [8], [9], [a], [b], [c], [d], [e], [f], [g], [h], [i], [j], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [(∗)^{M}], [If(∗, ∗, ∗)], [array{∗} ∗ end array], [l], [c], [r], [empty], [⟨∗ | ∗:= ∗⟩], [M(∗)], [Ũ(∗)], [U(∗)], [U^{M}(∗)], [apply(∗, ∗)], [apply_{1}(∗, ∗)], [identifier(∗)], [identifier_{1}(∗, ∗)], [arrayplus(∗, ∗)], [array-remove(∗, ∗, ∗)], [array-put(∗, ∗, ∗, ∗)], [array-add(∗, ∗, ∗, ∗, ∗)], [bit(∗, ∗)], [bit_{1}(∗, ∗)], [rack], ["vector"], ["bibliography"], ["dictionary"], ["body"], ["codex"], ["expansion"], ["code"], ["cache"], ["diagnose"], ["pyk"], ["tex"], ["texname"], ["value"], ["message"], ["macro"], ["definition"], ["unpack"], ["claim"], ["priority"], ["lambda"], ["apply"], ["true"], ["if"], ["quote"], ["proclaim"], ["define"], ["introduce"], ["hide"], ["pre"], ["post"], [E(∗, ∗, ∗)], [E_{2}(∗, ∗, ∗, ∗, ∗)], [E_{3}(∗, ∗, ∗, ∗)], [E_{4}(∗, ∗, ∗, ∗)], [lookup(∗, ∗, ∗)], [abstract(∗, ∗, ∗, ∗)], [⌈∗⌉], [M(∗, ∗, ∗)], [M_{2}(∗, ∗, ∗, ∗)], [M^{∗}(∗, ∗, ∗)], [macro], [s_{0}], [zip(∗, ∗)], [assoc_{1}(∗, ∗, ∗)], [(∗)^{p}], [self], [[∗ ¨= ∗]], [[∗ ˙= ∗]], [[∗ ´= ∗]], [[∗ =^{pyk} ∗]], [[∗ =^{tex} ∗]], [[∗ =^{name} ∗]], [Priority table[∗]], [M̃_{1}], [M̃_{2}(∗)], [M̃_{3}(∗)], [M̃_{4}(∗, ∗, ∗, ∗)], [M̃(∗, ∗, ∗)], [Q̃(∗, ∗, ∗)], [Q̃_{2}(∗, ∗, ∗)], [Q̃_{3}(∗, ∗, ∗, ∗)], [Q̃^{∗}(∗, ∗, ∗)], [(∗)], [aspect(∗, ∗)], [aspect(∗, ∗, ∗)], [⟨∗⟩], [tuple_{1}(∗)], [tuple_{2}(∗)], [let_{2}(∗, ∗)], [let_{1}(∗, ∗)], [[∗ =^{claim} ∗]], [checker], [check(∗, ∗)], [check_{2}(∗, ∗, ∗)], [check_{3}(∗, ∗, ∗)], [check^{∗}(∗, ∗)], [check_{2}^{∗}(∗, ∗, ∗)], [[∗]^{·}], [[∗]^{−}], [[∗]^{∘}], [msg], [[∗ =^{msg} ∗]], [<stmt>], [stmt], [[∗ =^{stmt} ∗]], [HeadNil′], [HeadPair′], [Transitivity′], [⊥ ⊥], [Contra′], [T′_{E}], [L_{1}], [\underline{∗}], [A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N], [O], [P], [Q], [R], [S], [T ], [U], [V], [W], [X], [Y], [Z], [⟨∗ | ∗:= ∗⟩], [⟨^{∗}∗ | ∗:= ∗⟩], [∅], [Remainder], [(∗)^{v}], [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], [S′], [A1′], [A2′], [A3′], [A4′], [A5′], [S1′], [S2′], [S3′], [S4′], [S5′], [S6′], [S7′], [S8′], [S9′], [MP′], [Gen′], [MP′_{d}], [A1′_{i}], [Hypothesize], [A2′_{i}], [A2′_{ii}], [MP′_{h}], [A2′_{iid}], [MP′_{hd}], [Mendelson 1.8], [Mendelson 1.8_{i}], [Repetition], [Mendelson 1.47 b], [Mendelson 1.47 c], [Mendelson 1.47 e], [Mendelson 1.11 d], [A1′_{ih}], [A2′_{ih}], [A2′_{iih}], [Mendelson 1.47 b_{h}], [Mendelson 1.47 c_{h}], [Mendelson 1.11 c], [Mendelson 1.48 d], [Mendelson 1.48 e], [Mendelson 1.48 h], [Mendelson 1.10 a], [Mendelson 1.10 b], [S1′_{i}], [S1′_{ii}], [S2′_{i}], [S2′_{ih}], [S9′_{ii}], [Induction], [Mendelson 3.2 a], [Mendelson 3.2 b], [Mendelson 3.2 b_{i}], [Mendelson 3.2 c], [Mendelson 3.2 c_{ii}], [Mendelson 3.2 c_{iih}], [Mendelson 3.2 d], [Mendelson 3.2 d_{ii}], [Mendelson 3.2 d_{iih}], [Mendelson 3.2 f], [Mendelson 3.2 f i], [Mendelson 3.2 f ii], [Mendelson 3.2 g], [Mendelson 3.2 g i], [Mendelson 3.2 g ii], [Mendelson 3.2 h], [Mendelson 3.2 h i], [Mendelson 3.2 h ii], [hyp], [instance], [conclusion]; 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 [∗ @ ∗], [∗ ⊳ ∗], [∗ ⊳ ⊳ ∗], [∗ ≫ ∗], [∗ ⊵ ∗], [∗ ⊵ ∗ ⊵ ∗], [∗ ⊵_{h} ∗], [∗ ⊵_{h} ∗ ⊵_{h} ∗]; Postassociative [∗ ⊢ ∗], [∗ ⊢⊢ ∗], [∗ i.e. ∗]; Preassociative [∀∗: ∗]; Postassociative [∗ ⊕ ∗]; Postassociative [∗; ∗]; Preassociative [∗ proves ∗]; Preassociative [∗ proof of ∗ : ∗], [Line ∗ : ∗ ≫ ∗; ∗], [Last line ∗ ≫ ∗ □], [Line ∗ : Premise ≫ ∗; ∗], [Line ∗ : Side-condition ≫ ∗; ∗], [Arbitrary ≫ ∗; ∗], [Local ≫ ∗ = ∗; ∗], [Line ∗ : • ∗ ⊵∗ ≫ ∗; ∗], [Line ∗ : • ∗ ∘ ⊵ ∗ ≫ ∗; ∗], [Line ∗ : • ∗ ⊵ ∗ ∘ ≫ ∗; ∗], [Line ∗ : • ∗ ⊵ ∗ ⊵∗ ≫ ∗; ∗], [Line ∗ : • Hypothesis ≫ ∗; ∗], [Line ∗ : • ∗ ≫ ∗; ∗], [Line ∗ : • ∗ ≫ ∗; ∗]; Postassociative [∗ then ∗], [∗[ ∗]∗]; Preassociative [∗&∗]; Preassociative [∗\\∗]; ]

[logic →^{pyk} “logic”]

MP′_{d}

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

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

[MP′_{d} →^{tex} “MP’ {d}”]

[MP′_{d} →^{pyk} “double rule prime mp”]

A1′_{i}

[A1′_{i} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\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} ] ] ] ] ⌉, p_{0}, c)]

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

[A1′_{i} →^{tex} “A1’ {i}”]

[A1′_{i} →^{pyk} “inference axiom prime a one”]

Hypothesize

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

[Hypothesize →^{tex} “Hypothesize”]

[Hypothesize →^{pyk} “rule hypothesize”]

A2′_{i}

[A2′_{i} →^{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} ] ] ] ] ] ⌉, p_{0}, c)]

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

[A2′_{i} →^{tex} “A2’ {i}”]

[A2′_{i} →^{pyk} “inference axiom prime a two”]

A2′_{ii}

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

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

[A2′_{ii} →^{tex} “A2’ {ii}”]

[A2′_{ii} →^{pyk} “inference inference axiom prime a two”]

MP′_{h}

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

[MP′_{h} →^{tex} “MP’ {h}”]

[MP′_{h} →^{pyk} “hypothetical rule prime mp”]

A2′_{iid}

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

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

[A2′_{iid} →^{tex} “A2’ {iid}”]

[A2′_{iid} →^{pyk} “double inference inference axiom prime a two”]

MP′_{hd}

[MP′_{hd} →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[MP′_{hd} ¨= A2′_{iid}]⌉)]

[MP′_{hd} →^{tex} “MP’ {hd}”]

[MP′_{hd} →^{pyk} “double hypothetical rule prime mp”]

Mendelson 1.8

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

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

[Mendelson 1.8 →^{tex} “Mendelson\ \textbf{1.8}”]

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

Mendelson 1.8_{i}

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

[Mendelson 1.8_{i} →^{stmt} S′ ⊢ ∀\underline{a}: [ \underline{a} ⊢ \underline{a} ] ]

[Mendelson 1.8_{i} →^{tex} “Mendelson\ \textbf{1.8} {i}”]

[Mendelson 1.8_{i} →^{pyk} “inference mendelson lemma one eight”]

Repetition

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

[Repetition →^{tex} “Repetition”]

[Repetition →^{pyk} “rule repetition”]

Mendelson 1.47 b

[Mendelson 1.47 b →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} ˙⇒ \underline{b} ] ⊢ [ [ \underline{b} ˙⇒ \underline{c} ] ⊢ [ [ [ A1′_{i} ⊳ [ \underline{b} ˙⇒ \underline{c} ] ] ≫ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ; [ [ [ A2′_{ii} ⊳ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ⊳ [ \underline{a} ˙⇒ \underline{b} ] ] ≫ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ⌉, p_{0}, c)]

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

[Mendelson 1.47 b →^{tex} “Mendelson\ \textbf{1.47}\ b”]

[Mendelson 1.47 b →^{pyk} “mendelson exercise one fourtyseven b”]

Mendelson 1.47 c

[Mendelson 1.47 c →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ⊢ [ [ [ A2′_{i} ⊳ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ≫ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ; [ [ [ A1′_{i} ⊳ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ≫ [ \underline{b} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ; [ [ A1′ ≫ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ] ; [ [ [ A2′_{ii} ⊳ [ \underline{b} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ⊳ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ] ≫ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[Mendelson 1.47 c →^{tex} “Mendelson\ \textbf{1.47}\ c”]

[Mendelson 1.47 c →^{pyk} “mendelson exercise one fourtyseven c”]

Mendelson 1.47 e

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

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

[Mendelson 1.47 e →^{tex} “Mendelson\ \textbf{1.47}\ e”]

[Mendelson 1.47 e →^{pyk} “mendelson exercise one fourtyseven e”]

Mendelson 1.11 d

[Mendelson 1.11 d →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: [ [ Mendelson 1.8 ≫ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ] ] ; [ [ A3′ ≫ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ [ [ ˙¬ \underline{a} ] ˙⇒ \underline{b} ] ˙⇒ \underline{a} ] ] ] ; [ [ [ A1′_{i} ⊳ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ [ [ ˙¬ \underline{a} ] ˙⇒ \underline{b} ] ˙⇒ \underline{a} ] ] ] ≫ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ [ [ ˙¬ \underline{a} ] ˙⇒ \underline{b} ] ˙⇒ \underline{a} ] ] ] ] ; [ [ A1′ ≫ [ \underline{b} ˙⇒ [ [ ˙¬ \underline{a} ] ˙⇒ \underline{b} ] ] ] ; [ [ [ A1′_{i} ⊳ [ \underline{b} ˙⇒ [ [ ˙¬ \underline{a} ] ˙⇒ \underline{b} ] ] ] ≫ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ \underline{b} ˙⇒ [ [ ˙¬ \underline{a} ] ˙⇒ \underline{b} ] ] ] ] ; [ [ [ [ A2′_{ii} ⊳ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ [ [ ˙¬ \underline{a} ] ˙⇒ \underline{b} ] ˙⇒ \underline{a} ] ] ] ] ⊳ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ] ] ≫ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ [ [ ˙¬ \underline{a} ] ˙⇒ \underline{b} ] ˙⇒ \underline{a} ] ] ] ; [ [ [ [ Mendelson 1.47 b_{h} ⊳ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ \underline{b} ˙⇒ [ [ ˙¬ \underline{a} ] ˙⇒ \underline{b} ] ] ] ] ⊳ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ [ [ ˙¬ \underline{a} ] ˙⇒ \underline{b} ] ˙⇒ \underline{a} ] ] ] ≫ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ \underline{b} ˙⇒ \underline{a} ] ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ \underline{b} ˙⇒ \underline{a} ] ] ] ≫ [ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{b} ] ˙⇒ [ \underline{b} ˙⇒ \underline{a} ] ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[Mendelson 1.11 d →^{tex} “Mendelson\ \textbf{1.11}\ d”]

[Mendelson 1.11 d →^{pyk} “mendelson lemma one eleven d”]

A1′_{ih}

[A1′_{ih} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: [ [ \underline{h} ˙⇒ \underline{a} ] ⊢ [ [ Mendelson 1.8 ≫ [ \underline{h} ˙⇒ \underline{h} ] ] ; [ [ A1′ ≫ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{a} ] ] ] ; [ [ [ A1′_{i} ⊳ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{a} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{a} ] ] ] ] ; [ [ [ [ A2′_{ii} ⊳ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{a} ] ] ] ] ⊳ [ \underline{h} ˙⇒ \underline{a} ] ] ≫ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ \underline{a} ] ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ \underline{a} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ \underline{a} ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[A1′_{ih} →^{tex} “A1’ {ih}”] [A1′_{ih} →^{pyk} “hypothetical inference axiom prime a one”]

A2′_{ih}

[A2′_{ih} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ⊢ [ [ Mendelson 1.8 ≫ [ \underline{h} ˙⇒ \underline{h} ] ] ; [ [ A2′ ≫ [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ; [ [ [ A1′_{i} ⊳ [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ≫ [ \underline{h} ˙⇒ [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ; [ [ [ [ A2′_{ii} ⊳ [ \underline{h} ˙⇒ [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ] ≫ [ \underline{h} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ \underline{h} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ≫ [ \underline{h} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[A2′_{ih} →^{tex} “A2’ {ih}”]

[A2′_{ih} →^{pyk} “hypothetical inference axiom prime a two”]

A2′_{iih}

[A2′_{iih} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ⊢ [ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ⊢ [ [ Mendelson 1.8 ≫ [ \underline{h} ˙⇒ \underline{h} ] ] ; [ [ A2′ ≫ [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ; [ [ [ A1′_{i} ⊳ [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ≫ [ \underline{h} ˙⇒ [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ; [ [ [ [ [ A2′_{iid} ⊳ [ \underline{h} ˙⇒ [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[A2′_{iih} →^{tex} “A2’ {iih}”]

[A2′_{iih} →^{pyk} “hypothetical inference inference axiom prime a two”]

Mendelson 1.47 b_{h}

[Mendelson 1.47 b_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ⊢ [ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ⊢ [ [ Mendelson 1.8 ≫ [ \underline{h} ˙⇒ \underline{h} ] ] ; [ [ [ A1′_{ih} ⊳ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ] ; [ [ [ [ A2′_{iih} ⊳ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 1.47 b_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ⊢ [ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ⊢ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ]

[Mendelson 1.47 b_{h} →^{tex} “Mendelson\ \textbf{1.47}\ b {h}”]

[Mendelson 1.47 b_{h} →^{pyk} “hypothetical mendelson exercise one fourtyseven b”]

Mendelson 1.47 c_{h}

[Mendelson 1.47 c_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ⊢ [ [ Mendelson 1.8 ≫ [ \underline{h} ˙⇒ \underline{h} ] ] ; [ [ [ A2′_{ih} ⊳ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ] ≫ [ \underline{h} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ; [ [ [ A1′_{ih} ⊳ [ \underline{h} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ; [ [ A1′ ≫ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ] ; [ [ [ A1′_{i} ⊳ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ] ] ; [ [ [ [ A2′_{iih} ⊳ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 1.47 c_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{h} ˙⇒ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ⊢ [ \underline{h} ˙⇒ [ \underline{b} ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ]

[Mendelson 1.47 c_{h} →^{tex} “Mendelson\ \textbf{1.47}\ c {h}”]

[Mendelson 1.47 c_{h} →^{pyk} “hypothetical mendelson exercise one fourtyseven c”]

Mendelson 1.11 c

[Mendelson 1.11 c →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: [ [ Mendelson 1.8 ≫ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{a} ] ] ; [ [ Mendelson 1.8 ≫ [ \underline{a} ˙⇒ \underline{a} ] ] ; [ [ [ A1′_{i} ⊳ [ \underline{a} ˙⇒ \underline{a} ] ] ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ \underline{a} ] ] ] ; [ [ A1′ ≫ [ \underline{a} ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ] ] ; [ [ [ A1′_{i} ⊳ [ \underline{a} ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ] ] ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ] ] ] ; [ [ [ A1′_{ih} ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ] ] ] ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ [ \underline{a} ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ] ] ] ] ; [ [ A1′ ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ] ] ; [ [ [ A1′_{i} ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ] ] ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ [ ˙¬ \underline{a} ] ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ] ] ] ; [ [ [ A1′_{ih} ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ [ [ ˙¬ \underline{a} ] ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ] ] ] ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ [ [ ˙¬ \underline{a} ] ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ] ] ] ] ; [ [ [ [ A2′_{iih} ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ [ \underline{a} ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ] ] ] ] ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ \underline{a} ] ] ] ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ] ] ] ; [ [ [ [ A2′_{ii} ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ [ [ ˙¬ \underline{a} ] ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ] ] ] ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ ˙¬ \underline{a} ] ] ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ] ] ; [ [ [ A1′_{ih} ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ] ] ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ] ] ] ; [ [ A3′ ≫ [ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ˙⇒ \underline{b} ] ] ] ; [ [ [ A1′_{i} ⊳ [ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ˙⇒ \underline{b} ] ] ] ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ˙⇒ \underline{b} ] ] ] ] ; [ [ [ A1′_{ih} ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ˙⇒ \underline{b} ] ] ] ] ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ˙⇒ \underline{b} ] ] ] ] ] ; [ [ [ [ A2′_{iih} ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ˙⇒ \underline{b} ] ] ] ] ] ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ] ] ] ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ˙⇒ \underline{b} ] ] ] ] ; [ [ [ [ A2′_{iih} ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ˙⇒ \underline{b} ] ] ] ] ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ] ] ] ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ] ≫ [ [ ˙¬ \underline{a} ] ˙⇒ [ \underline{a} ˙⇒ \underline{b} ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[Mendelson 1.11 c →^{tex} “Mendelson\ \textbf{1.11}\ c”]

[Mendelson 1.11 c →^{pyk} “mendelson lemma one eleven c”]

Mendelson 1.48 d

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

[Mendelson 1.48 d →^{tex} “Mendelson\ \textbf{1.48}\ d”]

[Mendelson 1.48 d →^{pyk} “mendelson exercise one fourtyeight d”]

Mendelson 1.48 e

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

[Mendelson 1.48 e →^{tex} “Mendelson\ \textbf{1.48}\ e”]

[Mendelson 1.48 e →^{pyk} “mendelson exercise one fourtyeight e”]

Mendelson 1.48 h

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

[Mendelson 1.48 h →^{tex} “Mendelson\ \textbf{1.48}\ h”]

[Mendelson 1.48 h →^{pyk} “mendelson exercise one fourtyeight h”]

Mendelson 1.10 a

[Mendelson 1.10 a →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} ˙⇒ \underline{b} ] ⊢ [ [ \underline{b} ˙⇒ \underline{c} ] ⊢ [ [ Mendelson 1.8 ≫ [ \underline{a} ˙⇒ \underline{a} ] ] ; [ [ [ [ Mendelson 1.47 b ⊳ [ \underline{a} ˙⇒ \underline{a} ] ] ⊳ [ \underline{a} ˙⇒ \underline{b} ] ] ≫ [ \underline{a} ˙⇒ \underline{b} ] ] ; [ [ [ [ Mendelson 1.47 b ⊳ [ \underline{a} ˙⇒ \underline{b} ] ] ⊳ [ \underline{b} ˙⇒ \underline{c} ] ] ≫ [ \underline{a} ˙⇒ \underline{c} ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ \underline{a} ˙⇒ \underline{c} ] ] ≫ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[Mendelson 1.10 a →^{tex} “Mendelson\ \textbf{1.10}\ a”]

[Mendelson 1.10 a →^{pyk} “mendelson corollary one ten a”]

Mendelson 1.10 b

[Mendelson 1.10 b →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ⊢ [ \underline{b} ⊢ [ [ Mendelson 1.8 ≫ [ \underline{a} ˙⇒ \underline{a} ] ] ; [ [ [ [ Mendelson 1.47 b ⊳ [ \underline{a} ˙⇒ \underline{a} ] ] ⊳ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ≫ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ; [ [ [ [ Mendelson 1.47 e ⊳ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ] ⊳ \underline{b} ] ≫ [ \underline{a} ˙⇒ \underline{c} ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ \underline{a} ˙⇒ \underline{c} ] ] ≫ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[Mendelson 1.10 b →^{tex} “Mendelson\ \textbf{1.10}\ b”]

[Mendelson 1.10 b →^{pyk} “mendelson corollary one ten b”]

S1′_{i}

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

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

[S1′_{i} →^{tex} “S1’ {i}”]

[S1′_{i} →^{pyk} “inference axiom prime s one”]

S1′_{ii}

[S1′_{ii} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} =^{p} \underline{b} ] ⊢ [ [ \underline{a} =^{p} \underline{c} ] ⊢ [ [ [ S1′_{i} ⊳ [ \underline{a} =^{p} \underline{b} ] ] ≫ [ [ \underline{a} =^{p} \underline{c} ] ˙⇒ [ \underline{b} =^{p} \underline{c} ] ] ] ; [ [ [ MP′ ⊳ [ [ \underline{a} =^{p} \underline{c} ] ˙⇒ [ \underline{b} =^{p} \underline{c} ] ] ] ⊳ [ \underline{a} =^{p} \underline{c} ] ] ≫ [ \underline{b} =^{p} \underline{c} ] ] ] ] ] ⌉, p_{0}, c)]

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

[S1′_{ii} →^{tex} “S1’ {ii}”]

[S1′_{ii} →^{pyk} “inference inference axiom prime s one”]

S2′_{i}

[S2′_{i} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} =^{p} \underline{b} ] ⊢ [ [ S2′ ≫ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ \underline{a}′ =^{p} [ \underline{b}′ ] ] ] ] ; [ [ [ MP′ ⊳ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ \underline{a}′ =^{p} [ \underline{b}′ ] ] ] ] ⊳ [ \underline{a} =^{p} \underline{b} ] ] ≫ [

\underline{a}′ =^{p} [ \underline{b}′ ] ] ] ] ] ⌉, p_{0}, c)]

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

[S2′_{i} →^{tex} “S2’ {i}”]

[S2′_{i} →^{pyk} “inference axiom prime s two”]

S2′_{ih}

[S2′_{ih} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: [ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{b} ] ] ⊢ [ [ Mendelson 1.8 ≫ [ \underline{h} ˙⇒ \underline{h} ] ] ; [ [ S2′ ≫ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ \underline{a}′ =^{p} [ \underline{b}′ ] ] ] ] ; [ [ [ A1′_{i} ⊳ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ \underline{a}′ =^{p} [ \underline{b}′ ] ] ] ] ≫ [ \underline{h} ˙⇒ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ \underline{a}′ =^{p} [ \underline{b}′ ] ] ] ] ] ; [ [ [ [ A2′_{ii} ⊳ [ \underline{h} ˙⇒ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ \underline{a}′ =^{p} [ \underline{b}′ ] ] ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{b} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{a}′ =^{p} [ \underline{b}′ ] ] ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ \underline{h} ˙⇒ [ \underline{a}′ =^{p} [ \underline{b}′ ] ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{a}′ =^{p} [ \underline{b}′ ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[S2′_{ih} →^{tex} “S2’ {ih}”]

[S2′_{ih} →^{pyk} “hypothetical inference axiom prime s two”]

S9′_{ii}

[S9′_{ii} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{y}: [ \underline{b}≡⟨\underline{a}|\underline{y} := ˙0⟩ ⊢⊢ [ \underline{c}≡⟨\underline{a}|\underline{y} := \underline{y}′⟩ ⊢⊢ [ \underline{b} ⊢ [ [ ˙∀\underline{y}: [ \underline{a} ˙⇒ \underline{c} ] ] ⊢ [ [ [ [ S9′ ⊳ ⊳ \underline{b}≡⟨\underline{a}|\underline{y} := ˙0⟩ ] ⊳ ⊳ \underline{c}≡⟨\underline{a}|\underline{y} := \underline{y}′⟩ ] ≫ [ \underline{b} ˙⇒ [ [ ˙∀\underline{y}: [ \underline{a} ˙⇒ \underline{c} ] ] ˙⇒ ˙∀\underline{y}: \underline{a} ] ] ] ; [ [ [ [ MP′_{d} ⊳ [ \underline{b} ˙⇒ [ [ ˙∀\underline{y}: [ \underline{a} ˙⇒ \underline{c} ] ] ˙⇒ ˙∀\underline{y}: \underline{a} ] ] ] ⊳ \underline{b} ] ⊳ ˙∀\underline{y}: [ \underline{a} ˙⇒ \underline{c} ] ] ≫ ˙∀\underline{y}: \underline{a} ] ] ] ] ] ] ⌉, p_{0}, c)]

[S9′_{ii} →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{y}: [ \underline{b}≡⟨\underline{a}|\underline{y} := ˙0⟩ ⊢⊢ [ \underline{c}≡⟨\underline{a}|\underline{y} := \underline{y}′⟩ ⊢⊢ [ \underline{b} ⊢ [ [ ˙∀\underline{y}: [ \underline{a} ˙⇒ \underline{c} ] ] ⊢ ˙∀\underline{y}: \underline{a} ] ] ] ] ]

[S9′_{ii} →^{tex} “S9’ {ii}”]

[S9′_{ii} →^{pyk} “inference inference axiom prime s nine”]

Induction

[Induction →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{y}: [ \underline{b}≡⟨\underline{a}|\underline{y} := ˙0⟩ ⊢⊢ [ \underline{c}≡⟨\underline{a}|\underline{y} := \underline{y}′⟩ ⊢⊢ [ ⌈\underline{a}⌉≡⟨⌈\underline{a}⌉|⌈\underline{y}⌉ := ⌈\underline{y}⌉⟩ ⊢⊢ [ \underline{b} ⊢ [ [ \underline{a} ˙⇒ \underline{c} ] ⊢ [ [ [ Gen′ ⊳ [ \underline{a} ˙⇒ \underline{c} ] ] ≫ ˙∀\underline{y}: [ \underline{a} ˙⇒ \underline{c} ] ] ; [ [ [ [ [ [ S9′_{ii} ⊳ ⊳ \underline{b}≡⟨\underline{a}|\underline{y} := ˙0⟩ ] ⊳ ⊳ \underline{c}≡⟨\underline{a}|\underline{y} := \underline{y}′⟩ ] ⊳ \underline{b} ] ⊳ ˙∀\underline{y}: [ \underline{a} ˙⇒ \underline{c} ] ] ≫ ˙∀\underline{y}: \underline{a} ] ; [ [ [ A4′ ⊳ ⊳ ⌈\underline{a}⌉≡⟨⌈\underline{a}⌉|⌈\underline{y}⌉ := ⌈\underline{y}⌉⟩ ] ≫ [ [ ˙∀\underline{y}: \underline{a} ] ˙⇒ \underline{a} ] ] ; [ [ [ MP′ ⊳ [ [ ˙∀\underline{y}: \underline{a} ] ˙⇒ \underline{a} ] ] ⊳ ˙∀\underline{y}: \underline{a} ] ≫ \underline{a} ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[Induction →^{tex} “Induction”]

[Induction →^{pyk} “rule induction”]

Mendelson 3.2 a

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

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

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

[Mendelson 3.2 a →^{pyk} “mendelson proposition three two a”]

Mendelson 3.2 b

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

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

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

[Mendelson 3.2 b →^{pyk} “mendelson proposition three two b”]

Mendelson 3.2 b_{i}

[Mendelson 3.2 b_{i} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} =^{p} \underline{b} ] ⊢ [ [ Mendelson 3.2 b ≫ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ \underline{b} =^{p} \underline{a} ] ] ] ; [ [ [ MP′ ⊳ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ \underline{b} =^{p} \underline{a} ] ] ] ⊳ [ \underline{a} =^{p} \underline{b} ] ] ≫ [ \underline{b} =^{p} \underline{a} ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 3.2 b_{i} →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} =^{p} \underline{b} ] ⊢ [ \underline{b} =^{p} \underline{a} ] ] ]

[Mendelson 3.2 b_{i} →^{tex} “Mendelson\ \textbf{3.2}\ b {i}”]

[Mendelson 3.2 b_{i} →^{pyk} “inference mendelson proposition three two b”]

Mendelson 3.2 c

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

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

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

[Mendelson 3.2 c →^{pyk} “mendelson proposition three two c”]

Mendelson 3.2 c_{ii}

[Mendelson 3.2 c_{ii} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} =^{p} \underline{b} ] ⊢ [ [ \underline{b} =^{p} \underline{c} ] ⊢ [ [ Mendelson 3.2 c ≫ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{b} =^{p} \underline{c} ] ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ; [ [ [ [ MP′_{d} ⊳ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{b} =^{p} \underline{c} ] ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ⊳ [ \underline{a} =^{p} \underline{b} ] ] ⊳ [ \underline{b} =^{p} \underline{c} ]

] ≫ [ \underline{a} =^{p} \underline{c} ] ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 3.2 c_{ii} →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} =^{p} \underline{b} ] ⊢ [ [ \underline{b} =^{p} \underline{c} ] ⊢ [ \underline{a} =^{p} \underline{c} ] ] ] ]

[Mendelson 3.2 c_{ii} →^{tex} “Mendelson\ \textbf{3.2}\ c {ii}”]

[Mendelson 3.2 c_{ii} →^{pyk} “inference inference mendelson proposition three two c”]

Mendelson 3.2 c_{iih}

[Mendelson 3.2 c_{iih} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{b} ] ] ⊢ [ [ \underline{h} ˙⇒ [ \underline{b} =^{p} \underline{c} ] ] ⊢ [ [ Mendelson 1.8 ≫ [ \underline{h} ˙⇒ \underline{h} ] ] ; [ [ Mendelson 3.2 c ≫ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{b} =^{p} \underline{c} ] ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ; [ [ [ A1′_{i} ⊳ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{b} =^{p} \underline{c} ] ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ≫ [ \underline{h} ˙⇒ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{b} =^{p} \underline{c} ] ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ] ; [ [ [ [ [ A2′_{iid} ⊳ [ \underline{h} ˙⇒ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{b} =^{p} \underline{c} ] ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{b} ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{b} =^{p} \underline{c} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 3.2 c_{iih} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{b} ] ] ⊢ [ [ \underline{h} ˙⇒ [

\underline{b} =^{p} \underline{c} ] ] ⊢ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ]

[Mendelson 3.2 c_{iih} →^{tex} “Mendelson\ \textbf{3.2}\ c {iih}”]

[Mendelson 3.2 c_{iih} →^{pyk} “hypothetical inference inference mendelson proposition three two c”]

Mendelson 3.2 d

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

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

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

[Mendelson 3.2 d →^{pyk} “mendelson proposition three two d”]

Mendelson 3.2 d_{ii}

[Mendelson 3.2 d_{ii} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} =^{p} \underline{b} ] ⊢ [ [ \underline{c} =^{p} \underline{b} ] ⊢ [ [ Mendelson 3.2 d ≫ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{c} =^{p} \underline{b} ] ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ; [ [ [ [ MP′_{d} ⊳ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{c} =^{p} \underline{b} ] ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ⊳ [ \underline{a} =^{p} \underline{b} ] ] ⊳ [ \underline{c} =^{p} \underline{b} ]

] ≫ [ \underline{a} =^{p} \underline{c} ] ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 3.2 d_{ii} →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} =^{p} \underline{b} ] ⊢ [ [ \underline{c} =^{p} \underline{b} ] ⊢ [ \underline{a} =^{p} \underline{c} ] ] ] ]

[Mendelson 3.2 d_{ii} →^{tex} “Mendelson\ \textbf{3.2}\ d {ii}”]

[Mendelson 3.2 d_{ii} →^{pyk} “inference inference mendelson proposition three two d”]

Mendelson 3.2 d_{iih}

[Mendelson 3.2 d_{iih} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{b} ] ] ⊢ [ [ \underline{h} ˙⇒ [ \underline{c} =^{p} \underline{b} ] ] ⊢ [ [ Mendelson 1.8 ≫ [ \underline{h} ˙⇒ \underline{h} ] ] ; [ [ Mendelson 3.2 d ≫ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{c} =^{p} \underline{b} ] ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ; [ [ [ A1′_{i} ⊳ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{c} =^{p} \underline{b} ] ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ≫ [ \underline{h} ˙⇒ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{c} =^{p} \underline{b} ] ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ] ; [ [ [ [ [ A2′_{iid} ⊳ [ \underline{h} ˙⇒ [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{c} =^{p} \underline{b} ] ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{b} ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{c} =^{p} \underline{b} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 3.2 d_{iih} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{b} ] ] ⊢ [ [ \underline{h} ˙⇒ [

\underline{c} =^{p} \underline{b} ] ] ⊢ [ \underline{h} ˙⇒ [ \underline{a} =^{p} \underline{c} ] ] ] ] ]

[Mendelson 3.2 d_{iih} →^{tex} “Mendelson\ \textbf{3.2}\ d {iih}”]

[Mendelson 3.2 d_{iih} →^{pyk} “hypothetical inference inference mendelson proposition three two d”]

Mendelson 3.2 f

[Mendelson 3.2 f →^{proof} λc.λx.P(⌈S′ ⊢ [ [ Mendelson 3.2 f i ≫ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ] ; [ [ Mendelson 3.2 f ii ≫ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ; [ [ [ Induction ⊳ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ] ⊳ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p}

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

[Mendelson 3.2 f →^{stmt} S′ ⊢ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ]

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

[Mendelson 3.2 f →^{pyk} “mendelson proposition three two f”]

Mendelson 3.2 f i

[Mendelson 3.2 f i →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S5′ ≫ [ [ ˙0 ˙+ ˙0 ] =^{p} ˙0 ] ] ; [ [ Mendelson 3.2 b_{i} ⊳ [ [ ˙0 ˙+ ˙0 ] =^{p} ˙0 ] ] ≫ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 3.2 f i →^{stmt} S′ ⊢ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ]

[Mendelson 3.2 f i →^{tex} “Mendelson\ \textbf{3.2}\ f\ i”]

[Mendelson 3.2 f i →^{pyk} “mendelson proposition three two f i”]

Mendelson 3.2 f ii

[Mendelson 3.2 f ii →^{proof} λc.λx.P(⌈S′ ⊢ [ [ Mendelson 1.8 ≫ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ

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

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

[ ẋ ] ] ] ˙⇒ [ [ ˙0 ˙+ [ ẋ′ ] ] =^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ] ] ; [ [ [ S2′_{ih} ⊳ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ] ≫ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ] ] ; [ [ [ [ Mendelson 3.2 d_{iih} ⊳ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ]

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

=^{p} [ [ ˙0 ˙+ [ ẋ ] ] ′ ] ] ] ] ≫ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ≫ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 3.2 f ii →^{stmt} S′ ⊢ [ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ˙⇒ [ ẋ′ =^{p} [ ˙0 ˙+ [ ẋ′ ] ] ] ] ]

[Mendelson 3.2 f ii →^{tex} “Mendelson\ \textbf{3.2}\ f\ ii”]

[Mendelson 3.2 f ii →^{pyk} “mendelson proposition three two f ii”]

Mendelson 3.2 g

[Mendelson 3.2 g →^{proof} λc.λx.P(⌈S′ ⊢ [ [ Mendelson 3.2 g i ≫ [ [ ẏ′ ˙+ ˙0 ] =^{p} [ [ ẏ ˙+ ˙0 ] ′ ] ] ] ; [ [ Mendelson 3.2 g ii ≫ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ′ ] ] ′ ] ] ] ] ; [ [ [ Induction ⊳ [ [ ẏ′ ˙+ ˙0 ] =^{p} [ [ ẏ ˙+ ˙0 ] ′ ] ] ] ⊳ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ′ ] ] ′ ] ] ] ] ≫ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 3.2 g →^{stmt} S′ ⊢ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ]

[Mendelson 3.2 g →^{tex} “Mendelson\ \textbf{3.2}\ g”]

[Mendelson 3.2 g →^{pyk} “mendelson proposition three two g”]

Mendelson 3.2 g i

[Mendelson 3.2 g i →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S5′ ≫ [ [ ẏ′ ˙+ ˙0 ] =^{p} [ ẏ′ ] ] ] ; [ [ S5′ ≫ [ [ ẏ ˙+ ˙0 ] =^{p} [ ẏ ] ] ] ; [ [ [ S2′_{i} ⊳ [ [ ẏ ˙+ ˙0 ] =^{p} [ ẏ ] ] ] ≫ [ [ ẏ ˙+ ˙0 ] ′ =^{p} [ ẏ′ ] ] ] ; [ [ [ Mendelson 3.2 d_{ii} ⊳ [ [ ẏ′ ˙+ ˙0 ] =^{p} [ ẏ′ ] ] ] ⊳ [ [ ẏ ˙+ ˙0 ] ′ =^{p} [ ẏ′ ] ] ] ≫ [ [ ẏ′ ˙+ ˙0 ] =^{p} [ [ ẏ ˙+ ˙0 ] ′ ] ] ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 3.2 g i →^{stmt} S′ ⊢ [ [ ẏ′ ˙+ ˙0 ] =^{p} [ [ ẏ ˙+ ˙0 ] ′ ] ] ]

[Mendelson 3.2 g i →^{tex} “Mendelson\ \textbf{3.2}\ g\ i”]

[Mendelson 3.2 g i →^{pyk} “mendelson proposition three two g i”]

Mendelson 3.2 g ii

[Mendelson 3.2 g ii →^{proof} λc.λx.P(⌈S′ ⊢ [ [ Mendelson 1.8 ≫ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ; [ [ S6′ ≫ [ [ ẏ′ ˙+ [ ẋ′ ] ] =^{p} [ [ ẏ′ ˙+ [ ẋ ] ] ′ ] ] ] ; [ [ [ A1′_{i} ⊳ [ [ ẏ′ ˙+ [ ẋ′ ] ] =^{p} [ [ ẏ′ ˙+ [ ẋ ] ] ′ ] ] ] ≫ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ′ ] ] =^{p} [ [ ẏ′ ˙+ [ ẋ ] ] ′ ] ] ] ] ; [ [ [ S2′_{ih} ⊳ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ≫ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ ] ] ′ =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′′ ] ] ] ] ; [ [ [ [ Mendelson 3.2 c_{iih} ⊳ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ′ ] ] =^{p} [ [ ẏ′ ˙+ [ ẋ ] ] ′ ] ] ] ] ⊳ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ ] ] ′ =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′′ ] ] ] ] ≫ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′′ ] ] ] ] ; [ [ S6′ ≫ [ [ ẏ ˙+ [ ẋ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ; [ [ [ A1′_{i} ⊳ [ [ ẏ ˙+ [ ẋ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ≫ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ ˙+ [ ẋ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ; [ [ [ S2′_{ih} ⊳ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ ˙+ [ ẋ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ≫ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [

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

Mendelson 3.2 d_{iih} ⊳ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′′ ] ] ] ] ⊳ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ ˙+ [ ẋ′ ] ] ′ =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′′ ] ] ] ] ≫ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ′ ] ] ′ ] ] ] ] ; [ [ Mendelson 1.8_{i} ⊳

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

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

[Mendelson 3.2 g ii →^{stmt} S′ ⊢ [ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ˙⇒ [ [

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

[Mendelson 3.2 g ii →^{tex} “Mendelson\ \textbf{3.2}\ g\ ii”]

[Mendelson 3.2 g ii →^{pyk} “mendelson proposition three two g ii”]

Mendelson 3.2 h

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

[Mendelson 3.2 h →^{stmt} S′ ⊢ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ]

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

[Mendelson 3.2 h →^{pyk} “mendelson proposition three two h”]

Mendelson 3.2 h i

[Mendelson 3.2 h i →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S5′ ≫ [ [ ẋ ˙+ ˙0 ] =^{p} [ ẋ ] ] ] ; [ [ Mendelson 3.2 f ≫ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ; [ [ [ Mendelson 3.2 c_{ii} ⊳ [ [ ẋ ˙+ ˙0 ] =^{p} [ ẋ ] ] ] ⊳ [ ẋ =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ≫ [ [ ẋ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 3.2 h i →^{stmt} S′ ⊢ [ [ ẋ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ẋ ] ] ] ]

[Mendelson 3.2 h i →^{tex} “Mendelson\ \textbf{3.2}\ h\ i”] [Mendelson 3.2 h i →^{pyk} “mendelson proposition three two h i”]

Mendelson 3.2 h ii

[Mendelson 3.2 h ii →^{proof} λc.λx.P(⌈S′ ⊢ [ [ Mendelson 1.8 ≫ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ] ] ; [ [ S6′ ≫ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ; [ [ [ A1′_{i} ⊳ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ≫ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ] ; [ [ Mendelson 3.2 g ≫ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ; [ [ [ A1′_{i} ⊳ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ≫ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ; [ [ [ S2′_{ih} ⊳ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ] ] ≫ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ ] ] ′ =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ; [ [ [ [ Mendelson 3.2 c_{iih} ⊳ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẋ ˙+ [ ẏ ] ] ′ ] ] ] ] ⊳ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ ] ] ′ =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ≫ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ; [ [ [ [ Mendelson 3.2 d_{iih} ⊳ [

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

⊳ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẏ′ ˙+ [ ẋ ] ] =^{p} [ [ ẏ ˙+ [ ẋ ] ] ′ ] ] ] ] ≫ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ; [ [ Mendelson 1.8_{i} ⊳ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [ ẏ′ ] ] =^{p} [ ẏ′ ˙+ [ ẋ ] ] ] ] ] ≫ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+

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

[Mendelson 3.2 h ii →^{stmt} S′ ⊢ [ [ [ ẋ ˙+ [ ẏ ] ] =^{p} [ ẏ ˙+ [ ẋ ] ] ] ˙⇒ [ [ ẋ ˙+ [

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

[Mendelson 3.2 h ii →^{tex} “Mendelson\ \textbf{3.2}\ h\ ii”]

[Mendelson 3.2 h ii →^{pyk} “mendelson proposition three two h ii”]

hyp

[hyp →^{tex} “\mathsf{hyp}”]

[hyp →^{pyk} “hypothesis”]

instance

[instance →^{tex} “\mathsf{instance}”] [instance →^{pyk} “instance”]

conclusion

[conclusion →^{tex} “\mathsf{conclusion}”] [conclusion →^{pyk} “conclusion”]

∗ ⊵ ∗

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

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

\unrhd #2.”] [x ⊵ y →^{pyk} “∗ macro modus ponens ∗”]

∗ ⊵ ∗ ⊵ ∗

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

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

\unrhd #2. \unrhd #3.”] [x ⊵ y ⊵ z →^{pyk} “∗ macro first modus ponens ∗ macro second modus ponens ∗”]

∗ ⊵_{h} ∗

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

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

\unrhd h #2.”] [x ⊵_{h} y →^{pyk} “∗ hypothetical macro modus ponens ∗”]

∗ ⊵_{h} ∗ ⊵_{h} ∗

[x ⊵_{h} y ⊵_{h} z →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ⊵_{h} y ⊵_{h} z ¨= [ [ MP′_{hd} ⊳ x ] ⊳ y ] ⊳ z]⌉)] [x ⊵_{h} y ⊵_{h} z →^{tex} “#1. \unrhd h #2.

\unrhd h #3.”]

[x ⊵_{h} y ⊵_{h} z →^{pyk} “∗ hypothetical macro first modus ponens ∗ hypothetical macro second modus ponens var ∗”]

Line ∗ : • ∗ ⊵∗ ≫ ∗; ∗

[Line l : • u ⊵ v ≫ i; p →^{name} “ Line \, #1. :\bullet{}\ #2. \unrhd{} #3. \gg #4. ; #5.”]

[Line l : • u ⊵ v ≫ i; p →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Line l : • u ⊵ v ≫ i; p ¨= ( [ [ u ⊵_{h} v ] ≫ [ hyp ˙⇒ i ] ] ; let l ¨= hyp ˙⇒ i in p)]⌉)]

[Line l : • u ⊵ v ≫ i; p →^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}$#2. \unrhd{} #3. {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#4. $\hfill \makebox [0mm][l]{\quad ; }}#5.”]

[Line l : • u ⊵ v ≫ i; p →^{pyk} “line ∗ hypothesis modus ponens ∗ modus ponens ∗ indeed ∗ end line ∗”]

Line ∗ : • ∗ ∘ ⊵ ∗ ≫ ∗; ∗

[Line l : • u ∘ ⊵ v ≫ i; p →^{name} “ Line \, #1. :\bullet{}\ #2. \circ{} \unrhd{} #3. \gg #4. ; #5.”]

[Line l : • u ∘ ⊵ v ≫ i; p →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Line l : • u ∘ ⊵ v ≫ i; p ¨= ( [ [ [ Mendelson 1.47 b ⊳ v ] ⊳ u ] ≫ [ hyp ˙⇒ i ] ] ; let l ¨= hyp ˙⇒ i in p)]⌉)]

[Line l : • u ∘ ⊵ v ≫ i; p →^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}$ #2. \circ{} \unrhd{} #3. {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#4. $\hfill \makebox [0mm][l]{\quad ; }}#5.”]

[Line l : • u ∘ ⊵ v ≫ i; p →^{pyk} “line ∗ hypothesis first modus ponens ∗ modus ponens ∗ indeed ∗ end line ∗”]

Line ∗ : • ∗ ⊵ ∗ ∘ ≫ ∗; ∗

[Line l : • u ⊵ v ∘ ≫ i; p →^{name} “ Line \, #1. :\bullet{}\ #2. \unrhd{} #3. \circ{} \gg #4. ; #5.”]

[Line l : • u ⊵ v ∘ ≫ i; p →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Line l : • u ⊵ v ∘ ≫ i; p ¨= ( [ [ [ Mendelson 1.47 e ⊳ u ] ⊳ v ] ≫ [ hyp ˙⇒ i ] ] ; let l ¨= hyp ˙⇒ i in p)]⌉)]

[Line l : • u ⊵ v ∘ ≫ i; p →^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}$ #2. \unrhd{} #3. \circ{} {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#4. $\hfill \makebox [0mm][l]{\quad ; }}#5.”]

[Line l : • u ⊵ v ∘ ≫ i; p →^{pyk} “line ∗ hypothesis second modus ponens ∗ modus ponens ∗ indeed ∗ end line ∗”]

Line ∗ : • ∗ ⊵ ∗ ⊵∗ ≫ ∗; ∗

[Line l : • u ⊵ v ⊵ z ≫ i; p →^{name} “ Line \, #1. :\bullet{}\ #2. \unrhd{} #3.

\unrhd{} #4. \gg #5. ; #6.”]

[Line l : • u ⊵ v ⊵ z ≫ i; p →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Line l : • u ⊵ v ⊵ z ≫ i; p ¨= ( [ [ u ⊵_{h} v ⊵_{h} z ] ≫ [ hyp ˙⇒ i ] ] ; let l ¨= hyp ˙⇒ i in p)]⌉)]

[Line l : • u ⊵ v ⊵ z ≫ i; p →^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}$ #2. \unrhd{} #3. \unrhd{} #4. {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#5. $\hfill \makebox [0mm][l]{\quad ; }}#6.”]

[Line l : • u ⊵ v ⊵ z ≫ i; p →^{pyk} “line ∗ hypothesis double modus ponens ∗ modus ponens ∗ modus ponens ∗ indeed ∗ end line ∗”]

Line ∗ : • Hypothesis ≫ ∗; ∗

[Line l : • Hypothesis ≫ i; p →^{name} “ Line \, #1. :\bullet{}\ Hypothesis \gg #2. ; #3.”]

[Line l : • Hypothesis ≫ i; p →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Line l : • Hypothesis ≫ i; p ¨= ( [ Mendelson 1.8 ≫ [ i ˙⇒ i ] ] ; let hyp ¨= i in let l ¨= i ˙⇒ i in p)]⌉)]

[Line l : • Hypothesis ≫ i; p →^{tex} “ \newline \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}\makebox [0.4\textwidth ][l]{$Hypothesis{} \gg{}$}\quad \parbox [t]{0.4\textwidth }{$#2. $\hfill \makebox [0mm][l]{\quad ; }}#3.”]

[Line l : • Hypothesis ≫ i; p →^{pyk} “line ∗ hypothesis indeed ∗ end line ∗”]

Line ∗ : • ∗ ≫ ∗; ∗

[Line l : • a ≫ i; p →^{name} “ Line \, #1. :\bullet{}\ #2. \gg #3. ; #4.”]

[Line l : • a ≫ i; p →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Line l : • a ≫ i; p ¨= ( [ a ≫ i ] ; [ [ [ Hypothesize ⊳ i ] ≫ [ hyp ˙⇒ i ] ] ; let l ¨= hyp ˙⇒ i in p ] )]⌉)]

[Line l : • a ≫ i; p →^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}$#2. {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#3. $\hfill \makebox [0mm][l]{\quad ; }}#4.”]

[Line l : • a ≫ i; p →^{pyk} “line ∗ hypothesis because ∗ indeed ∗ end line ∗”]

Line ∗ : • ∗ ≫ ∗; ∗

[Line l : • a ≫ i; p →^{name} “ Line \, #1. :\bullet{}\ #2. \gg #3. ; #4.”]

[Line l : • a ≫ i; p →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[Line l : • a ≫ i; p ¨= ( [ a ≫ [ hyp ˙⇒ i ] ] ; let l ¨= hyp ˙⇒ i in p)]⌉)]

[Line l : • a ≫ i; p →^{tex} “ \newline \makebox [0.1\textwidth]{}% \parbox [b]{0.4\textwidth }{\raggedright \setlength {\parindent }{-0.1\textwidth }% \makebox [0.1\textwidth ][l]{$#1. $:$\bullet$}$#2. {}\gg {}$}\quad \parbox [t]{0.4\textwidth }{$#3. $\hfill \makebox [0mm][l]{\quad ; }}#4.”]

[Line l : • a ≫ i; p →^{pyk} “line ∗ hypothesis raw because ∗ indeed ∗ end line ∗”] The pyk compiler, version 0.grue.20050603 by Klaus Grue GRD-2005-07-04.UTC:07:55:10.732497 = MJD-53555.TAI:07:55:42.732497 = LGT-4627180542732497e-6