---

Step * of Lemma bag-partitions-with-one-given

∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[as,bs,cs:bag(T)].
    ([p∈bag-partitions(eq;cs)|bag-eq(eq;fst(p);as)] = {<as, bs>} ∈ bag(bag(T) × bag(T)))
    ∧ ([p∈bag-partitions(eq;cs)|bag-eq(eq;snd(p);bs)] = {<as, bs>} ∈ bag(bag(T) × bag(T))) 
    supposing (as + bs) = cs ∈ bag(T) 
  supposing valueall-type(T)
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 `bag-filter-no-repeats` THEN Auto)⋅
              THEN (RepUR ``product-deq`` 0 THEN BLemma `no-repeats-bag-partitions` ⋅ THEN Auto)⋅
              )⋅)
   THEN Try ((BLemma `bag-single-no-repeats` THEN Auto)⋅)
   THEN Try ((BagMemberD (-1)
              THEN BagMemberD 0
              THEN Auto
              THEN RW assert_pushdownC 0⋅
              THEN Auto
              THEN (RWO "-1" 0 THEN Auto)
              THEN BagMemberD 0
              THEN Auto))) }

1
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. as : bag(T)
5. bs : bag(T)
6. cs : bag(T)
7. (as + bs) = cs ∈ bag(T)
8. x : bag(T) × bag(T)
9. x ↓∈ [p∈bag-partitions(eq;cs)|bag-eq(eq;fst(p);as)]
⊢ x = <as, bs> ∈ (bag(T) × bag(T))

2
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. as : bag(T)
5. bs : bag(T)
6. cs : bag(T)
7. (as + bs) = cs ∈ bag(T)
8. [p∈bag-partitions(eq;cs)|bag-eq(eq;fst(p);as)] = {<as, bs>} ∈ bag(bag(T) × bag(T))
9. x : bag(T) × bag(T)
10. x ↓∈ [p∈bag-partitions(eq;cs)|bag-eq(eq;snd(p);bs)]
⊢ x = <as, bs> ∈ (bag(T) × bag(T))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[eq:EqDecider(T)].  \mforall{}[as,bs,cs:bag(T)].
        ([p\mmember{}bag-partitions(eq;cs)|bag-eq(eq;fst(p);as)]  =  \{<as,  bs>\})
        \mwedge{}  ([p\mmember{}bag-partitions(eq;cs)|bag-eq(eq;snd(p);bs)]  =  \{<as,  bs>\}) 
        supposing  (as  +  bs)  =  cs 
    supposing  valueall-type(T)


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  `bag-filter-no-repeats`  THEN  Auto)\mcdot{}
                        THEN  (RepUR  ``product-deq``  0  THEN  BLemma  `no-repeats-bag-partitions`  \mcdot{}  THEN  Auto)\mcdot{}
                        )\mcdot{})
  THEN  Try  ((BLemma  `bag-single-no-repeats`  THEN  Auto)\mcdot{})
  THEN  Try  ((BagMemberD  (-1)
                        THEN  BagMemberD  0
                        THEN  Auto
                        THEN  RW  assert\_pushdownC  0\mcdot{}
                        THEN  Auto
                        THEN  (RWO  "-1"  0  THEN  Auto)
                        THEN  BagMemberD  0
                        THEN  Auto)))

---

Home Index