Step
*
of Lemma
bag-member-partitions
∀[T:Type]
∀[eq:EqDecider(T)]. ∀[as,bs,cs:bag(T)]. uiff(<as, bs> ↓∈ bag-partitions(eq;cs);(as + bs) = cs ∈ bag(T))
supposing valueall-type(T)
BY
{ ((UnivCD THENA Auto)
THEN Unfold `bag-partitions` 0
THEN (Assert proddeq(bag-deq(eq);bag-deq(eq)) ∈ EqDecider(bag(T) × bag(T)) BY
((Subst' proddeq(bag-deq(eq);bag-deq(eq)) ~ product-deq(bag(T);bag(T);bag-deq(eq);bag-deq(eq)) 0
THEN Auto
)
THEN RepUR ``product-deq`` 0
THEN Auto))
THEN (CallByValueReduce 0 THENA 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. proddeq(bag-deq(eq);bag-deq(eq)) ∈ EqDecider(bag(T) × bag(T))
⊢ uiff(<as, bs> ↓∈ bag-to-set(proddeq(bag-deq(eq);bag-deq(eq));bag-splits(cs));(as + bs) = cs ∈ bag(T))
Latex:
Latex:
\mforall{}[T:Type]
\mforall{}[eq:EqDecider(T)]. \mforall{}[as,bs,cs:bag(T)]. uiff(<as, bs> \mdownarrow{}\mmember{} bag-partitions(eq;cs);(as + bs) = cs)
supposing valueall-type(T)
By
Latex:
((UnivCD THENA Auto)
THEN Unfold `bag-partitions` 0
THEN (Assert proddeq(bag-deq(eq);bag-deq(eq)) \mmember{} EqDecider(bag(T) \mtimes{} bag(T)) BY
((Subst' proddeq(bag-deq(eq);bag-deq(eq))
\msim{} product-deq(bag(T);bag(T);bag-deq(eq);bag-deq(eq)) 0
THEN Auto
)
THEN RepUR ``product-deq`` 0
THEN Auto))
THEN (CallByValueReduce 0 THENA Auto))
Home
Index