---

Step * 2 1 of Lemma llex-linear


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

---

Latex:

---

Latex:

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


By

---

Latex:
(Auto  THEN  (InstLemma  `nil-llex`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}<\mkleeneclose{};\mkleeneopen{}[u  /  v]\mkleeneclose{}]\mcdot{}  THENM  D  (-1)\mcdot{})  THEN  Auto)\mcdot{}

---

Home Index