Logiweb codex of rapport

Up Help

rapport, , LEMMA3.2(a), LEMMA3.2(b), LEMMA3.2(c), LEMMA3.2(d), LEMMA3.2(f), LEMMA3.2(f)base, LEMMA3.2(f)induction, LEMMA3.2(g), LEMMA3.2(g)base, LEMMA3.2(g)induction, LEMMA3.2(h), LEMMA3.2(h)base, LEMMA3.2(h)induction, IMV, CImp, TImp,

rapport

[rapport →^{pyk} “rapport”]

[→^{tex} “”]

[ →^{pyk} “blank space”]

LEMMA3.2(a)

[LEMMA3.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)]

[LEMMA3.2(a) →^{stmt} S′ ⊢ ∀\underline{t}: [ \underline{t} =^{p} \underline{t} ] ]

[LEMMA3.2(a) →^{tex} “LEMMA 3.2(a)”]

[LEMMA3.2(a) →^{pyk} “mendelson lemma three two a”]

LEMMA3.2(b)

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

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

[LEMMA3.2(b) →^{tex} “LEMMA 3.2(b)”]

[LEMMA3.2(b) →^{pyk} “mendelson lemma three two b”]

LEMMA3.2(c)

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

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

[LEMMA3.2(c) →^{tex} “LEMMA 3.2(c)”]

[LEMMA3.2(c) →^{pyk} “mendelson lemma three two c”]

LEMMA3.2(d)

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

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

[LEMMA3.2(d) →^{tex} “LEMMA 3.2(d)”]

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

LEMMA3.2(f)

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

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

LEMMA3.2(f)induction ≫ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ; [ [ [ Gen′ ⊳ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ≫ ˙∀ṫ: [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ; [ [ [ [ MP′ ⊳ [ [ ˙∀ṫ: [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ˙⇒ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ⊳ ˙∀ṫ: [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ≫ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ; [ [ [ A4′ @ [ ṫ ] ] ≫ [ [ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ˙⇒ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ; [ [ [ MP′ ⊳ [ [ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ˙⇒ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ⊳ ˙∀ṫ: [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ≫ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ] ] ] ] ] ] ] ] ⌉, p_{0}, c)]

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

[LEMMA3.2(f) →^{tex} “LEMMA 3.2(f)”]

[LEMMA3.2(f) →^{pyk} “mendelson lemma three two f”]

LEMMA3.2(f)base

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

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

[LEMMA3.2(f)base →^{tex} “LEMMA 3.2(f) base”]

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

LEMMA3.2(f)induction

[LEMMA3.2(f)induction →^{proof} λc.λx.P(⌈S′ ⊢ [ [ S6′ ≫ [ [ ˙0 ˙+ [ ṫ′ ] ] =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′ ] ] ] ; [ [ S2′ ≫ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′ ] ] ] ] ; [ [ LEMMA3.2(d) ≫ [ [ ṫ′ =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′ ] ] ˙⇒ [ [ [ ˙0 ˙+ [ ṫ′ ] ] =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′ ] ] ˙⇒ [ ṫ′ =^{p} [ ˙0 ˙+ [ ṫ′ ] ] ] ] ] ] ; [ [ [ [ TImp ⊳ [ [ ṫ =^{p} [ ˙0 ˙+ [ ṫ ] ] ] ˙⇒ [ ṫ′ =^{p} [ [ ˙0 ˙+ [ ṫ ] ] ′ ] ] ] ] ⊳ [ [ ṫ′ =^{p} [ [ ˙0 ˙+ [ ṫ ] ]

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

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

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

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

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

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

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

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

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

[LEMMA3.2(f)induction →^{tex} “LEMMA 3.2(f) induction”]

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

LEMMA3.2(g)

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

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

] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ˙⇒ [ [ ṙ′ ˙+ [ ṫ′ ] ] =^{p} [ [ ṙ ˙+ [ ṫ′ ] ] ′ ] ] ] ] ˙⇒ ˙∀ṫ: [ [ ṙ′ ˙+ [ ṫ ] ] =^{p} [ [ ṙ ˙+ [ ṫ ] ] ′ ] ] ] ] ; [ [ LEMMA3.2(g)induction ≫ [ [ [

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

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

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

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

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

[LEMMA3.2(g) →^{tex} “LEMMA 3.2(g)”]

[LEMMA3.2(g) →^{pyk} “mendelson lemma three two g”]