Logiweb codex of peanorapport

Up Help

peanorapport, ˙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)′, L3.2(b)′, L3.2(c)′, L3.2(d)′, L3.2(f)′, L3.2(g)′, L3.2(g)′II, L3.2(h)′basis, L3.2(h)′, Taut1, Taut2, Taut3, Taut4, Weaken, M1.7, MPTwice, ˙∗, ∗′, ∗ ˙· ∗, ∗ ˙+ ∗, ∗ =^{p} ∗, ∗^{P}, ˙¬ ∗, ˙∀∗: ∗, ∗ ˙⇒ ∗,

peanorapport

[peanorapport →^{pyk} “peanorapport”]

˙0

[˙0 →^{tex} “

\dot{0}”]

[˙0 →^{pyk} “peano zero”]

˙1

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

[˙1 →^{tex} “

\dot{1}”]

[˙1 →^{pyk} “peano one”]

˙2

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

[˙2 →^{tex} “

\dot{2}”]

[˙2 →^{pyk} “peano two”]

ȧ

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

[ȧ →^{tex} “

\dot{\mathit{a}}”] [ȧ →^{pyk} “peano a”]

ḃ

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

[ḃ →^{tex} “

\dot{\mathit{b}}”] [ḃ →^{pyk} “peano b”]

ċ

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

[ċ →^{tex} “

\dot{\mathit{c}}”] [ċ →^{pyk} “peano c”]

ḋ

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

[ḋ →^{tex} “

\dot{\mathit{d}}”] [ḋ →^{pyk} “peano d”]

ė

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

[ė →^{tex} “

\dot{\mathit{e}}”] [ė →^{pyk} “peano e”]

ḟ

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

[ḟ →^{tex} “

\dot{\mathit{f}}”] [ḟ →^{pyk} “peano f”]

ġ

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

[ġ →^{tex} “

\dot{\mathit{g}}”] [ġ →^{pyk} “peano g”]

ḣ

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

[ḣ →^{tex} “

\dot{\mathit{h}}”] [ḣ →^{pyk} “peano h”]

i̇

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

[i̇ →^{tex} “

\dot{\mathit{i}}”] [i̇ →^{pyk} “peano i”]

j̇

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

[j̇ →^{tex} “

\dot{\mathit{j}}”] [j̇ →^{pyk} “peano j”]

k̇

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

[k̇ →^{tex} “

\dot{\mathit{k}}”] [k̇ →^{pyk} “peano k”]

l̇

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

[l̇ →^{tex} “

\dot{\mathit{l}}”] [l̇ →^{pyk} “peano l”]

ṁ

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

[ṁ →^{tex} “

\dot{\mathit{m}}”] [ṁ →^{pyk} “peano m”]

ṅ

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

[ṅ →^{tex} “

\dot{\mathit{n}}”] [ṅ →^{pyk} “peano n”]

ȯ

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

[ȯ →^{tex} “

\dot{\mathit{o}}”] [ȯ →^{pyk} “peano o”]

ṗ

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

[ṗ →^{tex} “

\dot{\mathit{p}}”] [ṗ →^{pyk} “peano p”]

q̇

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

[q̇ →^{tex} “

\dot{\mathit{q}}”] [q̇ →^{pyk} “peano q”]

ṙ

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

[ṙ →^{tex} “

\dot{\mathit{r}}”] [ṙ →^{pyk} “peano r”]

ṡ

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

[ṡ →^{tex} “

\dot{\mathit{s}}”] [ṡ →^{pyk} “peano s”]

ṫ

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

[ṫ →^{tex} “

\dot{\mathit{t}}”] [ṫ →^{pyk} “peano t”]

u̇

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

[u̇ →^{tex} “

\dot{\mathit{u}}”] [u̇ →^{pyk} “peano u”]

v̇

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

[v̇ →^{tex} “

\dot{\mathit{v}}”] [v̇ →^{pyk} “peano v”]

ẇ

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

[ẇ →^{tex} “

\dot{\mathit{w}}”] [ẇ →^{pyk} “peano w”]

ẋ

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

[ẋ →^{tex} “

\dot{\mathit{x}}”] [ẋ →^{pyk} “peano x”]

