---

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


1. L : (Id × Top) List
2. e : ℕ||L||
⊢ first(e) = (∀x∈upto(e).¬bloc(x) = loc(e))_b
BY
{ (RWO "global-eo-loc" 0 THENA Auto) }

1
1. L : (Id × Top) List
2. e : ℕ||L||
⊢ 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{}loc(x)  =  loc(e))\_b


By

---

Latex:
(RWO  "global-eo-loc"  0  THENA  Auto)

---

Home Index