Logiweb codex of HMpeano

Up Help

S′, A1′, A2′, A3′, A4′, A5′, S1′, S2′, S3′, S4′, S5′, S6′, S7′, S8′, S9′, MP′, Gen′, MP′_{h}, Hypothesize, ∗ ⊵ ∗, ∗ ⊵_{h} ∗, HMpeano, Mendelson 3 .2 (a), Mendelson 3 .2 (b), Mendelson 3 .2 (b)^{R}, Mendelson 3 .2 (c), Mendelson 3 .2 (c)^{R}, Mendelson 3 .2 (c)_{h}^{R}, Mendelson 3 .2 (d), Mendelson 3 .2 (d)^{R}, Mendelson 3 .2 (d)_{h}^{R}, Mendelson 3 .2 (f ), Mendelson 3 .2 (f )_{0} , Mendelson 3 .2 (f )_{n}, Mendelson 3 .2 (f )(ṫ), Mendelson 3 .2 (g), Mendelson 3 .2 (g)_{0} , Mendelson 3 .2 (g)_{n}, Mendelson 3 .2 (g)_{h}(ṙ, ṫ), Mendelson 3 .2 (h), Mendelson 3 .2 (h)_{0} , Mendelson 3 .2 (h)_{n}, S6′_{h}, Lemma 1 , Lemma 2 ,

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

MP′_{h}

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

Hypothesize

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

∗ ⊵ ∗

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

∗ ⊵_{h} ∗

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

HMpeano

[HMpeano →^{tex} “HMpeano”] [HMpeano →^{pyk} “hmpeano”]

Mendelson 3 .2 (a)

[Mendelson 3 .2 (a) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: [ [ S5′ ≫ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ] ; [ [ S1′ ≫ [ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ˙⇒ [ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ˙⇒ [ \underline{t} =^{p} \underline{t} ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ˙⇒ [ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ˙⇒ [ \underline{t} =^{p} \underline{t} ] ] ] ] ⊳ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ] ≫ [ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ˙⇒ [ \underline{t} =^{p} \underline{t} ] ] ] ; [ [ [ MP′ ⊳ [ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ˙⇒ [ \underline{t} =^{p} \underline{t} ] ] ] ⊳ [ [ \underline{t} ˙+ ˙0 ] =^{p} \underline{t} ] ] ≫ [ \underline{t} =^{p} \underline{t} ] ] ] ] ] ⌉, p_{0}, c)] [Mendelson 3 .2 (a) →^{stmt} S′ ⊢ ∀\underline{t}: [ \underline{t} =^{p} \underline{t} ] ] [Mendelson 3 .2 (a) →^{tex} “\mathit{Mendelson \; 3.2(a)}”] [Mendelson 3 .2 (a) →^{pyk} “prop three two a”]

Mendelson 3 .2 (b)

