---

Step * 1 1 of Lemma eo-strict-forward-before


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)
10. ↑(es-eq(es) pred(e) b)
⊢ [] = (b, e) ∈ (E List)
BY
{ ((Assert ⌈(b, e) ~ []⌉⋅ THENM (HypSubst' (-1) 0 THEN Auto))
   THEN (BLemma `es-open-interval-nil` THENA Auto)
   THEN OrRight
   THEN Auto
   THEN (BLemma `es-le_weakening_eq` THENA Auto)
   THEN (RWO "assert-es-eq-E" 0 THENA Auto)
   THEN RepUR ``es-eq-E eqof`` 0
   THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  e  :  E@i
4.  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  (\mforall{}b:E.  ((b  <loc  e1)  {}\mRightarrow{}  (before(e1)  =  (b,  e1)))))
5.  b  :  E@i
6.  (b  <loc  e)@i
7.  e  \mmember{}  E
8.  loc(e)  =  loc(b)
9.  \mneg{}\muparrow{}first(e)
10.  \muparrow{}(es-eq(es)  pred(e)  b)
\mvdash{}  []  =  (b,  e)


By

((Assert  \mkleeneopen{}(b,  e)  \msim{}  []\mkleeneclose{}\mcdot{}  THENM  (HypSubst'  (-1)  0  THEN  Auto))
  THEN  (BLemma  `es-open-interval-nil`  THENA  Auto)
  THEN  OrRight
  THEN  Auto
  THEN  (BLemma  `es-le\_weakening\_eq`  THENA  Auto)
  THEN  (RWO  "assert-es-eq-E"  0  THENA  Auto)
  THEN  RepUR  ``es-eq-E  eqof``  0
  THEN  Auto)

---

Home Index