Step
*
1
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)
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)) ∈ ℤ
BY
{ (Unfold `bag-partitions` 0 THEN (CallByValueReduce 0 THENA Auto)) }
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-to-set(proddeq(bag-deq(eq);bag-deq(eq));bag-splits(bs)))
= (#<snd(x), fst(x)> in bag-to-set(proddeq(bag-deq(eq);bag-deq(eq));bag-splits(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)
8. (\#x in bag-map(\mlambda{}p.<snd(p), fst(p)>bag-partitions(eq;bs))) \msim{} (\#<snd(x), fst(x)> in bag-partitions\000C(eq;bs))
\mvdash{} (\#x in bag-partitions(eq;bs)) = (\#<snd(x), fst(x)> in bag-partitions(eq;bs))
By
Latex:
(Unfold `bag-partitions` 0 THEN (CallByValueReduce 0 THENA Auto))
Home
Index