---

Step * 1 of Lemma es-init-forward


1. Info : Type
2. es : EO+(Info)
3. e' : E
4. e : E@i
5. ∀e1:E. ((e1 < e) ⇒ e' ≤loc e1  ⇒ (es-init(es.e';e1) = e' ∈ E))
6. e' ≤loc e @i
7. ↑first(e)
⊢ es-init(es.e';e) = e' ∈ E
BY
{ ((InstLemma `es-init-elim` [⌈es.e'⌉;⌈e⌉]⋅ THENA Auto)
   THEN RWO "-1" 0
   THEN (InstLemma `eo-forward-first2` [⌈Info⌉;⌈es⌉;⌈e⌉;⌈e'⌉]⋅ THENA Auto)
   THEN RWO "-1" (-3)
   THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  e'  :  E
4.  e  :  E@i
5.  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  e'  \mleq{}loc  e1    {}\mRightarrow{}  (es-init(es.e';e1)  =  e'))
6.  e'  \mleq{}loc  e  @i
7.  \muparrow{}first(e)
\mvdash{}  es-init(es.e';e)  =  e'


By

((InstLemma  `es-init-elim`  [\mkleeneopen{}es.e'\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  (InstLemma  `eo-forward-first2`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "-1"  (-3)
  THEN  Auto)

---

Home Index