---

Step * 1 1 1 1 1 of Lemma es-interval-open-interval


1. es : EO@i'
2. e : E@i
3. ∀e1:E
     ((e1 < e)
     ⇒ (∀e':E. (e' ≤loc e1  ⇒ ([e', e1] = (if e' <loc e1 then [e'] else [] fi  @ (e', e1) @ [e1]) ∈ (E List)))))
4. e' : E@i
5. ¬↑first(e)
6. ¬↑first(e)
7. e' ≤loc pred(e) 
8. (e' <loc e)
⊢ filter(λev.e' ≤loc ev;≤loc(pred(e))) = [e' / filter(λev.e' <loc ev;≤loc(pred(e)))] ∈ (E List)
BY
{ (MoveToConcl (-2)
   THEN (GenConcl ⌈pred(e) = a ∈ E⌉⋅ THENA Auto)
   THEN All Thin
   THEN MoveToConcl (-1)
   THEN Unfold `es-le-before` 0
   THEN CausalInd'
   THEN (D 0 THENA Auto)
   THEN (RecUnfold `es-before` 0 THEN OldAutoSplit)
   THEN Try ((RWO "filter_append_sq" 0 THENA Auto))⋅
   THEN Reduce 0
   THEN RepeatFor 2 (OldAutoSplit)) }

1
1. es : EO@i'
2. e' : E@i
3. a : E@i
4. ∀a1:E
     ((a1 < a)
     ⇒ e' ≤loc a1 
     ⇒ (filter(λev.e' ≤loc ev;before(a1) @ [a1]) = [e' / filter(λev.e' <loc ev;before(a1) @ [a1])] ∈ (E List)))
5. e' ≤loc a @i
6. ¬↑first(a)
7. e' ≤loc a 
8. (e' <loc a)
⊢ (filter(λev.e' ≤loc ev;before(pred(a)) @ [pred(a)]) @ [a])
= [e' / (filter(λev.e' <loc ev;before(pred(a)) @ [pred(a)]) @ [a])]
∈ (E List)

2
1. es : EO@i'
2. e' : E@i
3. a : E@i
4. ∀a1:E
     ((a1 < a)
     ⇒ e' ≤loc a1 
     ⇒ (filter(λev.e' ≤loc ev;before(a1) @ [a1]) = [e' / filter(λev.e' <loc ev;before(a1) @ [a1])] ∈ (E List)))
5. e' ≤loc a @i
6. ¬↑first(a)
7. e' ≤loc a 
8. ¬(e' <loc a)
⊢ (filter(λev.e' ≤loc ev;before(pred(a)) @ [pred(a)]) @ [a])
= [e' / (filter(λev.e' <loc ev;before(pred(a)) @ [pred(a)]) @ [])]
∈ (E List)

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  \mforall{}e1:E
          ((e1  <  e)
          {}\mRightarrow{}  (\mforall{}e':E
                      (e'  \mleq{}loc  e1    {}\mRightarrow{}  ([e',  e1]  =  (if  e'  <loc  e1  then  [e']  else  []  fi    @  (e',  e1)  @  [e1])))))
4.  e'  :  E@i
5.  \mneg{}\muparrow{}first(e)
6.  \mneg{}\muparrow{}first(e)
7.  e'  \mleq{}loc  pred(e) 
8.  (e'  <loc  e)
\mvdash{}  filter(\mlambda{}ev.e'  \mleq{}loc  ev;\mleq{}loc(pred(e)))  =  [e'  /  filter(\mlambda{}ev.e'  <loc  ev;\mleq{}loc(pred(e)))]


By

(MoveToConcl  (-2)
  THEN  (GenConcl  \mkleeneopen{}pred(e)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  MoveToConcl  (-1)
  THEN  Unfold  `es-le-before`  0
  THEN  CausalInd'
  THEN  (D  0  THENA  Auto)
  THEN  (RecUnfold  `es-before`  0  THEN  OldAutoSplit)
  THEN  Try  ((RWO  "filter\_append\_sq"  0  THENA  Auto))\mcdot{}
  THEN  Reduce  0
  THEN  RepeatFor  2  (OldAutoSplit))

---

Home Index