---

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


1. L : (Id × Top) List
2. e : ℕ||L||
⊢ map(λx.(snd(x));filter(λx.fst(x) = loc(e);firstn(e;L))) @ [info(e)] 
~ map(λx.(snd(x));filter(λx.fst(x) = loc(e);firstn(e + 1;L)))
BY
{ ((InstLemma `firstn_decomp` [⌈Id × Top⌉;⌈e + 1⌉;⌈L⌉]⋅ THENA Auto)
   THEN (Subst' (e + 1) - 1 ~ e -1 THENA Auto)
   THEN RevHypSubst' (-1) 0
   THEN ((RWW "filter_append_sq map_append_sq" 0 THENM (EqCD THEN Try (Trivial))) THENA Auto)) }

1
1. L : (Id × Top) List
2. e : ℕ||L||
3. firstn(e;L) @ [L[e]] ~ firstn(e + 1;L)
⊢ [info(e)] ~ map(λx.(snd(x));filter(λx.fst(x) = loc(e);[L[e]]))

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `firstn\_decomp`  [\mkleeneopen{}Id  \mtimes{}  Top\mkleeneclose{};\mkleeneopen{}e  +  1\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  (e  +  1)  -  1  \msim{}  e  -1  THENA  Auto)
  THEN  RevHypSubst'  (-1)  0
  THEN  ((RWW  "filter\_append\_sq  map\_append\_sq"  0  THENM  (EqCD  THEN  Try  (Trivial)))  THENA  Auto))

---

Home Index