---

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

.....wf..... 
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)))} )
10. z : bag({x:A| ↑((P x) ∧b (Q (f x)))} )
⊢ z = [x∈b|P[x] ∧b Q[f[x]]] ∈ bag({x:{x:A| ↑(P x)} | ↑(Q (f x))} ) ∈ ℙ
BY
{ (MemCD
   THEN Try (Complete (Auto))
   THEN DoSubsume
   THEN Try (CompleteAuto)
   THEN RepUR ``so_apply`` 0
   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:
.....wf..... 
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))]
10.  z  :  bag(\{x:A|  \muparrow{}((P  x)  \mwedge{}\msubb{}  (Q  (f  x)))\}  )
\mvdash{}  z  =  [x\mmember{}b|P[x]  \mwedge{}\msubb{}  Q[f[x]]]  \mmember{}  \mBbbP{}


By

---

Latex:
(MemCD
  THEN  Try  (Complete  (Auto))
  THEN  DoSubsume
  THEN  Try  (CompleteAuto)
  THEN  RepUR  ``so\_apply``  0
  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