---

Step * of Lemma wellfounded_functionality_wrt_implies

∀[T1,T2:Type]. ∀[r1:T1 ⟶ T1 ⟶ ℙ]. ∀[r2:T2 ⟶ T2 ⟶ ℙ].
  (∀x,y:T1.  {r1[x;y] ⇐ r2[x;y]}) ⇒ {WellFnd{i}(T1;x,y.r1[x;y]) ⇒ WellFnd{i}(T2;x,y.r2[x;y])} 
  supposing T1 = T2 ∈ Type
BY
{ ((Unfolds ``wellfounded guard`` 0 THEN UnivCD) THENA Auto) }

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

---

Latex:

---

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[r1:T1  {}\mrightarrow{}  T1  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[r2:T2  {}\mrightarrow{}  T2  {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}x,y:T1.    \{r1[x;y]  \mLeftarrow{}{}  r2[x;y]\})  {}\mRightarrow{}  \{WellFnd\{i\}(T1;x,y.r1[x;y])  {}\mRightarrow{}  WellFnd\{i\}(T2;x,y.r2[x;y])\} 
    supposing  T1  =  T2


By

---

Latex:
((Unfolds  ``wellfounded  guard``  0  THEN  UnivCD)  THENA  Auto)

---

Home Index