---

Step * of Lemma es-closed-open-interval-decomp-mem

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e1,e2,e:E].
  ([e1;e2) = ([e1;e) @ [e;e2)) ∈ (E List)) supposing (e1 ≤loc e  and e ≤loc e2 )
BY
{ (Auto THEN MoveToConcl (-4) THEN CausalInd' THEN Auto THEN D (-1)) }

1
1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e : E
5. e1 ≤loc e 
6. e2 : E@i
7. ∀e3:E. ((e3 < e2) ⇒ e ≤loc e3  ⇒ ([e1;e3) = ([e1;e) @ [e;e3)) ∈ (E List)))
8. (e <loc e2)@i
⊢ [e1;e2) = ([e1;e) @ [e;e2)) ∈ (E List)

2
1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e : E
5. e1 ≤loc e 
6. e2 : E@i
7. ∀e3:E. ((e3 < e2) ⇒ e ≤loc e3  ⇒ ([e1;e3) = ([e1;e) @ [e;e3)) ∈ (E List)))
8. e = e2 ∈ E@i
⊢ [e1;e2) = ([e1;e) @ [e;e2)) ∈ (E List)

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e1,e2,e:E].
    ([e1;e2)  =  ([e1;e)  @  [e;e2)))  supposing  (e1  \mleq{}loc  e    and  e  \mleq{}loc  e2  )


By

(Auto  THEN  MoveToConcl  (-4)  THEN  CausalInd'  THEN  Auto  THEN  D  (-1))

---

Home Index