---

Step * of Lemma equal-count-bag-to-set

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x,y:T].
  uiff((#x in bag-to-set(eq;bs)) = (#y in bag-to-set(eq;bs)) ∈ ℤ;x ↓∈ bs ⇐⇒ y ↓∈ bs)
BY
{ xxx((InstLemma `bag-member-count` []⋅ THEN RepeatFor 2 (ParallelLast'))
      THEN InstLemma `member-bag-to-set` [⌜T⌝;⌜eq⌝]⋅
      THEN Auto)xxx }

1
1. T : Type
2. eq : EqDecider(T)
3. ∀[x:T]. ∀[bs:bag(T)].  uiff(x ↓∈ bs;1 ≤ (#x in bs))
4. ∀[bs:bag(T)]. ∀[x:T].  uiff(x ↓∈ bs;x ↓∈ bag-to-set(eq;bs))
5. bs : bag(T)
6. x : T
7. y : T
8. (#x in bag-to-set(eq;bs)) = (#y in bag-to-set(eq;bs)) ∈ ℤ
9. x ↓∈ bs
⊢ y ↓∈ bs

2
1. T : Type
2. eq : EqDecider(T)
3. ∀[x:T]. ∀[bs:bag(T)].  uiff(x ↓∈ bs;1 ≤ (#x in bs))
4. ∀[bs:bag(T)]. ∀[x:T].  uiff(x ↓∈ bs;x ↓∈ bag-to-set(eq;bs))
5. bs : bag(T)
6. x : T
7. y : T
8. (#x in bag-to-set(eq;bs)) = (#y in bag-to-set(eq;bs)) ∈ ℤ
9. y ↓∈ bs
⊢ x ↓∈ bs

3
1. T : Type
2. eq : EqDecider(T)
3. ∀[x:T]. ∀[bs:bag(T)].  uiff(x ↓∈ bs;1 ≤ (#x in bs))
4. ∀[bs:bag(T)]. ∀[x:T].  uiff(x ↓∈ bs;x ↓∈ bag-to-set(eq;bs))
5. bs : bag(T)
6. x : T
7. y : T
8. x ↓∈ bs ⇒ y ↓∈ bs
9. x ↓∈ bs ⇐ y ↓∈ bs
⊢ (#x in bag-to-set(eq;bs)) = (#y in bag-to-set(eq;bs)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x,y:T].
    uiff((\#x  in  bag-to-set(eq;bs))  =  (\#y  in  bag-to-set(eq;bs));x  \mdownarrow{}\mmember{}  bs  \mLeftarrow{}{}\mRightarrow{}  y  \mdownarrow{}\mmember{}  bs)


By

---

Latex:
xxx((InstLemma  `bag-member-count`  []\mcdot{}  THEN  RepeatFor  2  (ParallelLast'))
        THEN  InstLemma  `member-bag-to-set`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}
        THEN  Auto)xxx

---

Home Index