---

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


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)
14. e1 ≤loc last(L_3) 
⊢ filter(λev.e1 ≤loc ev;L_3) = filter(λev.e1 ≤loc ev;≤loc(last(filter(λev.e1 ≤loc ev;L_3)))) ∈ (E List)
BY
{ ((RWO "last-filter1" 0 THENA Auto)
   THEN Assert ⌈L_3 = ≤loc(last(L_3)) ∈ (E List)⌉⋅
   THEN Auto
   THEN (InstLemma `list_decomp_last` [⌈E⌉;⌈L_3⌉]⋅ THENA Auto)
   THEN ExRepD
   THEN MoveToHyp 0 (-10)
   THEN (HypSubst (-2) (-1) THENA Auto)
   THEN (FLemma `iseg-es-le-before-is-before` [-1] THENA Auto)
   THEN (HypSubst (-1) (-3) THENA Auto)
   THEN Fold `es-le-before` (-3)
   THEN Auto) }

---

Latex:



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}$)
14.  e1  \mleq{}loc  last(L$_{3}$) 
\mvdash{}  filter(\mlambda{}ev.e1  \mleq{}loc  ev;L$_{3}$)  =  filter(\mlambda{}ev.e1  \mleq{}loc  ev;\mleq{}loc(last(filter(\mlambda{}ev.e1\000C  \mleq{}loc  ev;L$_{3}$))))


By

((RWO  "last-filter1"  0  THENA  Auto)
  THEN  Assert  \mkleeneopen{}L$_{3}$  =  \mleq{}loc(last(L$_{3}$))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `list\_decomp\_last`  [\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}L$_{3}$\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  MoveToHyp  0  (-10)
  THEN  (HypSubst  (-2)  (-1)  THENA  Auto)
  THEN  (FLemma  `iseg-es-le-before-is-before`  [-1]  THENA  Auto)
  THEN  (HypSubst  (-1)  (-3)  THENA  Auto)
  THEN  Fold  `es-le-before`  (-3)
  THEN  Auto)

---

Home Index