---

Step * of Lemma map-concat-filter-lemma2

∀[C:Id ─→ Type]. ∀[A,B:Type]. ∀[L2:(tg:Id × (A ─→ B ─→ (C[tg] List))) List]. ∀[L:(l:IdLnk × t:Id × C[t]) List].
∀[tg:Id]. ∀[a:A]. ∀[b:B].
  {(||filter(λms.fst(snd(ms)) = tg;L)|| = 0 ∈ ℤ) 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 × C[tg]) List)))}
BY
{ (((Auto THEN (InstLemma `map-concat-filter-lemma1` [⌈A⌉; ⌈B⌉; ⌈L2⌉; ⌈L⌉; ⌈tg⌉; ⌈a⌉; ⌈b⌉])⋅) THENA Auto)
   THEN Unfold `guard` 0
   ) }

1
1. C : Id ─→ Type
2. A : Type
3. B : Type
4. L2 : (tg:Id × (A ─→ B ─→ (C[tg] List))) List
5. L : (l:IdLnk × t:Id × C[t]) List
6. tg : Id
7. a : A
8. b : B
9. (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)))
⊢ (||filter(λms.fst(snd(ms)) = tg;L)|| = 0 ∈ ℤ) 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 × C[tg]) List)))

---

Latex:


\mforall{}[C:Id  {}\mrightarrow{}  Type].  \mforall{}[A,B:Type].  \mforall{}[L2:(tg:Id  \mtimes{}  (A  {}\mrightarrow{}  B  {}\mrightarrow{}  (C[tg]  List)))  List].  \mforall{}[L:(l:IdLnk
                                                                                                                                                                  \mtimes{}  t:Id
                                                                                                                                                                  \mtimes{}  C[t])  List].
\mforall{}[tg:Id].  \mforall{}[a:A].  \mforall{}[b:B].
    \{(||filter(\mlambda{}ms.fst(snd(ms))  =  tg;L)||  =  0)  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

(((Auto  THEN  (InstLemma  `map-concat-filter-lemma1`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}L2\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{};  \mkleeneopen{}tg\mkleeneclose{};  \mkleeneopen{}a\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{}])\mcdot{})
    THENA  Auto
    )
  THEN  Unfold  `guard`  0
  )

---

Home Index