---

Step * 1 of Lemma global-eo-info-before


1. L : (Id × Top) List
2. e : {e:ℕ||L||| True} 
⊢ map(λe.info(e);filter(λn.loc(n) = loc(e);upto(e))) ~ map(λx.(snd(x));filter(λx.fst(x) = loc(e);map(λi.L[i];upto(e))))
BY
{ ((GenConclTerm ⌈upto(e)⌉⋅ THENA Auto) THEN (RWO "global-eo-loc global-eo-info" 0 THENA Auto)) }

1
1. L : (Id × Top) List
2. e : {e:ℕ||L||| True} 
3. v : ℕe List@i
4. upto(e) = v ∈ (ℕe List)@i
⊢ map(λe.(snd(L[e]));filter(λn.fst(L[n]) = fst(L[e]);v)) ~ map(λx.(snd(x));filter(λx.fst(x) = fst(L[e]);map(λi.L[i];v)))

---

Latex:

---

Latex:

1.  L  :  (Id  \mtimes{}  Top)  List
2.  e  :  \{e:\mBbbN{}||L|||  True\} 
\mvdash{}  map(\mlambda{}e.info(e);filter(\mlambda{}n.loc(n)  =  loc(e);upto(e))) 
\msim{}  map(\mlambda{}x.(snd(x));filter(\mlambda{}x.fst(x)  =  loc(e);map(\mlambda{}i.L[i];upto(e))))


By

---

Latex:
((GenConclTerm  \mkleeneopen{}upto(e)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (RWO  "global-eo-loc  global-eo-info"  0  THENA  Auto))

---

Home Index