---

Step * 1 1 of Lemma bag-partitions-symmetry


1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. bs : bag(T)
5. proddeq(bag-deq(eq);bag-deq(eq)) ∈ EqDecider(bag(T) × bag(T))
6. x : bag(T) × bag(T)
7. x ↓∈ bag-partitions(eq;bs)
⊢ (#x in bag-partitions(eq;bs)) = (#x in bag-map(λp.<snd(p), fst(p)>;bag-partitions(eq;bs))) ∈ ℤ
BY
{ ((InstLemma `bag-count-map` 
    [⌜bag(T) × bag(T)⌝;⌜bag(T) × bag(T)⌝;⌜λp.<snd(p), fst(p)>⌝;⌜proddeq(bag-deq(eq);bag-deq(eq))⌝;
    ⌜proddeq(bag-deq(eq);bag-deq(eq))⌝;⌜x⌝;⌜bag-partitions(eq;bs)⌝;⌜λp.<snd(p), fst(p)>⌝]⋅
    THEN (Reduce 0 THEN Auto)
    THEN Reduce (-1))
   THEN Try ((D -1 THEN Reduce 0 THEN Auto))
   THEN RWO "-1" 0) }

1
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. bs : bag(T)
5. proddeq(bag-deq(eq);bag-deq(eq)) ∈ EqDecider(bag(T) × bag(T))
6. x : bag(T) × bag(T)
7. x ↓∈ bag-partitions(eq;bs)
8. (#x in bag-map(λp.<snd(p), fst(p)>;bag-partitions(eq;bs))) ~ (#<snd(x), fst(x)> in bag-partitions(eq;bs))
⊢ (#x in bag-partitions(eq;bs)) = (#<snd(x), fst(x)> in bag-partitions(eq;bs)) ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  valueall-type(T)
3.  eq  :  EqDecider(T)
4.  bs  :  bag(T)
5.  proddeq(bag-deq(eq);bag-deq(eq))  \mmember{}  EqDecider(bag(T)  \mtimes{}  bag(T))
6.  x  :  bag(T)  \mtimes{}  bag(T)
7.  x  \mdownarrow{}\mmember{}  bag-partitions(eq;bs)
\mvdash{}  (\#x  in  bag-partitions(eq;bs))  =  (\#x  in  bag-map(\mlambda{}p.<snd(p),  fst(p)>bag-partitions(eq;bs)))


By

---

Latex:
((InstLemma  `bag-count-map` 
    [\mkleeneopen{}bag(T)  \mtimes{}  bag(T)\mkleeneclose{};\mkleeneopen{}bag(T)  \mtimes{}  bag(T)\mkleeneclose{};\mkleeneopen{}\mlambda{}p.<snd(p),  fst(p)>\mkleeneclose{};\mkleeneopen{}proddeq(bag-deq(eq);bag-deq(eq))\mkleeneclose{};
    \mkleeneopen{}proddeq(bag-deq(eq);bag-deq(eq))\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bag-partitions(eq;bs)\mkleeneclose{};\mkleeneopen{}\mlambda{}p.<snd(p),  fst(p)>\mkleeneclose{}]\mcdot{}
    THEN  (Reduce  0  THEN  Auto)
    THEN  Reduce  (-1))
  THEN  Try  ((D  -1  THEN  Reduce  0  THEN  Auto))
  THEN  RWO  "-1"  0)

---

Home Index