---

Step * of Lemma bag-filter-trivial2

∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  [x∈bs|p[x]] = bs ∈ bag(T) supposing ∀x:T. (x ↓∈ bs ⇒ (↑p[x]))
BY
{ ((UnivCD THENA Auto)
   THEN (BagToList (-2) THENA (Auto THEN DoSubsume THEN Auto))
   THEN RepUR ``bag-filter`` 0
   THEN (MemTypeCD THEN Auto)
   THEN ListInd (-2)
   THEN Reduce 0
   THEN Auto
   THEN (InstHyp [⌜u⌝] (-1)⋅ THENA (Auto THEN BagMemberD 0 THEN (D 0 THEN Auto) THEN OrLeft THEN Auto))) }

1
1. T : Type
2. p : T ⟶ 𝔹
3. u : T
4. v : T List
5. (∀x:T. (x ↓∈ v ⇒ (↑p[x]))) ⇒ permutation(T;filter(λx.p[x];v);v)
6. ∀x:T. (x ↓∈ [u / v] ⇒ (↑p[x]))
7. ↑p[u]
⊢ permutation(T;if p[u] then [u / filter(λx.p[x];v)] else filter(λx.p[x];v) fi ;[u / v])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[bs:bag(T)].    [x\mmember{}bs|p[x]]  =  bs  supposing  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  (\muparrow{}p[x]))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (BagToList  (-2)  THENA  (Auto  THEN  DoSubsume  THEN  Auto))
  THEN  RepUR  ``bag-filter``  0
  THEN  (MemTypeCD  THEN  Auto)
  THEN  ListInd  (-2)
  THEN  Reduce  0
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  (-1)\mcdot{}
              THENA  (Auto  THEN  BagMemberD  0  THEN  (D  0  THEN  Auto)  THEN  OrLeft  THEN  Auto)
              ))

---

Home Index