ẏ

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

[ẏ →^{tex} “

\dot{\mathit{y}}”] [ẏ →^{pyk} “peano y”]

ż

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

[ż →^{tex} “

\dot{\mathit{z}}”]

[ż →^{pyk} “peano z”]

ṅonfree(∗, ∗)

[ṅonfree(x, y) →^{val}

If(y^{P}, ¬ [ x =^{t} y ] ,

If(¬ [ y =^{r} ⌈ ˙∀x: y⌉ ] , ṅonfree^{∗}(x, y^{t}), If(x =^{t} [ y^{1} ] , T, ṅonfree(x, y^{2}))))]

[ṅonfree(x, y) →^{tex} “ \dot{nonfree}(#1. , #2. )”]

[ṅonfree(x, y) →^{pyk} “peano nonfree ∗ in ∗ end nonfree”]

ṅonfree^{∗}(∗, ∗)

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

[ṅonfree^{∗}(x, y) →^{tex} “ \dot{nonfree}ˆ ∗(#1. , #2. )”]

[ṅonfree^{∗}(x, y) →^{pyk} “peano nonfree star ∗ in ∗ end nonfree”]

ḟree⟨∗|∗ := ∗⟩

[ḟree⟨a|x := b⟩ →^{val} x! [ b! If(a^{P}, T, If(¬ [ a =^{r} ⌈ ˙∀u: v⌉ ] , ḟree^{∗}⟨a^{t}|x := b⟩,

If(a^{1} =^{t} x, T,

If(ṅonfree(x, a^{2}), T, If(¬ṅonfree(a^{1}, b), F, ḟree⟨a^{2}|x := b⟩))))) ] ]

[ḟree⟨a|x := b⟩ →^{tex} “ \dot{free}\langle #1. | #2. := #3. \rangle”]

[ḟree⟨a|x := b⟩ →^{pyk} “peano free ∗ set ∗ to ∗ end free”]

ḟree^{∗}⟨∗|∗ := ∗⟩

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

[ḟree^{∗}⟨a|x := b⟩ →^{tex} “ \dot{free}{}ˆ ∗\langle #1. | #2. := #3. \rangle”]

[ḟree^{∗}⟨a|x := b⟩ →^{pyk} “peano free star ∗ set ∗ to ∗ end free”]

∗≡⟨∗|∗ := ∗⟩

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

[a≡⟨b|x := c⟩ →^{tex} “#1.

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

[a≡⟨b|x := c⟩ →^{pyk} “peano sub ∗ is ∗ where ∗ is ∗ end sub”]

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

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

[a≡⟨^{∗}b|x := c⟩ →^{tex} “#1.

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

[a≡⟨^{∗}b|x := c⟩ →^{pyk} “peano sub star ∗ is ∗ where ∗ is ∗ end sub”]

S′

[S′ →^{stmt} [ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} ˙+ [ \underline{b}′ ] ] =^{p} [ [ \underline{a} ˙+ \underline{b} ] ′ ] ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: [ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ˙⇒ \underline{b} ] ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ \underline{a}′ =^{p} [ \underline{b}′ ] ] ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} ˙⇒ \underline{b} ] ⊢ [ \underline{a} ⊢ \underline{b} ] ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a}′ =^{p} [ \underline{b}′ ] ] ˙⇒ [ \underline{a} =^{p} \underline{b} ] ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{a} ] ] ] ⊕ [ [ ∀\underline{x}: ∀\underline{a}: ∀\underline{b}: [ ṅonfree(⌈\underline{x}⌉, ⌈\underline{a}⌉) ⊢⊢ [ [ ˙∀\underline{x}: [ \underline{a} ˙⇒ \underline{b} ] ] ˙⇒ [ \underline{a} ˙⇒ ˙∀\underline{x}: \underline{b} ] ] ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} ˙· [ \underline{b}′ ] ] =^{p} [ [ \underline{a} ˙· \underline{b} ] ˙+ \underline{a} ] ] ] ⊕ [ [ ∀\underline{a}: [ [ \underline{a} ˙+ ˙0 ] =^{p} \underline{a} ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} =^{p} \underline{b} ] ˙⇒ [ [ \underline{a} =^{p} \underline{c} ] ˙⇒ [ \underline{b} =^{p} \underline{c} ] ] ] ] ⊕ [ [ ∀\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} ] ] ] ] ] ⊕ [ [ ∀\underline{a}: ¬ [ ˙0 =^{p} [ \underline{a}′ ] ] ] ⊕ [ [ ∀\underline{x}: ∀\underline{a}: [ \underline{a} ⊢ ˙∀\underline{x}: \underline{a} ] ] ⊕ [ [ ∀\underline{c}: ∀\underline{a}: ∀\underline{x}: ∀\underline{b}: [ ⌈\underline{a}⌉≡⟨⌈\underline{b}⌉|⌈\underline{x}⌉ := ⌈\underline{c}⌉⟩ ⊢⊢ [ [ ˙∀\underline{x}: \underline{b} ] ˙⇒ \underline{a} ] ] ] ⊕ ∀\underline{a}: [ [ \underline{a} ˙· ˙0 ] =^{p} ˙0 ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ]

[S′ →^{tex} “

S’”]

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

A1′

[A1′ →^{proof} Rule tactic]

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

[A1′ →^{tex} “

A1’”]

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

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

[A2′ →^{tex} “

A2’”] [A2′ →^{pyk} “axiom prime a two”]

A3′

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

[A3′ →^{tex} “

A3’”] [A3′ →^{pyk} “axiom prime a three”]

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

[A4′ →^{tex} “

A4’”] [A4′ →^{pyk} “axiom prime a four”]

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

[A5′ →^{tex} “

A5’”] [A5′ →^{pyk} “axiom prime a five”]

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

[S1′ →^{tex} “

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

S2′

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

[S2′ →^{tex} “

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

S3′

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

[S3′ →^{tex} “

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

S4′

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

[S4′ →^{tex} “

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

S5′

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

[S5′ →^{tex} “

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

S6′

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

[S6′ →^{tex} “

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

S7′

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

[S7′ →^{tex} “

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

S8′

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

[S8′ →^{tex} “

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

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

[S9′ →^{tex} “

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

MP′

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

[MP′ →^{tex} “

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

Gen′

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

[Gen′ →^{tex} “

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

L3.2(a)′

[L3.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} ] ] ] ] ; [ [ [ [ MPTwice ⊳ [ [ [ \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} ] ] ] ] ⌉, p_{0}, c)] [L3.2(a)′ →^{stmt} S′ ⊢ ∀\underline{t}: [ \underline{t} =^{p} \underline{t} ] ]

[L3.2(a)′ →^{tex} “L3.2 (a)’”]

[L3.2(a)′ →^{pyk} “lemma prime three two a”]

L3.2(b)′

[L3.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} ] ] ] ] ; [ [ [ Taut1 ⊳ [ [ \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} ] ] ] ] ; [ [ L3.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)]

[L3.2(b)′ →^{stmt} S′ ⊢ ∀\underline{t}: ∀\underline{r}: [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ]

[L3.2(b)′ →^{tex} “L3.2 (b)’”]

[L3.2(b)′ →^{pyk} “lemma prime three two b”]

L3.2(c)′

[L3.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} ] ] ] ] ; [ [ L3.2(b)′ ≫ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ; [ [ [ Taut2 ⊳ [ [ \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)]

[L3.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} ] ] ] ]

[L3.2(c)′ →^{tex} “L3.2 (c)’”]

[L3.2(c)′ →^{pyk} “lemma prime three two c”]

L3.2(d)′

[L3.2(d)′ →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: [ [ L3.2(c)′ ≫ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{t} =^{p} \underline{s} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ; [ [ [ Taut1 ⊳ [ [ \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} ] ] ] ] ; [ [ L3.2(b)′ ≫ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ; [ [ [ [ Taut2 ⊳ [ [ \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} ] ] ] ] ; [ [ Taut1 ⊳ [ [ \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)]

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

[L3.2(d)′ →^{tex} “L3.2 (d)’”]

[L3.2(d)′ →^{pyk} “lemma prime three two d”]

L3.2(f)′

[L3.2(f)′ →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S5′ ≫ [ [ ˙0 ˙+ ˙0 ] =^{p} ˙0 ] ] ; [ [ L3.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 ] ] ] ; [ [ S6′ ≫ [

[ ˙0 ˙+ [ ṫ′ ] ] =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′ ] ] ] ; [ [ A1′ ≫ [ [ [ ˙0 ˙+ [ ṫ′ ] ] =^{p} [ [ ˙0 ˙+

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

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

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

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

˙0 ˙+ [ ṫ ] ] ′ ] ] ] ] ; [ [ M1.7 ≫ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ]

] ] ] ; [ [ S2′ ≫ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′ ] ] ] ] ; [ [

[ [ Taut2 ⊳ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ⊳ [ [ ṫ =^{p} [

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

ṫ′ =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′ ] ] ] ] ; [ [ L3.2(d)′ ≫ [ [ ṫ′ =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′ ] ] ˙⇒ [

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

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

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

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

′ ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ] ; [ [ [ [ Taut3 ⊳ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ]

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

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

ṫ′ ] ] ] ] ] ; [ [ S9′ ≫ [ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ˙⇒ [ [ ˙∀ṫ: [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ]

˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ˙⇒ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ] ; [ [ [ [

MPTwice ⊳ [ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ˙⇒ [ [ ˙∀ṫ: [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [

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

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

[L3.2(f)′ →^{stmt} S′ ⊢ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ]

[L3.2(f)′ →^{tex} “L3.2 (f)’”]

[L3.2(f)′ →^{pyk} “lemma prime three two f”]

L3.2(g)′

[L3.2(g)′ →^{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} [ ṫ′ ] ] ] ; [ [ L3.2(d)′ ≫ [ [ [ ṫ′ ˙+ ˙0 ] =^{p} [ ṫ′ ] ] ˙⇒ [ [ [ ṫ ˙+ ˙0 ] ′ =^{p} [ ṫ′ ] ] ˙⇒ [ [ ṫ′ ˙+ ˙0 ] =^{p} [ [ ṫ ˙+ ˙0 ] ′ ] ] ] ] ] ; [ [ [ [ [ MPTwice ⊳ [ [ [ ṫ′ ˙+ ˙0 ] =^{p} [ ṫ′ ] ] ˙⇒ [ [ [ ṫ ˙+ ˙0 ] ′ =^{p} [ ṫ′ ] ] ˙⇒ [ [ ṫ′ ˙+ ˙0 ] =^{p} [ [ ṫ ˙+ ˙0 ] ′ ] ] ] ] ] ⊳ [ [ ṫ′ ˙+ ˙0 ] =^{p} [ ṫ′ ] ] ] ⊳ [ [ ṫ ˙+ ˙0 ] ′ =^{p} [ ṫ′ ] ] ] ≫ [ [ ṫ′ ˙+ ˙0 ] =^{p} [ [ ṫ ˙+ ˙0 ] ′ ] ] ] ; [ [ S6′ ≫ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ′ ˙+ [ ṙ ] ] ′ ] ] ] ; [ [ [ Weaken ⊳ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ′ ˙+ [ ṙ ] ] ′ ] ] ] ≫ [ [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ′ ˙+ [ ṙ ] ] ′ ] ] ] ] ; [ [ S2′ ≫ [ [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ] ] ; [ [ L3.2(c)′ ≫ [ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ′ ˙+ [ ṙ ]

] ′ ] ] ˙⇒ [ [ [ ṫ′ ˙+ [ ṙ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [

ṫ ˙+ [ ṙ ] ] ′′ ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ′ ˙+ [ ṙ ] ] ′ ] ]

˙⇒ [ [ [ ṫ′ ˙+ [ ṙ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ]

] ′′ ] ] ] ] ] ⊳ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ′ ˙+ [ ṙ ] ] ′ ] ] ] ≫ [ [ [ ṫ′ ˙+ [ ṙ ] ]

′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ] ] ; [ [ [ [ Taut2 ⊳ [ [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ] ] ⊳ [ [ [ ṫ′ ˙+ [ ṙ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ] ] ≫ [ [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ] ] ; [ [ S6′ ≫ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ] ; [ [ S2′ ≫ [ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ] ] ⊳ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [

[ ṫ ˙+ [ ṙ ] ] ′ ] ] ] ≫ [ [ ṫ ˙+ [ ṙ′ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ] ; [ [

L3.2(d)′ ≫ [ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ˙⇒ [ [ [ ṫ ˙+ [ ṙ′ ] ] ′ =^{p} [

[ ṫ ˙+ [ ṙ ] ] ′′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ′ ] ] ′ ] ] ] ] ] ; [ [ [ [

Taut2 ⊳ [ [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ] ] ⊳ [ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ˙⇒ [ [ [ ṫ ˙+ [ ṙ′ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ′ ] ] ′ ] ] ] ] ] ≫ [

[ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ [ ṫ ˙+ [ ṙ′ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ]

] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ′ ] ] ′ ] ] ] ] ] ; [ [ [ Taut1 ⊳ [ [ [ ṫ′ ˙+ [ ṙ

] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ [ ṫ ˙+ [ ṙ′ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ˙⇒ [ [

ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ′ ] ] ′ ] ] ] ] ] ≫ [ [ [ ṫ ˙+ [ ṙ′ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ]

] ′′ ] ] ˙⇒ [ [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [

ṫ ˙+ [ ṙ′ ] ] ′ ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ ṫ ˙+ [ ṙ′ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ]

˙⇒ [ [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ′ ]

] ′ ] ] ] ] ] ⊳ [ [ ṫ ˙+ [ ṙ′ ] ] ′ =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′′ ] ] ] ≫ [ [ [ ṫ′ ˙+ [ ṙ ] ]

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

] =^{p} [ [ ṫ ˙+ [ ṙ′ ] ] ′ ] ] ] ] ; [ [ S9′ ≫ [ [ [ ṫ′ ˙+ ˙0 ] =^{p} [ [ ṫ ˙+ ˙0 ] ′ ] ] ˙⇒ [

[ ˙∀ṙ: [ [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ′

] ] ′ ] ] ] ] ˙⇒ ˙∀ṙ: [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ] ] ] ; [ [ [ [ [

MPTwice ⊳ [ [ [ ṫ′ ˙+ ˙0 ] =^{p} [ [ ṫ ˙+ ˙0 ] ′ ] ] ˙⇒ [ [ ˙∀ṙ: [ [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ′ ] ] ′ ] ] ] ] ˙⇒ ˙∀ṙ: [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ] ] ] ⊳ [ [ ṫ′ ˙+ ˙0 ] =^{p} [ [ ṫ ˙+ ˙0 ] ′ ] ] ] ⊳ ˙∀ṙ: [ [

[ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ′ ] ] ′ ] ] ]

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

[L3.2(g)′ →^{stmt} S′ ⊢ ˙∀ṫ: ˙∀ṙ: [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ]

[L3.2(g)′ →^{tex} “L3.2 (g)’”]

[L3.2(g)′ →^{pyk} “lemma prime three two g”]

L3.2(g)′II

[L3.2(g)′II →^{proof} λc.λx.P(⌈S′ ⊢ [ [ L3.2(g)′ ≫ ˙∀ṫ: ˙∀ṙ: [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ] ; [ ⌈ ˙∀ṙ: [ [ ṡ′ ˙+ [ ṙ ] ] =^{p} [ [ ṡ ˙+ [ ṙ ] ] ′ ] ] ⌉≡⟨⌈ ˙∀ṙ: [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ⌉|⌈ṫ⌉ := ⌈ṡ⌉⟩ ⊢⊢ [ [ [ A4′ ⊳ ⊳ ⌈ ˙∀ṙ: [ [ ṡ′ ˙+ [ ṙ ] ] =^{p} [ [ ṡ ˙+ [ ṙ ] ] ′ ] ] ⌉≡⟨⌈ ˙∀ṙ: [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ⌉|⌈ṫ⌉ := ⌈ṡ⌉⟩ ] ≫ [ [ ˙∀ṫ: ˙∀ṙ: [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ] ˙⇒ ˙∀ṙ: [ [ ṡ′ ˙+ [ ṙ ] ] =^{p} [ [ ṡ ˙+ [ ṙ ] ] ′ ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ˙∀ṫ: ˙∀ṙ: [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ] ˙⇒ ˙∀ṙ: [ [ ṡ′ ˙+ [ ṙ ] ] =^{p} [ [ ṡ ˙+ [ ṙ ] ] ′ ] ] ] ] ⊳ ˙∀ṫ: ˙∀ṙ: [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ] ≫ ˙∀ṙ: [ [ ṡ′ ˙+ [ ṙ ] ] =^{p} [ [ ṡ ˙+ [ ṙ ] ] ′ ] ] ] ; [ ⌈ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ] ⌉≡⟨⌈ [ ṡ′ ˙+ [ ṙ ] ] =^{p} [ [ ṡ ˙+ [ ṙ ] ] ′ ] ⌉|⌈ṙ⌉ := ⌈ṫ⌉⟩ ⊢⊢ [ [ [ A4′ ⊳ ⊳ ⌈ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ] ⌉≡⟨⌈ [ ṡ′ ˙+ [ ṙ ] ] =^{p} [ [ ṡ ˙+ [ ṙ ] ] ′ ] ⌉|⌈ṙ⌉ := ⌈ṫ⌉⟩ ] ≫ [ [ ˙∀ṙ: [ [ ṡ′ ˙+ [ ṙ ] ] =^{p} [ [ ṡ ˙+ [ ṙ ] ] ′ ] ] ] ˙⇒ [ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ˙∀ṙ: [

[ ṡ′ ˙+ [ ṙ ] ] =^{p} [ [ ṡ ˙+ [ ṙ ] ] ′ ] ] ] ˙⇒ [ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ] ]

] ] ⊳ ˙∀ṙ: [ [ ṡ′ ˙+ [ ṙ ] ] =^{p} [ [ ṡ ˙+ [ ṙ ] ] ′ ] ] ] ≫ [ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ] ] ] ; [ [ [ Gen′ ⊳ [ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ] ] ] ≫ ˙∀ṡ: [ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ] ] ] ; [ ⌈ [ ṙ′ ˙+ [ ṫ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ⌉≡⟨⌈ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ] ⌉|⌈ṡ⌉ := ⌈ṙ⌉⟩ ⊢⊢ [ [ [ A4′ ⊳ ⊳ ⌈ [ ṙ′ ˙+ [ ṫ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ⌉≡⟨⌈ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ] ⌉|⌈ṡ⌉ := ⌈ṙ⌉⟩ ] ≫ [ [ ˙∀ṡ: [ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ] ] ] ˙⇒ [ [ ṙ′ ˙+ [ ṫ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ] ; [ [ [ MP′ ⊳ [ [ ˙∀ṡ: [ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ] ] ] ˙⇒ [ [ ṙ′ ˙+ [ ṫ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ] ⊳ ˙∀ṡ: [ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ]

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

[L3.2(g)′II →^{stmt} S′ ⊢ [ ⌈ ˙∀ṙ: [ [ ṡ′ ˙+ [ ṙ ] ] =^{p} [ [ ṡ ˙+ [ ṙ ] ] ′ ] ] ⌉≡⟨⌈ ˙∀ṙ: [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ⌉|⌈ṫ⌉ := ⌈ṡ⌉⟩ ⊢⊢ [ ⌈ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ] ⌉≡⟨⌈ [ ṡ′ ˙+ [ ṙ ] ] =^{p} [ [ ṡ ˙+ [ ṙ ] ] ′ ] ⌉|⌈ṙ⌉ := ⌈ṫ⌉⟩ ⊢⊢ [ ⌈ [ ṙ′ ˙+ [ ṫ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ⌉≡⟨⌈ [ ṡ′ ˙+ [ ṫ ] ] =^{p} [ [ ṡ ˙+ [ ṫ ] ] ′ ] ⌉|⌈ṡ⌉ := ⌈ṙ⌉⟩ ⊢⊢ [ [ ṙ′ ˙+

[ ṫ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ] ] ]

[L3.2(g)′II →^{tex} “L3.2 (g)’ II”]

[L3.2(g)′II →^{pyk} “lemma prime three two g rev”]

L3.2(h)′basis

[L3.2(h)′basis →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S5′ ≫ [ [ ṫ ˙+ ˙0 ] =^{p} [ ṫ ] ] ] ; [ [ L3.2(f)′ ≫ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ; [ ⌈ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ⌉≡⟨⌈ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ⌉|⌈ṫ⌉ := ⌈ṫ⌉⟩ ⊢⊢ [ [ [ A4′ ⊳ ⊳ ⌈ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ⌉≡⟨⌈ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ⌉|⌈ṫ⌉ := ⌈ṫ⌉⟩ ] ≫ [ [ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ˙⇒ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ˙⇒ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ⊳ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ≫ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ; [ [ L3.2(c)′ ≫ [ [ [ ṫ ˙+ ˙0 ] =^{p} [ ṫ ] ] ˙⇒ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ] ; [ [ [ [ [ MPTwice ⊳ [ [ [ ṫ ˙+ ˙0 ] =^{p} [ ṫ ] ] ˙⇒ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ] ⊳ [ [ ṫ ˙+ ˙0 ] =^{p} [ ṫ ] ] ] ⊳ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ]

] ] ≫ [ [ ṫ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ; [ [ S9′ ≫ [ [ [ ṫ ˙+ ˙0 ] =^{p} [ ˙0 ˙+ [ ṫ ] ]

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

[L3.2(h)′basis →^{stmt} S′ ⊢ [ ⌈ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ⌉≡⟨⌈ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ⌉|⌈ṫ⌉ := ⌈ṫ⌉⟩ ⊢⊢ [ [ ˙∀ṙ: [ [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ ṙ′ ˙+ [ ṫ ] ] ]

] ] ˙⇒ ˙∀ṙ: [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ] ] ]

[L3.2(h)′basis →^{tex} “L3.2 (h)’ basis”]

[L3.2(h)′basis →^{pyk} “lemma prime three two h base”]

L3.2(h)′

[L3.2(h)′ →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S6′ ≫ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ] ; [ [ L3.2(g)′II ≫ [ [ ṙ′ ˙+ [ ṫ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ; [ [ S2′ ≫ [ [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ ] ] ′ =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ] ; [ [ L3.2(c)′ ≫ [ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ [ ṫ ˙+ [ ṙ ] ] ′ =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ] ] ; [ [ [ [ MP′ ⊳

[ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ [ ṫ ˙+ [ ṙ ] ] ′ =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′

] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ] ] ⊳ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ] ≫ [ [ [ ṫ ˙+ [ ṙ ] ] ′ =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ] ; [ [ [ [ Taut2 ⊳ [ [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ ] ] ′ =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ] ⊳ [ [ [ ṫ ˙+ [ ṙ ] ] ′ =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ] ≫ [ [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ] ; [ [ L3.2(d)′ ≫ [ [ [

ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ˙⇒ [ [ [ ṙ′ ˙+ [ ṫ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ]

˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ ṙ′ ˙+ [ ṫ ] ] ] ] ] ] ; [ [ [ [ Taut2 ⊳ [ [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ] ⊳ [ [ [ ṫ ˙+ [ ṙ′

] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ˙⇒ [ [ [ ṙ′ ˙+ [ ṫ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ˙⇒ [ [

ṫ ˙+ [ ṙ′ ] ] =^{p} [ ṙ′ ˙+ [ ṫ ] ] ] ] ] ] ≫ [ [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ˙⇒ [

[ [ ṙ′ ˙+ [ ṫ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ ṙ′ ˙+ [ ṫ ] ] ] ] ]

] ; [ [ [ [ Taut4 ⊳ [ [ ṙ′ ˙+ [ ṫ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ⊳ [ [ [ ṫ ˙+ [ ṙ ] ]

=^{p} [ ṙ ˙+ [ ṫ ] ] ] ˙⇒ [ [ [ ṙ′ ˙+ [ ṫ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ]

=^{p} [ ṙ′ ˙+ [ ṫ ] ] ] ] ] ] ≫ [ [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ ṙ′ ˙+ [ ṫ ] ] ] ] ] ; [ [ [ Gen′ ⊳ [ [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ ṙ′ ˙+ [ ṫ ] ] ] ] ] ≫ ˙∀ṙ: [ [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ ṙ′ ˙+ [ ṫ ] ] ] ] ] ; [ [ L3.2(h)′basis ≫ [ [ ˙∀ṙ: [ [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ ṙ′ ˙+ [ ṫ ] ] ] ] ] ˙⇒ ˙∀ṙ: [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ˙∀ṙ: [ [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ ṙ′ ˙+ [ ṫ ] ] ] ] ] ˙⇒ ˙∀ṙ: [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ] ] ⊳ ˙∀ṙ: [ [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ ˙+ [ ṙ′ ] ] =^{p} [ ṙ′ ˙+ [ ṫ ] ] ] ] ] ≫ ˙∀ṙ: [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ] ; [ [ Gen′ ⊳ ˙∀ṙ: [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ] ≫ ˙∀ṫ: ˙∀ṙ: [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[L3.2(h)′ →^{stmt} S′ ⊢ ˙∀ṫ: ˙∀ṙ: [ [ ṫ ˙+ [ ṙ ] ] =^{p} [ ṙ ˙+ [ ṫ ] ] ] ]

[L3.2(h)′ →^{tex} “L3.2 (h)’”]

[L3.2(h)′ →^{pyk} “lemma prime three two h”]

Taut1

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

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

[Taut1 →^{tex} “Taut 1”]

[Taut1 →^{pyk} “lemma tautology one”]

Taut2

[Taut2 →^{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} ] ] ] ] ; [ [ [ [ MPTwice ⊳ [ [ \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} ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[Taut2 →^{tex} “Taut 2”]

[Taut2 →^{pyk} “lemma tautology two”]

Taut3

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

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

[Taut3 →^{tex} “Taut 3”]

[Taut3 →^{pyk} “lemma tautology three”]

Taut4

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

[Taut4 →^{tex} “Taut 4”]

[Taut4 →^{pyk} “lemma tautology four”]

Weaken

[Weaken →^{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)]

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

[Weaken →^{tex} “Weaken”]

[Weaken →^{pyk} “lemma weaken”]

M1.7

[M1.7 →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{b}: [ [ A1′ ≫ [ \underline{b} ˙⇒ [ [ \underline{b} ˙⇒ \underline{b} ] ˙⇒ \underline{b} ] ] ] ; [ [ A2′ ≫ [ [ \underline{b} ˙⇒ [ [ \underline{b} ˙⇒ \underline{b} ] ˙⇒ \underline{b} ] ] ˙⇒ [ [ \underline{b} ˙⇒ [ \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)]

[M1.7 →^{stmt} S′ ⊢ ∀\underline{b}: [ \underline{b} ˙⇒ \underline{b} ] ]

[M1.7 →^{tex} “

M1.7”]

[M1.7 →^{pyk} “mendelson one seven”]

MPTwice

[MPTwice →^{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)]

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

[MPTwice →^{tex} “MPTwice”]

[MPTwice →^{pyk} “lemma mp twice”]

˙∗

[ẋ →^{tex} “

\dot{#1. }”]

[ẋ →^{pyk} “∗ peano var”]

∗′

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

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

∗ ˙· ∗

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

\mathop{\dot{\cdot}} #2.”]

[x ˙· y →^{pyk} “∗ peano times ∗”]

∗ ˙+ ∗

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

\mathop{\dot{+}} #2.”]

[x ˙+ y →^{pyk} “∗ peano plus ∗”]

∗ =^{p} ∗

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

\stackrel{p}{=} #2.”]

[x =^{p} y →^{pyk} “∗ peano is ∗”]

∗^{P}

[x^{P} →^{val} x =^{r} ⌈ẋ⌉]

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

{} ˆ {\cal P}”] [x^{P} →^{pyk} “∗ is peano var”]

˙¬ ∗

[ ˙¬ x →^{tex} “

\dot{\neg}\, #1.”]

[ ˙¬ x →^{pyk} “peano not ∗”]

˙∀∗: ∗

[ ˙∀x: y →^{tex} “

\dot{\forall} #1. \colon #2.”]

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

∗ ˙⇒ ∗

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

\mathrel{\dot{\Rightarrow}} #2.”]

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

The pyk compiler, version 0.grue.20050603 by Klaus Grue GRD-2005-06-30.UTC:07:14:31.615667 = MJD-53551.TAI:07:15:03.615667 = LGT-4626832503615667e-6