Logiweb codex of peano commutativity

Up Help

A1′, A2′, A3′, A4′, A5′, S1′, S2′, S3′, S4′, S5′, S6′, S7′, S8′, S9′, MP′, Gen′, peano commutativity, Weakening, ConditionedMP′, PermuteAntecedents, ImplyTransitivity, EqualReflexivity, EqualSymmetry, EqualTransitivity, Mendelson3.2(d), SubstitutionMacro, Mendelson3.2(f)Base, Mendelson3.2(f)Indu, Mendelson3.2(f), Mendelson3.2(g)Base, Mendelson3.2(g)Indu, Mendelson3.2(g), Mendelson3.2(g)Switch, AddOne, Mendelson3.2(d)Rule, Mendelson3.2(d)CondRule, EqualTransitivityRule, EqualTransitivityCondRule, PlusCommutativityBase, PlusCommutativityIndu, PlusCommutativity, DoubleMP′, InductionMacro, EqualSymmetryRule, DoubleConditionedMP′,

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{b} ] ˙⇒ ˙¬ \underline{a} ] ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ˙⇒ \underline{b} ] ] ]

A4′

[A4′ →^{proof} Rule tactic]

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

A5′

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

S1′

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

S2′

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

S3′

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

S4′

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

S5′

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

S6′

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

S7′

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

S8′

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

S9′

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

MP′

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

Gen′

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

peano commutativity

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

Weakening

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

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

[Weakening →^{tex} “Weakening”]

[Weakening →^{pyk} “weakening”]

ConditionedMP′

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

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

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

[ConditionedMP′ →^{pyk} “conditioned mp prime”]

PermuteAntecedents

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

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

[PermuteAntecedents →^{tex} “PermuteAntecedents”]

[PermuteAntecedents →^{pyk} “permute antecedents”]

ImplyTransitivity

[ImplyTransitivity →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{d}: ∀\underline{e}: ∀\underline{f}: [ [ \underline{d} ˙⇒ \underline{e} ] ⊢ [ [ \underline{e} ˙⇒ \underline{f} ] ⊢ [ [ [ Weakening ⊳ [ \underline{e} ˙⇒ \underline{f} ] ] ≫ [ \underline{d} ˙⇒ [ \underline{e} ˙⇒ \underline{f} ] ] ] ; [ [ [ ConditionedMP′ ⊳ [ \underline{d} ˙⇒ [ \underline{e} ˙⇒ \underline{f} ] ] ] ⊳ [ \underline{d} ˙⇒ \underline{e} ] ] ≫ [ \underline{d} ˙⇒ \underline{f} ] ] ] ] ] ⌉, p_{0}, c)]

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

[ImplyTransitivity →^{tex} “ImplyTransitivity”]

[ImplyTransitivity →^{pyk} “imply transitivity”]

EqualReflexivity

