---

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


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
BY
{ (Unfold `es-first` 0 THEN (RWO "global-eo-eq-E global-eo-dom" 0 THENA Auto) THEN Reduce 0) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `es-first`  0  THEN  (RWO  "global-eo-eq-E  global-eo-dom"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index