---

Step * of Lemma bag-partitions-cons

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[x:X]. ∀[b:bag(X)].
    (bag-partitions(eq;x.b)
    = (bag-map(λp.<x.fst(p), snd(p)>;[p∈bag-partitions(eq;b)|((#x in snd(p)) =z 0)])
      + bag-map(λp.<fst(p), x.snd(p)>;bag-partitions(eq;b)))
    ∈ bag(bag(X) × bag(X))) 
  supposing valueall-type(X)
BY
{ (Auto
   THEN Using [`eq',⌜product-deq(bag(T);bag(T);bag-deq(eq);bag-deq(eq))⌝] (BLemma `bag-extensionality-no-repeats`)⋅
   THEN Auto
   THEN Try ((BLemma `no-repeats-bag-partitions` ⋅ THEN Auto))) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. x : X
5. b : bag(X)
6. bag-no-repeats(bag(X) × bag(X);bag-partitions(eq;x.b))
⊢ bag-no-repeats(bag(X) × bag(X);bag-map(λp.<x.fst(p), snd(p)>;[p∈bag-partitions(eq;b)|((#x in snd(p)) =z 0)])
+ bag-map(λp.<fst(p), x.snd(p)>;bag-partitions(eq;b)))

2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. x : X
5. b : bag(X)
6. x1 : bag(X) × bag(X)
7. x1 ↓∈ bag-partitions(eq;x.b)
⊢ x1 ↓∈ bag-map(λp.<x.fst(p), snd(p)>;[p∈bag-partitions(eq;b)|((#x in snd(p)) =z 0)])
+ bag-map(λp.<fst(p), x.snd(p)>;bag-partitions(eq;b))

3
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. x : X
5. b : bag(X)
6. x1 : bag(X) × bag(X)
7. x1 ↓∈ bag-map(λp.<x.fst(p), snd(p)>;[p∈bag-partitions(eq;b)|((#x in snd(p)) =z 0)])
+ bag-map(λp.<fst(p), x.snd(p)>;bag-partitions(eq;b))
⊢ x1 ↓∈ bag-partitions(eq;x.b)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[x:X].  \mforall{}[b:bag(X)].
        (bag-partitions(eq;x.b)
        =  (bag-map(\mlambda{}p.<x.fst(p),  snd(p)>[p\mmember{}bag-partitions(eq;b)|((\#x  in  snd(p))  =\msubz{}  0)])
            +  bag-map(\mlambda{}p.<fst(p),  x.snd(p)>bag-partitions(eq;b)))) 
    supposing  valueall-type(X)


By

---

Latex:
(Auto
  THEN  Using  [`eq',\mkleeneopen{}product-deq(bag(T);bag(T);bag-deq(eq);bag-deq(eq))\mkleeneclose{}
  ]  (BLemma  `bag-extensionality-no-repeats`)\mcdot{}
  THEN  Auto
  THEN  Try  ((BLemma  `no-repeats-bag-partitions`  \mcdot{}  THEN  Auto)))

---

Home Index