---

Step * of Lemma hd-es-le-before-is-first

∀[es:EO]. ∀[e:E].  (first(hd(≤loc(e))) ~ tt)
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN CausalInd'
   THEN Auto
   THEN Unfold `es-le-before` 0
   THEN RecUnfold `es-before` 0
   THEN OldAutoSplit
   THEN (InstHyp [⌈pred(e)⌉] 3⋅ THENA Auto)
   THEN Fold `es-le-before` 0) }

1
1. es : EO
2. e : E@i
3. ∀e1:E. ((e1 < e) ⇒ first(hd(≤loc(e1))) = tt)
4. ¬↑first(e)
5. first(hd(≤loc(pred(e)))) = tt
⊢ first(hd(≤loc(pred(e)) @ [e])) = tt

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    (first(hd(\mleq{}loc(e)))  \msim{}  tt)


By

(Auto
  THEN  MoveToConcl  (-1)
  THEN  CausalInd'
  THEN  Auto
  THEN  Unfold  `es-le-before`  0
  THEN  RecUnfold  `es-before`  0
  THEN  OldAutoSplit
  THEN  (InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  Fold  `es-le-before`  0)

---

Home Index