[EqualReflexivity →^{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} ] ] ] ] ; [ [ [ [ DoubleMP′ ⊳ [ [ [ \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)]

[EqualReflexivity →^{stmt} S′ ⊢ ∀\underline{t}: [ \underline{t} =^{p} \underline{t} ] ]

[EqualReflexivity →^{tex} “EqualReflexivity”]

[EqualReflexivity →^{pyk} “equal reflexivity”]

EqualSymmetry

[EqualSymmetry →^{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} ] ] ] ] ; [ [ [ PermuteAntecedents ⊳ [ [ \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} ] ] ] ] ; [ [ EqualReflexivity ≫ [ \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)]

[EqualSymmetry →^{stmt} S′ ⊢ ∀\underline{t}: ∀\underline{r}: [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ]

[EqualSymmetry →^{tex} “EqualSymmetry”]

[EqualSymmetry →^{pyk} “equal symmetry”]

EqualTransitivity

[EqualTransitivity →^{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} ] ] ] ] ; [ [ [ Weakening ⊳ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ≫ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ] ; [ [ EqualSymmetry ≫ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ; [ [ [ ConditionedMP′ ⊳ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ] ⊳ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ≫ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[EqualTransitivity →^{stmt} S′ ⊢ ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ]

[EqualTransitivity →^{tex} “EqualTransitivity”]

[EqualTransitivity →^{pyk} “equal transitivity”]

Mendelson3.2(d)

[Mendelson3.2(d) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: ∀\underline{u}: ∀\underline{s}: [ [ EqualTransitivity ≫ [ [ \underline{t} =^{p} \underline{u} ] ˙⇒ [ [ \underline{u} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ; [ [ [ PermuteAntecedents ⊳ [ [ \underline{t} =^{p} \underline{u} ] ˙⇒ [ [ \underline{u} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ≫ [ [ \underline{u} =^{p} \underline{s} ] ˙⇒ [ [ \underline{t} =^{p} \underline{u} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ; [ [ EqualSymmetry ≫ [ [ \underline{s} =^{p} \underline{u} ] ˙⇒ [ \underline{u} =^{p} \underline{s} ] ] ] ; [ [ [ [ ImplyTransitivity ⊳ [ [ \underline{s} =^{p} \underline{u} ] ˙⇒ [ \underline{u} =^{p} \underline{s} ] ] ] ⊳ [ [ \underline{u} =^{p} \underline{s} ] ˙⇒ [ [ \underline{t} =^{p} \underline{u} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ≫ [ [ \underline{s} =^{p} \underline{u} ] ˙⇒ [ [ \underline{t} =^{p} \underline{u} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ; [ [ PermuteAntecedents ⊳ [ [ \underline{s} =^{p} \underline{u} ] ˙⇒ [ [ \underline{t} =^{p} \underline{u} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ≫ [ [ \underline{t} =^{p} \underline{u} ] ˙⇒ [ [ \underline{s} =^{p} \underline{u} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[Mendelson3.2(d) →^{tex} “Mendelson3.2(d)”]

[Mendelson3.2(d) →^{pyk} “mendelson three two d”]

SubstitutionMacro

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

[SubstitutionMacro →^{stmt} S′ ⊢ ∀\underline{z}: ∀\underline{c}: ∀\underline{a}: ∀\underline{d}: [ ⌈\underline{a}⌉≡⟨⌈\underline{d}⌉|⌈\underline{z}⌉ := ⌈\underline{c}⌉⟩ ⊢⊢ [ \underline{d} ⊢ \underline{a} ] ] ]

[SubstitutionMacro →^{tex} “SubstitutionMacro”] [SubstitutionMacro →^{pyk} “substitution macro”]

Mendelson3.2(f)Base

[Mendelson3.2(f)Base →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S5′ ≫ [ [ ṫ ˙+ ˙0 ] =^{p} [ ṫ ] ] ] ; [ [ [ EqualSymmetryRule ⊳ [ [ ṫ ˙+ ˙0 ] =^{p} [ ṫ ] ] ] ≫ [ ṫ =^{p} [ ṫ ˙+ ˙0 ] ] ] ; [ [ [ [ SubstitutionMacro @ [ ṫ ] ] @ ˙0 ] ⊳ [ ṫ =^{p} [ ṫ ˙+ ˙0 ] ] ] ≫ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ] ] ] ⌉, p_{0}, c)]

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

[Mendelson3.2(f)Base →^{tex} “Mendelson3.2(f)Base”]

[Mendelson3.2(f)Base →^{pyk} “mendelson three two f base”]

Mendelson3.2(f)Indu

[Mendelson3.2(f)Indu →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S2′ ≫ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒

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

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

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

Mendelson3.2(d)CondRule ⊳ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′

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

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

[Mendelson3.2(f)Indu →^{stmt} S′ ⊢ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ]

[Mendelson3.2(f)Indu →^{tex} “Mendelson3.2(f)Indu”]

[Mendelson3.2(f)Indu →^{pyk} “mendelson three two f induction”]

Mendelson3.2(f)

[Mendelson3.2(f) →^{proof} λc.λx.P(⌈S′ ⊢ [ [ Mendelson3.2(f)Base ≫ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ] ; [ [ Mendelson3.2(f)Indu ≫ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ; [ [ [ InductionMacro ⊳ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ] ⊳ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ≫ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[Mendelson3.2(f) →^{tex} “Mendelson3.2(f)”]