---

Step * of Lemma es-init-forward

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e',e:E].  es-init(es.e';e) = e' ∈ E supposing e' ≤loc e 
BY
{ ((UnivCD THENA Auto) THEN MoveToConcl (-2) THEN CausalInd' THEN Auto THEN (Decide ↑first(e) THENA Auto)) }

1
1. Info : Type
2. es : EO+(Info)
3. e' : E
4. e : E@i
5. ∀e1:E. ((e1 < e) ⇒ e' ≤loc e1  ⇒ (es-init(es.e';e1) = e' ∈ E))
6. e' ≤loc e @i
7. ↑first(e)
⊢ es-init(es.e';e) = e' ∈ E

2
1. Info : Type
2. es : EO+(Info)
3. e' : E
4. e : E@i
5. ∀e1:E. ((e1 < e) ⇒ e' ≤loc e1  ⇒ (es-init(es.e';e1) = e' ∈ E))
6. e' ≤loc e @i
7. ¬↑first(e)
⊢ es-init(es.e';e) = e' ∈ E

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e',e:E].    es-init(es.e';e)  =  e'  supposing  e'  \mleq{}loc  e 


By

((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  CausalInd'
  THEN  Auto
  THEN  (Decide  \muparrow{}first(e)  THENA  Auto))

---

Home Index