---

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