---

Step * 1 of Lemma es-interval-less


1. es : EO
2. e : E
3. e' : E
4. (e <loc e')
⊢ (filter(λev.e ≤loc ev;before(e')) @ filter(λev.e ≤loc ev;[e']))
= ((filter(λev.e ≤loc ev;before(pred(e'))) @ filter(λev.e ≤loc ev;[pred(e')])) @ [e'])
∈ (E List)
BY
{ (((RW (AddrC [2] (RecUnfoldC `es-before`)) 0) THEN SplitOnConclITE) THENA Auto) }

1
.....truecase..... 
1. es : EO
2. e : E
3. e' : E
4. (e <loc e')
5. ↑first(e')
⊢ (filter(λev.e ≤loc ev;[]) @ filter(λev.e ≤loc ev;[e']))
= ((filter(λev.e ≤loc ev;before(pred(e'))) @ filter(λev.e ≤loc ev;[pred(e')])) @ [e'])
∈ (E List)

2
.....falsecase..... 
1. es : EO
2. e : E
3. e' : E
4. (e <loc e')
5. ¬↑first(e')
⊢ (filter(λev.e ≤loc ev;before(pred(e')) @ [pred(e')]) @ filter(λev.e ≤loc ev;[e']))
= ((filter(λev.e ≤loc ev;before(pred(e'))) @ filter(λev.e ≤loc ev;[pred(e')])) @ [e'])
∈ (E List)

---

Latex:



1.  es  :  EO
2.  e  :  E
3.  e'  :  E
4.  (e  <loc  e')
\mvdash{}  (filter(\mlambda{}ev.e  \mleq{}loc  ev;before(e'))  @  filter(\mlambda{}ev.e  \mleq{}loc  ev;[e']))
=  ((filter(\mlambda{}ev.e  \mleq{}loc  ev;before(pred(e')))  @  filter(\mlambda{}ev.e  \mleq{}loc  ev;[pred(e')]))  @  [e'])


By

(((RW  (AddrC  [2]  (RecUnfoldC  `es-before`))  0)  THEN  SplitOnConclITE)  THENA  Auto)

---

Home Index