---

Step * 1 of Lemma llex-linear


1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀a,b:A.  (<[a;b] ∨ (a = b ∈ A) ∨ <[b;a])
⊢ ∀L2:A List. (([] llex(A;a,b.<[a;b]) L2) ∨ ([] = L2 ∈ (A List)) ∨ (L2 llex(A;a,b.<[a;b]) []))
BY
{ xxx(Auto THEN (InstLemma `nil-llex` [⌜A⌝;⌜<⌝;⌜L2⌝]⋅ THENM D (-1)⋅) THEN Auto THEN Sel 2 (D 0) THEN Auto)xxx }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [<]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}a,b:A.    (<[a;b]  \mvee{}  (a  =  b)  \mvee{}  <[b;a])
\mvdash{}  \mforall{}L2:A  List.  (([]  llex(A;a,b.<[a;b])  L2)  \mvee{}  ([]  =  L2)  \mvee{}  (L2  llex(A;a,b.<[a;b])  []))


By

---

Latex:
xxx(Auto
        THEN  (InstLemma  `nil-llex`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}<\mkleeneclose{};\mkleeneopen{}L2\mkleeneclose{}]\mcdot{}  THENM  D  (-1)\mcdot{})
        THEN  Auto
        THEN  Sel  2  (D  0)
        THEN  Auto)xxx

---

Home Index