---

Step * 1 of Lemma wellfounded_functionality_wrt_implies


1. [T1] : Type
2. [T2] : Type
3. [r1] : T1 ⟶ T1 ⟶ ℙ
4. [r2] : T2 ⟶ T2 ⟶ ℙ
5. T1 = T2 ∈ Type
6. ∀x,y:T1.  (r1[x;y] ⇐ r2[x;y])
7. ∀[P:T1 ⟶ ℙ]. ((∀j:T1. ((∀k:T1. (r1[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:T1. P[n]})
8. [P] : T2 ⟶ ℙ
9. ∀j:T2. ((∀k:T2. (r2[k;j] ⇒ P[k])) ⇒ P[j])
⊢ ∀n:T2. P[n]
BY
{ SubstClause ⌜∀n:T1. P[n]⌝ 0 }

1
.....equality..... 
1. T1 : Type
2. T2 : Type
3. r1 : T1 ⟶ T1 ⟶ ℙ
4. r2 : T2 ⟶ T2 ⟶ ℙ
5. T1 = T2 ∈ Type
6. ∀x,y:T1.  (r1[x;y] ⇐ r2[x;y])
7. ∀[P:T1 ⟶ ℙ]. ((∀j:T1. ((∀k:T1. (r1[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:T1. P[n]})
8. P : T2 ⟶ ℙ
9. ∀j:T2. ((∀k:T2. (r2[k;j] ⇒ P[k])) ⇒ P[j])
⊢ (∀n:T2. P[n]) = (∀n:T1. P[n]) ∈ ℙ{[1 | i 0]}

2
1. [T1] : Type
2. [T2] : Type
3. [r1] : T1 ⟶ T1 ⟶ ℙ
4. [r2] : T2 ⟶ T2 ⟶ ℙ
5. T1 = T2 ∈ Type
6. ∀x,y:T1.  (r1[x;y] ⇐ r2[x;y])
7. ∀[P:T1 ⟶ ℙ]. ((∀j:T1. ((∀k:T1. (r1[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:T1. P[n]})
8. [P] : T2 ⟶ ℙ
9. ∀j:T2. ((∀k:T2. (r2[k;j] ⇒ P[k])) ⇒ P[j])
⊢ ∀n:T1. P[n]

---

Latex:

---

Latex:

1.  [T1]  :  Type
2.  [T2]  :  Type
3.  [r1]  :  T1  {}\mrightarrow{}  T1  {}\mrightarrow{}  \mBbbP{}
4.  [r2]  :  T2  {}\mrightarrow{}  T2  {}\mrightarrow{}  \mBbbP{}
5.  T1  =  T2
6.  \mforall{}x,y:T1.    (r1[x;y]  \mLeftarrow{}{}  r2[x;y])
7.  \mforall{}[P:T1  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}j:T1.  ((\mforall{}k:T1.  (r1[k;j]  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j]))  {}\mRightarrow{}  \{\mforall{}n:T1.  P[n]\})
8.  [P]  :  T2  {}\mrightarrow{}  \mBbbP{}
9.  \mforall{}j:T2.  ((\mforall{}k:T2.  (r2[k;j]  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j])
\mvdash{}  \mforall{}n:T2.  P[n]


By

---

Latex:
SubstClause  \mkleeneopen{}\mforall{}n:T1.  P[n]\mkleeneclose{}  0

---

Home Index