Step
*
of Lemma
bag-remove-repeats-append
∀[T:Type]. ∀[as,bs:bag(T)]. ∀[eq:EqDecider(T)].
  (bag-remove-repeats(eq;as + bs)
  = (bag-remove-repeats(eq;as) + [x∈bag-remove-repeats(eq;bs)|¬bbag-deq-member(eq;x;as)])
  ∈ bag(T))
BY
{ ((UnivCD THENA Auto)
   THEN BLemma `bag-extensionality-no-repeats`
   THEN Auto
   THEN Try ((BLemma `bag-remove-repeats-no-repeats` THEN Auto))) }
1
1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. eq : EqDecider(T)
5. bag-no-repeats(T;bag-remove-repeats(eq;as + bs))
⊢ bag-no-repeats(T;bag-remove-repeats(eq;as) + [x∈bag-remove-repeats(eq;bs)|¬bbag-deq-member(eq;x;as)])
2
1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. eq : EqDecider(T)
5. x : T@i
6. x ↓∈ bag-remove-repeats(eq;as + bs)
⊢ x ↓∈ bag-remove-repeats(eq;as) + [x∈bag-remove-repeats(eq;bs)|¬bbag-deq-member(eq;x;as)]
3
1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. eq : EqDecider(T)
5. x : T@i
6. x ↓∈ bag-remove-repeats(eq;as) + [x∈bag-remove-repeats(eq;bs)|¬bbag-deq-member(eq;x;as)]
⊢ x ↓∈ bag-remove-repeats(eq;as + bs)
Latex:
Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:bag(T)].  \mforall{}[eq:EqDecider(T)].
    (bag-remove-repeats(eq;as  +  bs)
    =  (bag-remove-repeats(eq;as)  +  [x\mmember{}bag-remove-repeats(eq;bs)|\mneg{}\msubb{}bag-deq-member(eq;x;as)]))
By
Latex:
((UnivCD  THENA  Auto)
  THEN  BLemma  `bag-extensionality-no-repeats`
  THEN  Auto
  THEN  Try  ((BLemma  `bag-remove-repeats-no-repeats`  THEN  Auto)))
Home
Index