---

Step * 2 1 1 1 2 1 1 of Lemma bag-partitions-cons


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. x : X
5. b : bag(X)
6. x2 : bag(X)
7. x3 : bag(X)
8. (x2 + x3) = x.b ∈ bag(X)
9. ∀x:bag(X) × bag(X). ∀as,bs:bag(bag(X) × bag(X)).  (x ↓∈ as + bs ⇐⇒ x ↓∈ as ↓∨ x ↓∈ bs)
10. ∀x:bag(X) × bag(X). ∀f:(bag(X) × bag(X)) ⟶ (bag(X) × bag(X)). ∀bs:bag(bag(X) × bag(X)).
      uiff(x ↓∈ bag-map(f;bs);↓∃v:bag(X) × bag(X). (v ↓∈ bs ∧ (x = (f v) ∈ (bag(X) × bag(X)))))
11. (#x in x3) = 0 ∈ ℤ
12. x2 = bag-drop(eq;x2;x) ∈ bag(X)
13. ∀[x:X]. ∀[bs:bag(X)].  uiff(x ↓∈ bs;1 ≤ (#x in bs))
⊢ 1 ≤ (#x in x2)
BY
{ ((Assert (#x in x2 + x3) = (#x in {x} + b) ∈ ℤ BY
          (EqCD THEN Auto))
   THEN Unfold `single-bag` -1
   THEN (RWW "bag-count-append bag-count-single" (-1) THENA Auto)) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. x : X
5. b : bag(X)
6. x2 : bag(X)
7. x3 : bag(X)
8. (x2 + x3) = x.b ∈ bag(X)
9. ∀x:bag(X) × bag(X). ∀as,bs:bag(bag(X) × bag(X)).  (x ↓∈ as + bs ⇐⇒ x ↓∈ as ↓∨ x ↓∈ bs)
10. ∀x:bag(X) × bag(X). ∀f:(bag(X) × bag(X)) ⟶ (bag(X) × bag(X)). ∀bs:bag(bag(X) × bag(X)).
      uiff(x ↓∈ bag-map(f;bs);↓∃v:bag(X) × bag(X). (v ↓∈ bs ∧ (x = (f v) ∈ (bag(X) × bag(X)))))
11. (#x in x3) = 0 ∈ ℤ
12. x2 = bag-drop(eq;x2;x) ∈ bag(X)
13. ∀[x:X]. ∀[bs:bag(X)].  uiff(x ↓∈ bs;1 ≤ (#x in bs))
14. ((#x in x2) + (#x in x3)) = (if eq x x then 1 else 0 fi  + (#x in b)) ∈ ℤ
⊢ 1 ≤ (#x in x2)

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  x  :  X
5.  b  :  bag(X)
6.  x2  :  bag(X)
7.  x3  :  bag(X)
8.  (x2  +  x3)  =  x.b
9.  \mforall{}x:bag(X)  \mtimes{}  bag(X).  \mforall{}as,bs:bag(bag(X)  \mtimes{}  bag(X)).    (x  \mdownarrow{}\mmember{}  as  +  bs  \mLeftarrow{}{}\mRightarrow{}  x  \mdownarrow{}\mmember{}  as  \mdownarrow{}\mvee{}  x  \mdownarrow{}\mmember{}  bs)
10.  \mforall{}x:bag(X)  \mtimes{}  bag(X).  \mforall{}f:(bag(X)  \mtimes{}  bag(X))  {}\mrightarrow{}  (bag(X)  \mtimes{}  bag(X)).  \mforall{}bs:bag(bag(X)  \mtimes{}  bag(X)).
            uiff(x  \mdownarrow{}\mmember{}  bag-map(f;bs);\mdownarrow{}\mexists{}v:bag(X)  \mtimes{}  bag(X).  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v))))
11.  (\#x  in  x3)  =  0
12.  x2  =  bag-drop(eq;x2;x)
13.  \mforall{}[x:X].  \mforall{}[bs:bag(X)].    uiff(x  \mdownarrow{}\mmember{}  bs;1  \mleq{}  (\#x  in  bs))
\mvdash{}  1  \mleq{}  (\#x  in  x2)


By

---

Latex:
((Assert  (\#x  in  x2  +  x3)  =  (\#x  in  \{x\}  +  b)  BY
                (EqCD  THEN  Auto))
  THEN  Unfold  `single-bag`  -1
  THEN  (RWW  "bag-count-append  bag-count-single"  (-1)  THENA  Auto))

---

Home Index