---

Step * of Lemma eo-strict-forward-before

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e,b:E].  before(e) = (b, e) ∈ (E List) supposing (b <loc e)
BY
{ (Auto
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN CausalInd'
   THEN Auto
   THEN (Assert ⌈e ∈ E⌉⋅ THENA (BLemma `member-eo-strict-forward-E` THEN Auto))
   THEN RecUnfold `es-before` 0
   THEN (RWO "eo-strict-forward-first" 0 THENA Auto)
   THEN OldAutoSplit
   THEN Try (Complete ((Assert ⌈False⌉⋅ THEN Auto)))
   THEN (Assert ⌈¬↑first(e)⌉⋅ THENA Auto)) }

1
1. Info : Type
2. es : EO+(Info)
3. e : E@i
4. ∀e1:E. ((e1 < e) ⇒ (∀b:E. ((b <loc e1) ⇒ (before(e1) = (b, e1) ∈ (E List)))))
5. b : E@i
6. (b <loc e)@i
7. e ∈ E
8. loc(e) = loc(b) ∈ Id
9. ¬↑first(e)
⊢ if es-eq(es) pred(e) b then [] else before(pred(e)) @ [pred(e)] fi  = (b, e) ∈ (E List)

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e,b:E].    before(e)  =  (b,  e)  supposing  (b  <loc  e)


By

(Auto
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  CausalInd'
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}e  \mmember{}  E\mkleeneclose{}\mcdot{}  THENA  (BLemma  `member-eo-strict-forward-E`  THEN  Auto))
  THEN  RecUnfold  `es-before`  0
  THEN  (RWO  "eo-strict-forward-first"  0  THENA  Auto)
  THEN  OldAutoSplit
  THEN  Try  (Complete  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  (Assert  \mkleeneopen{}\mneg{}\muparrow{}first(e)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index