---

Step * 1 of Lemma order-type-less-maximal


1. x : WFTRO{i:l}()
⊢ x order-type-less() <WFO{i:l}(), order-type-less(), DCC-order-type()>
BY
{ (RepeatFor 3 (D (-1)) THEN RepUR ``order-type-less`` 0 THEN RenameVar `<' 2 THEN All Reduce THEN Unfold `WFO` 0) }

1
1. A : Type
2. < : A ⟶ A ⟶ ℙ
3. x3 : DCC(A;<)
4. x4 : Trans(A;x,y.x < y)
⊢ ∃f:A ⟶ (A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<))
   ∃b:A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<)
    (order-preserving(A;A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<);a1,a2.a1 < a2;b1,b2.let A,R,wf1 = b1 in 
    let B,S,wf2 = b2 in 
    ∃f:A ⟶ B. ∃b:B. (order-preserving(A;B;a1,a2.a1 R a2;b1,b2.b1 S b2;f) ∧ (∀a:A. ((f a) S b)));f)
    ∧ (∀a:A
         let A,R,wf1 = f a in 
         let B,S,wf2 = b in 
         ∃f:A ⟶ B. ∃b:B. (order-preserving(A;B;a1,a2.a1 R a2;b1,b2.b1 S b2;f) ∧ (∀a:A. ((f a) S b)))))

---

Latex:

---

Latex:

1.  x  :  WFTRO\{i:l\}()
\mvdash{}  x  order-type-less()  <WFO\{i:l\}(),  order-type-less(),  DCC-order-type()>


By

---

Latex:
(RepeatFor  3  (D  (-1))
  THEN  RepUR  ``order-type-less``  0
  THEN  RenameVar  `<'  2
  THEN  All  Reduce
  THEN  Unfold  `WFO`  0)

---

Home Index