---

Step * of Lemma hd-es-le-before

∀es:EO. ∀e,fst:E.  ((↑first(fst)) ⇒ fst ≤loc e  ⇒ (hd(≤loc(e)) = fst ∈ E))
BY
{ ((D 0 THENA Auto)
   THEN CausalInd'
   THEN 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) ⇒ (∀fst:E. ((↑first(fst)) ⇒ fst ≤loc e1  ⇒ (hd(≤loc(e1)) = fst ∈ E))))
4. fst : E@i
5. ↑first(fst)@i
6. fst ≤loc e @i
7. ¬↑first(e)
⊢ hd((before(pred(e)) @ [pred(e)]) @ [e]) = fst ∈ E

---

Latex:


\mforall{}es:EO.  \mforall{}e,fst:E.    ((\muparrow{}first(fst))  {}\mRightarrow{}  fst  \mleq{}loc  e    {}\mRightarrow{}  (hd(\mleq{}loc(e))  =  fst))


By

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

---

Home Index