---

Step * 1 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. ¬↑null(L)
7. L_3 : E List
8. L_3 ≤ ≤loc(e2)
9. L = filter(λev.e1 ≤loc ev;L_3) ∈ (E List)
⊢ 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 "-1" (-4) THENA Auto)
   THEN Duplicate (-1)
   THEN (RWO "null-filter2" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN (RWO "l_all_not" (-1) THENA Auto)
   THEN (RWO "assert-bl-exists<" (-1) THENA Auto)
   THEN (RWO "not-not-assert" (-1) THENA Auto)
   THEN (RWO "assert-bl-exists" (-1) THENA Auto)
   THEN (RWO "l_exists_iff" (-1) THENA Auto)
   THEN ExRepD
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN skip{(RWO "last-filter1" 0 THENA Auto)}) }

1
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 
⊢ filter(λev.e1 ≤loc ev;L_3) = filter(λev.e1 ≤loc ev;≤loc(last(filter(λev.e1 ≤loc ev;L_3)))) ∈ (E List)

---

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.  \mneg{}\muparrow{}null(L)
7.  L$_{3}$  :  E  List
8.  L$_{3}$  \mleq{}  \mleq{}loc(e2)
9.  L  =  filter(\mlambda{}ev.e1  \mleq{}loc  ev;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  "-1"  (-4)  THENA  Auto)
  THEN  Duplicate  (-1)
  THEN  (RWO  "null-filter2"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  (RWO  "l\_all\_not"  (-1)  THENA  Auto)
  THEN  (RWO  "assert-bl-exists<"  (-1)  THENA  Auto)
  THEN  (RWO  "not-not-assert"  (-1)  THENA  Auto)
  THEN  (RWO  "assert-bl-exists"  (-1)  THENA  Auto)
  THEN  (RWO  "l\_exists\_iff"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  skip\{(RWO  "last-filter1"  0  THENA  Auto)\})

---

Home Index