---

Step * 1 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. 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)
BY
{ ((Assert ⌈¬↑null(L_3)⌉⋅ THENA (FLemma `member_null` [-2] THEN Auto)) THEN Assert ⌈e1 ≤loc last(L_3) ⌉⋅) }

1
.....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) 

2
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)

---

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 
\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

((Assert  \mkleeneopen{}\mneg{}\muparrow{}null(L$_{3}$)\mkleeneclose{}\mcdot{}  THENA  (FLemma  `member\_null`  [-2]  THEN  Auto))
  THEN  Assert  \mkleeneopen{}e1  \mleq{}loc  last(L$_{3}$)  \mkleeneclose{}\mcdot{}
  )

---

Home Index