---

Step * 2 2 1 of Lemma bag-mapfilter-mapfilter


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. [x∈[x∈b|P x]|Q (f x)] = [x∈b|(P x) ∧b (Q (f x))] ∈ bag({x:A| ↑((P x) ∧b (Q (f x)))} )
⊢ [x∈b|(P x) ∧b (Q (f x))] = [x∈b|P[x] ∧b Q[f[x]]] ∈ bag({x:{x:A| ↑(P x)} | ↑(Q (f x))} )
BY
{ (RepUR ``so_apply`` 0
   THEN Try (Fold `member` 0)
   THEN DoSubsume
   THEN Try (Complete (Auto))
   THEN SubtypeReasoning
   THEN Try (CompleteAuto)
   THEN Try (Complete ((SupposeNot THEN Assert ⌜False⌝⋅ THEN Auto THEN Subst ⌜P x ~ ff⌝ (-2)⋅ THEN Auto)))
   THEN ((Decide ↑(P x) THENA Auto) THENL [(Subst ⌜P x ~ tt⌝ (-2)⋅ THENA Auto);(Subst ⌜P x ~ ff⌝ (-2)⋅ THENA Auto)⋅])
   THEN Reduce (-2)
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  b  :  bag(A)
5.  P  :  A  {}\mrightarrow{}  \mBbbB{}
6.  f  :  \{x:A|  \muparrow{}P[x]\}    {}\mrightarrow{}  B
7.  Q  :  B  {}\mrightarrow{}  \mBbbB{}
8.  g  :  \{x:B|  \muparrow{}Q[x]\}    {}\mrightarrow{}  C
9.  [x\mmember{}[x\mmember{}b|P  x]|Q  (f  x)]  =  [x\mmember{}b|(P  x)  \mwedge{}\msubb{}  (Q  (f  x))]
\mvdash{}  [x\mmember{}b|(P  x)  \mwedge{}\msubb{}  (Q  (f  x))]  =  [x\mmember{}b|P[x]  \mwedge{}\msubb{}  Q[f[x]]]


By

---

Latex:
(RepUR  ``so\_apply``  0
  THEN  Try  (Fold  `member`  0)
  THEN  DoSubsume
  THEN  Try  (Complete  (Auto))
  THEN  SubtypeReasoning
  THEN  Try  (CompleteAuto)
  THEN  Try  (Complete  ((SupposeNot
                                            THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
                                            THEN  Auto
                                            THEN  Subst  \mkleeneopen{}P  x  \msim{}  ff\mkleeneclose{}  (-2)\mcdot{}
                                            THEN  Auto)))
  THEN  ((Decide  \muparrow{}(P  x)  THENA  Auto)
  THENL  [(Subst  \mkleeneopen{}P  x  \msim{}  tt\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto);(Subst  \mkleeneopen{}P  x  \msim{}  ff\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)\mcdot{}])
  THEN  Reduce  (-2)
  THEN  Auto)

---

Home Index