---

Step * 1 1 of Lemma global-eo-first


1. [L] : (Id × Top) List
2. [e] : {e:ℕ||L||| True} 
⊢ first(e) ~ (∀x∈upto(e).¬bloc(x) = loc(e))_b
BY
{ Assert ⌈first(e) = (∀x∈upto(e).¬bloc(x) = loc(e))_b⌉⋅ }

1
.....assertion..... 
1. L : (Id × Top) List
2. e : {e:ℕ||L||| True} 
⊢ first(e) = (∀x∈upto(e).¬bloc(x) = loc(e))_b

2
1. [L] : (Id × Top) List
2. [e] : {e:ℕ||L||| True} 
3. first(e) = (∀x∈upto(e).¬bloc(x) = loc(e))_b
⊢ first(e) ~ (∀x∈upto(e).¬bloc(x) = loc(e))_b

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}first(e)  =  (\mforall{}x\mmember{}upto(e).\mneg{}\msubb{}loc(x)  =  loc(e))\_b\mkleeneclose{}\mcdot{}

---

Home Index