---

Step * of Lemma null-bag-filter-map

∀[T,A:Type]. ∀[f:A ⟶ T]. ∀[p:T ⟶ 𝔹]. ∀[as:bag(A)].  null([x∈bag-map(f;as)|p[x]]) = null([x∈as|p[f x]])
BY
{ (Auto
   THEN Unfolds ``bag-filter bag-map`` 0
   THEN BagD (-1)
   THEN Auto
   THEN (RWO "filter_map" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN (RWO "null-map" 0 THENA Auto)
   THEN Subst ⌜as = bs ∈ bag(A)⌝ 0 ⋅
   THEN Try ((EqTypeCD THEN Auto))
   THEN Try (Complete (Auto))) }

1
.....wf..... 
1. T : Type
2. A : Type
3. f : A ⟶ T
4. p : T ⟶ 𝔹
5. as : A List
6. bs : A List
7. permutation(A;as;bs)
8. z : bag(A)
⊢ null(filter(λx.p[f x];z)) = null(filter(λx.p[f x];bs)) ∈ ℙ

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[f:A  {}\mrightarrow{}  T].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[as:bag(A)].
    null([x\mmember{}bag-map(f;as)|p[x]])  =  null([x\mmember{}as|p[f  x]])


By

---

Latex:
(Auto
  THEN  Unfolds  ``bag-filter  bag-map``  0
  THEN  BagD  (-1)
  THEN  Auto
  THEN  (RWO  "filter\_map"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  (RWO  "null-map"  0  THENA  Auto)
  THEN  Subst  \mkleeneopen{}as  =  bs\mkleeneclose{}  0  \mcdot{}
  THEN  Try  ((EqTypeCD  THEN  Auto))
  THEN  Try  (Complete  (Auto)))

---

Home Index