---

Step * 1 2 1 of Lemma assert-eo-forward-first


1. Info : Type
2. eo : EO+(Info)@i'
3. e : E@i
4. e' : E@i
5. first(e') ~ first(e')
6. E ⊆r E
7. ¬(loc(e') = loc(e) ∈ Id)
8. ¬(loc(e') = loc(e) ∈ Id)
9. e' = e ∈ E
⊢ ↑first(e')
BY
{ (All (RWO "eo-forward-loc") THEN Auto THEN D (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  eo  :  EO+(Info)@i'
3.  e  :  E@i
4.  e'  :  E@i
5.  first(e')  \msim{}  first(e')
6.  E  \msubseteq{}r  E
7.  \mneg{}(loc(e')  =  loc(e))
8.  \mneg{}(loc(e')  =  loc(e))
9.  e'  =  e
\mvdash{}  \muparrow{}first(e')


By

---

Latex:
(All  (RWO  "eo-forward-loc")  THEN  Auto  THEN  D  (-2)  THEN  Auto)

---

Home Index