---

Step * 2 2 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))
7. u1 : A
8. v1 : A List
9. ([u / v] llex(A;a,b.<[a;b]) v1) ∨ ([u / v] = v1 ∈ (A List)) ∨ (v1 llex(A;a,b.<[a;b]) [u / v])
10. u = u1 ∈ A
⊢ ([u / v] llex(A;a,b.<[a;b]) [u1 / v1]) ∨ ([u / v] = [u1 / v1] ∈ (A List)) ∨ ([u1 / v1] llex(A;a,b.<[a;b]) [u / v])
BY
{ ((Thin (-2) THEN (InstHyp [⌜v1⌝] 6⋅ THENA Auto))
   THEN RepeatFor 2 (ParallelLast)
   THEN Try (ParallelLast)
   THEN RepUR ``llex`` (-1)
   THEN RepUR ``llex`` 0
   THEN (D (-1)⋅ THENL [xxxOrLeftxxx; xxxOrRightxxx])
   THEN Auto
   THEN Try ((CaseNat 0 `i' THEN Reduce 0 THEN Auto THEN RWO "select_cons_tl" 0 THEN Auto))
   THEN ExRepD
   THEN With ⌜i + 1⌝ (D 0)⋅
   THEN Auto
   THEN (Try ((CaseNat 0 `j' THEN Reduce 0 THEN Auto THEN RWO "select_cons_tl" 0 THEN Auto))
         THEN (RWO "select_cons_tl" 0 THEN Auto)
         THEN EqCD
         THEN Auto
         THEN RWO "select_cons_tl" 0
         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))
7.  u1  :  A
8.  v1  :  A  List
9.  ([u  /  v]  llex(A;a,b.<[a;b])  v1)  \mvee{}  ([u  /  v]  =  v1)  \mvee{}  (v1  llex(A;a,b.<[a;b])  [u  /  v])
10.  u  =  u1
\mvdash{}  ([u  /  v]  llex(A;a,b.<[a;b])  [u1  /  v1])
\mvee{}  ([u  /  v]  =  [u1  /  v1])
\mvee{}  ([u1  /  v1]  llex(A;a,b.<[a;b])  [u  /  v])


By

---

Latex:
((Thin  (-2)  THEN  (InstHyp  [\mkleeneopen{}v1\mkleeneclose{}]  6\mcdot{}  THENA  Auto))
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Try  (ParallelLast)
  THEN  RepUR  ``llex``  (-1)
  THEN  RepUR  ``llex``  0
  THEN  (D  (-1)\mcdot{}  THENL  [xxxOrLeftxxx;  xxxOrRightxxx])
  THEN  Auto
  THEN  Try  ((CaseNat  0  `i'  THEN  Reduce  0  THEN  Auto  THEN  RWO  "select\_cons\_tl"  0  THEN  Auto))
  THEN  ExRepD
  THEN  With  \mkleeneopen{}i  +  1\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (Try  ((CaseNat  0  `j'  THEN  Reduce  0  THEN  Auto  THEN  RWO  "select\_cons\_tl"  0  THEN  Auto))
              THEN  (RWO  "select\_cons\_tl"  0  THEN  Auto)
              THEN  EqCD
              THEN  Auto
              THEN  RWO  "select\_cons\_tl"  0
              THEN  Auto)\mcdot{})

---

Home Index