Logiweb codex of logik rapport

Up Help S′, A1′, A2′, A3′, A4′, A5′, S1′, S2′, S3′, S4′, S5′, S6′, S7′, S8′, S9′, MP′, Gen′, logik rapport, A2′^{∗}, A1′^{∗}, DoubleHypothesis, C1.10a, C1.10(b), L1.8, L3.2(b)′, L3.2(c)′, L3.2(d)′, L3.2(f)′, L3.2(f)′_{BASE}, L3.2(f)′_{HYP}, L3.2(g)′, L3.2(g)′_{BASE}, L3.2(g)′_{HYP}, L3.2(h)′, L3.2(h)′_{BASE}, L3.2(h)′_{HYP}, L3.2h_{SWAP}, Tautology1,

S′

[S′ →^{stmt} x]

A1′

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

A2′

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

A3′

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

A4′

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

A5′

[A5′ →^{proof} Rule tactic]

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

S1′

[S1′ →^{proof} Rule tactic]

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

S2′

[S2′ →^{proof} Rule tactic]

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

S3′

[S3′ →^{proof} Rule tactic]

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

S4′

[S4′ →^{proof} Rule tactic]

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

S5′

[S5′ →^{proof} Rule tactic]

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

S6′

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

S7′

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

S8′

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

S9′

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

MP′

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

Gen′

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

logik rapport

[logik rapport →^{pyk} “logik rapport”]

A2′^{∗}

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

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

[A2′^{∗} →^{tex} “{A2’}ˆ ∗”]

[A2′^{∗} →^{pyk} “lemma prime a two star”]

A1′^{∗}

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

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

[A1′^{∗} →^{tex} “{A1’}ˆ ∗”]

[A1′^{∗} →^{pyk} “lemma prime a one star”]

DoubleHypothesis

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

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

[DoubleHypothesis →^{tex} “Double Hypothesis”]

[DoubleHypothesis →^{pyk} “lemma double hyp”]

C1.10a

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

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

[C1.10a →^{tex} “C1.10a”]

[C1.10a →^{pyk} “corollary one point ten a”]

C1.10(b)

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

[C1.10(b) →^{stmt} S′ ⊢ ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: [ [ \underline{b} ˙⇒ [ \underline{c} ˙⇒ \underline{d} ] ] ⊢ [ \underline{c} ⊢ [ \underline{b} ˙⇒ \underline{d} ] ] ] ]

[C1.10(b) →^{tex} “C1.10(b)”]

[C1.10(b) →^{pyk} “corollary one point ten b”]

L1.8

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

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

[L1.8 →^{tex} “L1.8”]

[L1.8 →^{pyk} “lemma one point eight”]

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} ] ] ] ] ; [ [ L3.2(a)′ ≫ [ \underline{t} =^{p} \underline{t} ] ] ; [ [ [ C1.10(b) ⊳ [ [ \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} ] ] ] ] ] ⌉, 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 l 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} ] ] ] ; [ [ [ C1.10a ⊳ [ [ \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 l 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} ] ] ] ] ; [ [ [ Tautology1 ⊳ [ [ \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} ] ] ] ; [ [ [ [ C1.10a ⊳ [ [ \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} ] ] ] ] ; [ [ Tautology1 ⊳ [ [ \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 l three two d”]

L3.2(f)′

[L3.2(f)′ →^{proof} λc.λx.P(⌈S′ ⊢ [ [ L3.2(f)′_{BASE} ≫ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ] ; [ [ L3.2(f)′_{HYP} ≫ ˙∀ṫ: [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ; [ [ S9′ ≫ [ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ˙⇒ [ [ ˙∀ṫ: [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ˙⇒ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ˙⇒ [ [ ˙∀ṫ: [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ˙⇒ ˙∀ṫ: [ ṫ =^{p} [

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

[ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ˙⇒ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ; [ [ [ MP′ ⊳ [ [ ˙∀ṫ: [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ˙⇒ ˙∀ṫ: [ ṫ =^{p} [ ˙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 l three two f”]

L3.2(f)′_{BASE}

[L3.2(f)′_{BASE} →^{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 ] ] ] ] ] ⌉, p_{0}, c)]

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

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

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

L3.2(f)′_{HYP}

[L3.2(f)′_{HYP} →^{proof} λc.λx.P(⌈S′ ⊢ [ [ L1.8 ≫ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ =^{p} [

˙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 ˙+ [ ṫ ] ] ′ ] ] ] ] ; [ [ S2′ ≫ [ [ ṫ =^{p} [ ˙0 ˙+ [

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

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

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

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

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

˙⇒ [ ṫ′ =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′ ] ] ] ] ≫ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′ ] ] ] ] ] ; [ [ [ A2′^{∗} ⊳ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′ ] ] ] ] ] ≫ [ [ [ ṫ =^{p} [

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

] ] ] ] ] ⌉, p_{0}, c)]

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

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

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

L3.2(g)′

[L3.2(g)′ →^{proof} λc.λx.P(⌈S′ ⊢ [ [ L3.2(g)′_{BASE} ≫ ˙∀ṫ: [ [ ṫ′ ˙+ ˙0 ] =^{p} [ [ ṫ ˙+ ˙0 ] ′ ] ] ] ; [ [ L3.2(g)′_{HYP} ≫ ˙∀ṙ: [ [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ′ ] ] ′ ] ] ] ] ; [ [ S9′ ≫ [ [ ˙∀ṫ: [ [ ṫ′ ˙+ ˙0 ] =^{p} [ [ ṫ ˙+ ˙0 ] ′ ] ] ] ˙⇒ [ [ ˙∀ṙ: [ [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ˙⇒ [ [ ṫ′ ˙+ [ ṙ′ ] ] =^{p} [ [ ṫ ˙+ [ ṙ′ ] ] ′ ] ] ] ] ˙⇒ ˙∀ṙ: [ [ ṫ′ ˙+ [ ṙ ] ] =^{p} [ [ ṫ ˙+ [ ṙ ] ] ′ ] ] ]