[Mendelson 3 .2 (b) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: ∀\underline{r}: [ [ S1′ ≫ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ [ \underline{t} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ] ; [ [ [ Lemma 1 ⊳ [ [ \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} ] ] ] ] ; [ [ Mendelson 3 .2 (a) ≫ [ \underline{t} =^{p} \underline{t} ] ] ; [ [ [ MP′ ⊳ [ [ \underline{t} =^{p} \underline{t} ] ˙⇒ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ] ⊳ [ \underline{t} =^{p} \underline{t} ] ] ≫ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[Mendelson 3 .2 (b) →^{tex} “\mathit{Mendelson \; 3.2(b)}”]

[Mendelson 3 .2 (b) →^{pyk} “prop three two b”]

Mendelson 3 .2 (b)^{R}

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

[Mendelson 3 .2 (b)^{R} →^{stmt} S′ ⊢ ∀\underline{t}: ∀\underline{r}: [ [ \underline{t} =^{p} \underline{r} ] ⊢ [ \underline{r} =^{p} \underline{t} ] ] ]

[Mendelson 3 .2 (b)^{R} →^{tex} “\mathit{Mendelson \; 3.2(b)ˆ R}”]

[Mendelson 3 .2 (b)^{R} →^{pyk} “prop three two b rule”]

Mendelson 3 .2 (c)

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

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

[Mendelson 3 .2 (c) →^{tex} “\mathit{Mendelson \; 3.2(c)}”]

[Mendelson 3 .2 (c) →^{pyk} “prop three two c”]

Mendelson 3 .2 (c)^{R}

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

\underline{t} =^{p} \underline{s} ] ] ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 3 .2 (c)^{R} →^{stmt} S′ ⊢ ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: [ [ \underline{t} =^{p} \underline{r} ] ⊢ [ [ \underline{r} =^{p} \underline{s} ] ⊢ [ \underline{t} =^{p} \underline{s} ] ] ] ]

[Mendelson 3 .2 (c)^{R} →^{tex} “\mathit{Mendelson \; 3.2(c)ˆ R}”]

[Mendelson 3 .2 (c)^{R} →^{pyk} “prop three two c rule”]

Mendelson 3 .2 (c)_{h}^{R}

[Mendelson 3 .2 (c)_{h}^{R} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: [ [ \underline{h} ˙⇒ [ \underline{t} =^{p} \underline{r} ] ] ⊢ [ [ \underline{h} ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ⊢ [ [ Mendelson 3 .2 (c) ≫ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ; [ [ [ Hypothesize ⊳ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ≫ [ \underline{h} ˙⇒ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ] ; [ [ [ [ MP′_{h} ⊳ [ \underline{h} ˙⇒ [ [ \underline{t} =^{p} \underline{r} ] ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{t} =^{p} \underline{r} ] ] ] ≫ [ \underline{h} ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ; [ [ [ MP′_{h} ⊳ [ \underline{h} ˙⇒ [ [ \underline{r} =^{p} \underline{s} ] ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

[Mendelson 3 .2 (c)_{h}^{R} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: [ [ \underline{h} ˙⇒ [ \underline{t} =^{p} \underline{r} ] ] ⊢ [ [ \underline{h} ˙⇒ [

\underline{r} =^{p} \underline{s} ] ] ⊢ [ \underline{h} ˙⇒ [ \underline{t} =^{p} \underline{s} ] ] ] ] ]

[Mendelson 3 .2 (c)_{h}^{R} →^{tex} “\mathit{Mendelson \; 3.2(c) hˆ R}”]

[Mendelson 3 .2 (c)_{h}^{R} →^{pyk} “prop three two c hyp rule”]

Mendelson 3 .2 (d)

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

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

[Mendelson 3 .2 (d) →^{tex} “\mathit{Mendelson \; 3.2(d)}”]

[Mendelson 3 .2 (d) →^{pyk} “prop three two d”]

Mendelson 3 .2 (d)^{R}

[Mendelson 3 .2 (d)^{R} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: [ [ \underline{r} =^{p} \underline{t} ] ⊢ [ [ \underline{s} =^{p} \underline{t} ] ⊢ [ [ Mendelson 3 .2 (d) ≫ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ⊳ [ \underline{r} =^{p} \underline{t} ] ] ≫ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ; [ [ [ MP′ ⊳ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ⊳ [ \underline{s} =^{p} \underline{t} ] ] ≫ [

\underline{r} =^{p} \underline{s} ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[Mendelson 3 .2 (d)^{R} →^{tex} “\mathit{Mendelson \; 3.2(d)ˆ R}”]

[Mendelson 3 .2 (d)^{R} →^{pyk} “prop three two d rule”]

Mendelson 3 .2 (d)_{h}^{R}

[Mendelson 3 .2 (d)_{h}^{R} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: [ [ \underline{h} ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ⊢ [ [ \underline{h} ˙⇒ [ \underline{s} =^{p} \underline{t} ] ] ⊢ [ [ Mendelson 3 .2 (d) ≫ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ; [ [ [ Hypothesize ⊳ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ≫ [ \underline{h} ˙⇒ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ] ; [ [ [ [ MP′_{h} ⊳ [ \underline{h} ˙⇒ [ [ \underline{r} =^{p} \underline{t} ] ˙⇒ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{r} =^{p} \underline{t} ] ] ] ≫ [ \underline{h} ˙⇒ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ; [ [ [ MP′_{h} ⊳ [ \underline{h} ˙⇒ [ [ \underline{s} =^{p} \underline{t} ] ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ⊳ [ \underline{h} ˙⇒ [ \underline{s} =^{p} \underline{t} ] ] ] ≫ [ \underline{h} ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

\underline{s} =^{p} \underline{t} ] ] ⊢ [ \underline{h} ˙⇒ [ \underline{r} =^{p} \underline{s} ] ] ] ] ]

[Mendelson 3 .2 (d)_{h}^{R} →^{tex} “\mathit{Mendelson \; 3.2(d) hˆ R}”]

[Mendelson 3 .2 (d)_{h}^{R} →^{pyk} “prop three two d hyp rule”]

Mendelson 3 .2 (f )

[Mendelson 3 .2 (f ) →^{proof} λc.λx.P(⌈S′ ⊢ [ [ Mendelson 3 .2 (f )_{0} ≫ [ ˙0 =^{p} [ ˙0 ˙+ ˙0 ] ] ] ; [ [ Mendelson 3 .2 (f )_{n} ≫ ˙∀ṫ: [ [ ṫ =^{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)]

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

[Mendelson 3 .2 (f ) →^{tex} “\mathit{Mendelson \; 3.2(f)}”]

[Mendelson 3 .2 (f ) →^{pyk} “prop three two f”]

Mendelson 3 .2 (f )_{0}

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

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

[Mendelson 3 .2 (f )_{0} →^{tex} “\mathit{Mendelson\; 3.2(f) 0}”]

[Mendelson 3 .2 (f )_{0} →^{pyk} “prop three two f base”]

Mendelson 3 .2 (f )_{n}

[Mendelson 3 .2 (f )_{n} →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S6′_{h} ≫ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [

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

[ ṫ′ =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′ ] ] ] ] ; [ [ [ [ Mendelson 3 .2 (d)_{h}^{R} ⊳ [ [ ṫ =^{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)]

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

[Mendelson 3 .2 (f )_{n} →^{tex} “\mathit{Mendelson\; 3.2(f) n}”]

[Mendelson 3 .2 (f )_{n} →^{pyk} “prop three two f ind”]

Mendelson 3 .2 (f )(ṫ)

[Mendelson 3 .2 (f )(ṫ) →^{proof} λc.λx.P(⌈S′ ⊢ [ [ Mendelson 3 .2 (f ) ≫ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ; [ [ [ A4′ @ [ ṫ ] ] ≫ [ [ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ˙⇒ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ; [ [ [ MP′ ⊳ [ [ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ˙⇒ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ⊳ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ≫ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[Mendelson 3 .2 (f )(ṫ) →^{tex} “\mathit{Mendelson \; 3.2(f)(\dot{t})}”]

[Mendelson 3 .2 (f )(ṫ) →^{pyk} “prop three two f t”]

Mendelson 3 .2 (g)

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

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

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

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

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

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

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

[Mendelson 3 .2 (g) →^{tex} “\mathit{Mendelson \; 3.2(g)}”]

[Mendelson 3 .2 (g) →^{pyk} “prop three two g”]