Step * 1 1 of Lemma wellfounded_functionality_wrt_iff


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])
⊢ WellFnd{i}(T1;x,y.r1[x;y])  WellFnd{i}(T2;x,y.r2[x;y])
BY
(BackThruLemma `wellfounded_functionality_wrt_implies` 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])
⊢ T1 T2 ∈ Type

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])
⊢ ∀x,y:T1.  {r1[x;y]  r2[x;y]}


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{}{}\mRightarrow{}  r2[x;y])
\mvdash{}  WellFnd\{i\}(T1;x,y.r1[x;y])  {}\mRightarrow{}  WellFnd\{i\}(T2;x,y.r2[x;y])


By


Latex:
(BackThruLemma  `wellfounded\_functionality\_wrt\_implies`  THENA  Auto)




Home Index