---

Step * of Lemma tl-es-le-before

∀es:EO. ∀e,e':E.  ((e' ∈ tl(≤loc(e))) ⇐⇒ e' ≤loc e  ∧ (¬↑first(e')))
BY
{ ((D 0 THENA Auto)
   THEN CausalInd'
   THEN (D 0 THENA Auto)
   THEN Unfold `es-le-before` 0
   THEN RecUnfold `es-before` 0
   THEN OldAutoSplit) }

1
1. es : EO@i'
2. e : E@i
3. ∀e1:E. ((e1 < e) ⇒ (∀e':E. ((e' ∈ tl(≤loc(e1))) ⇐⇒ e' ≤loc e1  ∧ (¬↑first(e')))))
4. e' : E@i
5. ¬↑first(e)
⊢ (e' ∈ tl((before(pred(e)) @ [pred(e)]) @ [e])) ⇐⇒ e' ≤loc e  ∧ (¬↑first(e'))

---

Latex:


\mforall{}es:EO.  \mforall{}e,e':E.    ((e'  \mmember{}  tl(\mleq{}loc(e)))  \mLeftarrow{}{}\mRightarrow{}  e'  \mleq{}loc  e    \mwedge{}  (\mneg{}\muparrow{}first(e')))


By

((D  0  THENA  Auto)
  THEN  CausalInd'
  THEN  (D  0  THENA  Auto)
  THEN  Unfold  `es-le-before`  0
  THEN  RecUnfold  `es-before`  0
  THEN  OldAutoSplit)

---

Home Index