---

Step * of Lemma iseg-es-interval

∀[es:EO]. ∀[L:E List]. ∀[e1,e2:E].  (L = [e1, last(L)] ∈ (E List)) supposing ((¬↑null(L)) and L ≤ [e1, e2])
BY
{ (Auto
   THEN All(Unfold `es-interval`)
   THEN (FLemma `iseg_filter` [-2] THENA Auto)
   THEN All(Fold `es-le-before`)
   THEN ExRepD
   THEN (RWO "-1" 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. ¬↑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)

---

Latex:


\mforall{}[es:EO].  \mforall{}[L:E  List].  \mforall{}[e1,e2:E].    (L  =  [e1,  last(L)])  supposing  ((\mneg{}\muparrow{}null(L))  and  L  \mleq{}  [e1,  e2])


By

(Auto
  THEN  All(Unfold  `es-interval`)
  THEN  (FLemma  `iseg\_filter`  [-2]  THENA  Auto)
  THEN  All(Fold  `es-le-before`)
  THEN  ExRepD
  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index