---

Step * 1 1 1 1 1 of Lemma global-eo-first


1. L : (Id × Top) List
2. e : ℕ||L||
⊢ first(e) = (∀x∈upto(e).¬bfst(L[x]) = fst(L[e]))_b
BY
{ ((Assert e ∈ E BY
          (BLemma `global-eo-E` THEN Auto))
   THEN (Assert pred(e) ∈ E BY
               ((InstLemma `es-pred-wf-base` [⌜global-eo(L)⌝;⌜e⌝]⋅ THENA Auto)
                THEN (RWO "global-eo-base-E" (-1) THENA Auto)
                THEN (RWO "global-eo-E-sq" 0 THENA Auto)
                THEN Auto))
   ) }

1
1. L : (Id × Top) List
2. e : ℕ||L||
3. e ∈ E
4. pred(e) ∈ E
⊢ first(e) = (∀x∈upto(e).¬bfst(L[x]) = fst(L[e]))_b

---

Latex:

---

Latex:

1.  L  :  (Id  \mtimes{}  Top)  List
2.  e  :  \mBbbN{}||L||
\mvdash{}  first(e)  =  (\mforall{}x\mmember{}upto(e).\mneg{}\msubb{}fst(L[x])  =  fst(L[e]))\_b


By

---

Latex:
((Assert  e  \mmember{}  E  BY
                (BLemma  `global-eo-E`  THEN  Auto))
  THEN  (Assert  pred(e)  \mmember{}  E  BY
                          ((InstLemma  `es-pred-wf-base`  [\mkleeneopen{}global-eo(L)\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (RWO  "global-eo-base-E"  (-1)  THENA  Auto)
                            THEN  (RWO  "global-eo-E-sq"  0  THENA  Auto)
                            THEN  Auto))
  )

---

Home Index