---

Step * of Lemma llex-le-lin-order

∀[A:Type]. ∀[<:A ⟶ A ⟶ ℙ].
  ((∀a:A. (¬<[a;a]))
  ⇒ Trans(A;a,b.<[a;b])
  ⇒ (∀a,b:A.  (<[a;b] ∨ (a = b ∈ A) ∨ <[b;a]))
  ⇒ Linorder(A List;as,bs.as llex-le(A;a,b.<[a;b]) bs))
BY
{ (InstLemma `llex-le-order` [] THEN RepeatFor 4 ((ParallelLast' THENA Auto)) THEN Auto THEN D 0 THEN Try (Trivial)) }

1
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀a:A. (¬<[a;a])
4. Trans(A;a,b.<[a;b])
5. Order(A List;as,bs.as llex-le(A;a,b.<[a;b]) bs)
6. ∀a,b:A.  (<[a;b] ∨ (a = b ∈ A) ∨ <[b;a])
⊢ Connex(A List;as,bs.as llex-le(A;a,b.<[a;b]) bs)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[<:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}a:A.  (\mneg{}<[a;a]))
    {}\mRightarrow{}  Trans(A;a,b.<[a;b])
    {}\mRightarrow{}  (\mforall{}a,b:A.    (<[a;b]  \mvee{}  (a  =  b)  \mvee{}  <[b;a]))
    {}\mRightarrow{}  Linorder(A  List;as,bs.as  llex-le(A;a,b.<[a;b])  bs))


By

---

Latex:
(InstLemma  `llex-le-order`  []
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  D  0
  THEN  Try  (Trivial))

---

Home Index