---

Step * of Lemma bag-mapfilter-mapfilter

No Annotations
∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]}  ⟶ B]. ∀[Q:B ⟶ 𝔹]. ∀[g:{x:B| ↑Q[x]}  ⟶ C].
  (bag-mapfilter(g;Q;bag-mapfilter(f;P;b)) = bag-mapfilter(g o f;λx.(P[x] ∧b Q[f[x]]);b) ∈ bag(C))
BY
{ TACTIC:(Auto THEN RepUR ``bag-mapfilter`` 0 THEN Assert ⌜bag-map(g o f;[x∈b|P[x] ∧b Q[f[x]]]) ∈ bag(C)⌝⋅) }

1
.....assertion..... 
1. A : Type
2. B : Type
3. C : Type
4. b : bag(A)
5. P : A ⟶ 𝔹
6. f : {x:A| ↑P[x]}  ⟶ B
7. Q : B ⟶ 𝔹
8. g : {x:B| ↑Q[x]}  ⟶ C
⊢ bag-map(g o f;[x∈b|P[x] ∧b Q[f[x]]]) ∈ bag(C)

2
1. A : Type
2. B : Type
3. C : Type
4. b : bag(A)
5. P : A ⟶ 𝔹
6. f : {x:A| ↑P[x]}  ⟶ B
7. Q : B ⟶ 𝔹
8. g : {x:B| ↑Q[x]}  ⟶ C
9. bag-map(g o f;[x∈b|P[x] ∧b Q[f[x]]]) ∈ bag(C)
⊢ bag-map(g;[x∈bag-map(f;[x∈b|P x])|Q x]) = bag-map(g o f;[x∈b|P[x] ∧b Q[f[x]]]) ∈ bag(C)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B,C:Type].  \mforall{}[b:bag(A)].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:A|  \muparrow{}P[x]\}    {}\mrightarrow{}  B].  \mforall{}[Q:B  {}\mrightarrow{}  \mBbbB{}].
\mforall{}[g:\{x:B|  \muparrow{}Q[x]\}    {}\mrightarrow{}  C].
    (bag-mapfilter(g;Q;bag-mapfilter(f;P;b))  =  bag-mapfilter(g  o  f;\mlambda{}x.(P[x]  \mwedge{}\msubb{}  Q[f[x]]);b))


By

---

Latex:
TACTIC:(Auto
                THEN  RepUR  ``bag-mapfilter``  0
                THEN  Assert  \mkleeneopen{}bag-map(g  o  f;[x\mmember{}b|P[x]  \mwedge{}\msubb{}  Q[f[x]]])  \mmember{}  bag(C)\mkleeneclose{}\mcdot{})

---

Home Index