---

Step * of Lemma bag-filter-equal

∀[T:Type]. ∀[p1,p2:T ⟶ 𝔹]. ∀[b:bag(T)].  uiff([x∈b|p1[x]] = [x∈b|p2[x]] ∈ bag(T);∀x:T. (x ↓∈ b ⇒ (↑p1[x] ⇐⇒ ↑p2[x])))
BY
{ ((UnivCD THENA (Auto THEN DoSubsume THEN Auto)) THEN D 0 THEN (UnivCD THENA (Auto THEN DoSubsume THEN Auto))) }

1
1. T : Type
2. p1 : T ⟶ 𝔹
3. p2 : T ⟶ 𝔹
4. b : bag(T)
5. [x∈b|p1[x]] = [x∈b|p2[x]] ∈ bag(T)
6. x : T
7. x ↓∈ b
⊢ ↑p1[x] ⇐⇒ ↑p2[x]

2
1. T : Type
2. p1 : T ⟶ 𝔹
3. p2 : T ⟶ 𝔹
4. b : bag(T)
5. ∀x:T. (x ↓∈ b ⇒ (↑p1[x] ⇐⇒ ↑p2[x]))
⊢ [x∈b|p1[x]] = [x∈b|p2[x]] ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[p1,p2:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[b:bag(T)].
    uiff([x\mmember{}b|p1[x]]  =  [x\mmember{}b|p2[x]];\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (\muparrow{}p1[x]  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}p2[x])))


By

---

Latex:
((UnivCD  THENA  (Auto  THEN  DoSubsume  THEN  Auto))
  THEN  D  0
  THEN  (UnivCD  THENA  (Auto  THEN  DoSubsume  THEN  Auto)))

---

Home Index