---

Step * of Lemma assert-eo-forward-first

∀[Info:Type]. ∀eo:EO+(Info). ∀e:E. ∀e':E.  uiff(↑first(e');(e' = e ∈ E) ∨ ((¬(loc(e') = loc(e) ∈ Id)) ∧ (↑first(e'))))
BY
{ (InstLemma `eo-forward-first` []
   THEN RepeatFor 4 ((ParallelLast THEN Thin (-3)))
   THEN HypSubst' (-1) 0
   THEN (Assert E ⊆r E BY
               (BLemma `eo-forward-E-subtype` THEN Auto))) }

1
1. [Info] : Type
2. eo : EO+(Info)@i'
3. e : E@i
4. e' : E@i
5. first(e') ~ if loc(e') = loc(e) then e' = e else first(e') fi 
6. E ⊆r E
⊢ uiff(↑if loc(e') = loc(e) then e' = e else first(e') fi ;(e' = e ∈ E) ∨ ((¬(loc(e') = loc(e) ∈ Id)) ∧ (↑first(e'))))

---

Latex:


\mforall{}[Info:Type]
    \mforall{}eo:EO+(Info).  \mforall{}e:E.  \mforall{}e':E.    uiff(\muparrow{}first(e');(e'  =  e)  \mvee{}  ((\mneg{}(loc(e')  =  loc(e)))  \mwedge{}  (\muparrow{}first(e'))))


By

(InstLemma  `eo-forward-first`  []
  THEN  RepeatFor  4  ((ParallelLast  THEN  Thin  (-3)))
  THEN  HypSubst'  (-1)  0
  THEN  (Assert  E  \msubseteq{}r  E  BY
                          (BLemma  `eo-forward-E-subtype`  THEN  Auto)))

---

Home Index