---

Step * 1 1 1 of Lemma iseg-es-interval

.....assertion..... 
1. es : EO
2. L : E List
3. e1 : E
4. e2 : E
5. L ≤ filter(λev.e1 ≤loc ev;≤loc(e2))
6. L_3 : E List
7. L_3 ≤ ≤loc(e2)
8. L = filter(λev.e1 ≤loc ev;L_3) ∈ (E List)
9. ¬↑null(filter(λev.e1 ≤loc ev;L_3))
10. x : E
11. (x ∈ L_3)
12. e1 ≤loc x 
13. ¬↑null(L_3)
⊢ e1 ≤loc last(L_3) 
BY
{ (RepeatFor 2 (D (-3))
   THEN (Decide ⌈i = (||L_3|| - 1) ∈ ℤ⌉⋅ THENA Auto)
   THEN Try (((RWO "-1" (-4) THENA Auto) THEN Fold `last` (-4) THEN Auto))
   THEN (InstLemma `es-le-before-ordered` [⌈es⌉;⌈e2⌉]⋅ THENA Auto)
   THEN (FLemma `iseg-l-ordered` [-1;-11] THENA Auto)
   THEN InstLemma `l-ordered-inst` [⌈E⌉;⌈L_3⌉;⌈λ2x.λ2y.(x <loc y)⌉;⌈||L_3|| - 1⌉;⌈i⌉]⋅
   THEN Auto
   THEN Reduce (-1)
   THEN Fold `last` (-1)
   THEN (RevHypSubst (-7) (-1) THEN Auto)
   THEN (FLemma `es-locl_transitivity1` [-6;-1] THEN Auto)
   THEN UnfoldTopAb 0
   THEN OrLeft
   THEN Auto) }

---

Latex:


.....assertion..... 
1.  es  :  EO
2.  L  :  E  List
3.  e1  :  E
4.  e2  :  E
5.  L  \mleq{}  filter(\mlambda{}ev.e1  \mleq{}loc  ev;\mleq{}loc(e2))
6.  L$_{3}$  :  E  List
7.  L$_{3}$  \mleq{}  \mleq{}loc(e2)
8.  L  =  filter(\mlambda{}ev.e1  \mleq{}loc  ev;L$_{3}$)
9.  \mneg{}\muparrow{}null(filter(\mlambda{}ev.e1  \mleq{}loc  ev;L$_{3}$))
10.  x  :  E
11.  (x  \mmember{}  L$_{3}$)
12.  e1  \mleq{}loc  x 
13.  \mneg{}\muparrow{}null(L$_{3}$)
\mvdash{}  e1  \mleq{}loc  last(L$_{3}$) 


By

(RepeatFor  2  (D  (-3))
  THEN  (Decide  \mkleeneopen{}i  =  (||L$_{3}$||  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (((RWO  "-1"  (-4)  THENA  Auto)  THEN  Fold  `last`  (-4)  THEN  Auto))
  THEN  (InstLemma  `es-le-before-ordered`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (FLemma  `iseg-l-ordered`  [-1;-11]  THENA  Auto)
  THEN  InstLemma  `l-ordered-inst`  [\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}L$_{3}$\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.\mlambda{}\msubtwo{}y.(x  <loc  y)\mkleeneclose{};\mkleeneopen{}||L$\mbackslash{}f\000Cf5f{3}$||  -  1\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Reduce  (-1)
  THEN  Fold  `last`  (-1)
  THEN  (RevHypSubst  (-7)  (-1)  THEN  Auto)
  THEN  (FLemma  `es-locl\_transitivity1`  [-6;-1]  THEN  Auto)
  THEN  UnfoldTopAb  0
  THEN  OrLeft
  THEN  Auto)

---

Home Index