---

Step * of Lemma map-concat-filter-lemma1

∀[A,B:Type]. ∀[L2:(tg:Id × (A ─→ B ─→ (Top List))) List]. ∀[L:(Top × Id × Top) List]. ∀[tg:Id]. ∀[a:A]. ∀[b:B].
  {(filter(λms.fst(snd(ms)) = tg;L) = [] ∈ ((Top × Id × Top) List)) supposing 
      ((¬(tg ∈ map(λp.(fst(p));L2))) and 
      (map(λx.(snd(x));L) = concat(map(λtgf.map(λx.<fst(tgf), x>;(snd(tgf)) a b);L2)) ∈ ((tg:Id × Top) List)))}
BY
{ (Unfold `guard` 0 THEN Auto THEN RWO "nil-iff-no-member" 0 THEN Auto THEN (ParallelOp (-2))) }

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 ∈ filter(λms.fst(snd(ms)) = tg;L))@i
⊢ (tg ∈ map(λp.(fst(p));L2))

---

Latex:


\mforall{}[A,B:Type].  \mforall{}[L2:(tg:Id  \mtimes{}  (A  {}\mrightarrow{}  B  {}\mrightarrow{}  (Top  List)))  List].  \mforall{}[L:(Top  \mtimes{}  Id  \mtimes{}  Top)  List].  \mforall{}[tg:Id].
\mforall{}[a:A].  \mforall{}[b:B].
    \{(filter(\mlambda{}ms.fst(snd(ms))  =  tg;L)  =  [])  supposing 
            ((\mneg{}(tg  \mmember{}  map(\mlambda{}p.(fst(p));L2)))  and 
            (map(\mlambda{}x.(snd(x));L)  =  concat(map(\mlambda{}tgf.map(\mlambda{}x.<fst(tgf),  x>(snd(tgf))  a  b);L2))))\}


By

(Unfold  `guard`  0  THEN  Auto  THEN  RWO  "nil-iff-no-member"  0  THEN  Auto  THEN  (ParallelOp  (-2)))

---

Home Index