---

Step * 1 of Lemma map-concat-filter-lemma1


1. A : Type
2. B : Type
3. L2 : (tg:Id × (A ─→ B ─→ (Top List))) List
4. L : (Top × Id × Top) List
5. tg : Id
6. a : A
7. b : B
8. map(λx.(snd(x));L) = concat(map(λtgf.map(λx.<fst(tgf), x>;(snd(tgf)) a b);L2)) ∈ ((tg:Id × Top) List)
9. x : Top × Id × Top
10. (x ∈ filter(λms.fst(snd(ms)) = tg;L))@i
⊢ (tg ∈ map(λp.(fst(p));L2))
BY
{ (((RWO "member_filter" (-1)) THENA Auto) THEN (Reduce (-1)) THEN (D (-1))) }

1
1. A : Type
2. B : Type
3. L2 : (tg:Id × (A ─→ B ─→ (Top List))) List
4. L : (Top × Id × Top) List
5. tg : Id
6. a : A
7. b : B
8. map(λx.(snd(x));L) = concat(map(λtgf.map(λx.<fst(tgf), x>;(snd(tgf)) a b);L2)) ∈ ((tg:Id × Top) List)
9. x : Top × Id × Top
10. (x ∈ L)
11. ↑fst(snd(x)) = tg
⊢ (tg ∈ map(λp.(fst(p));L2))

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  L2  :  (tg:Id  \mtimes{}  (A  {}\mrightarrow{}  B  {}\mrightarrow{}  (Top  List)))  List
4.  L  :  (Top  \mtimes{}  Id  \mtimes{}  Top)  List
5.  tg  :  Id
6.  a  :  A
7.  b  :  B
8.  map(\mlambda{}x.(snd(x));L)  =  concat(map(\mlambda{}tgf.map(\mlambda{}x.<fst(tgf),  x>(snd(tgf))  a  b);L2))
9.  x  :  Top  \mtimes{}  Id  \mtimes{}  Top
10.  (x  \mmember{}  filter(\mlambda{}ms.fst(snd(ms))  =  tg;L))@i
\mvdash{}  (tg  \mmember{}  map(\mlambda{}p.(fst(p));L2))


By

(((RWO  "member\_filter"  (-1))  THENA  Auto)  THEN  (Reduce  (-1))  THEN  (D  (-1)))

---

Home Index