---

Step * of Lemma bag-member-decomp

∀[T:Type]. ∀[bs:bag(T)]. ∀[x:T]. ∀[b:bag(T)].  uiff(<x, b> ↓∈ bag-decomp(bs);({x} + b) = bs ∈ bag(T))
BY
{ ((UnivCD THENA Auto) THEN UseWitness ⌜<Ax, Ax>⌝⋅ THEN BagD 4 THEN BagD 2 THEN Auto) }

1
1. T : Type
2. x : T
3. as : T List
4. v1 : T List
5. permutation(T;as;v1)
6. v : T List
7. bs : T List
8. permutation(T;v;bs)
9. <x, as> ↓∈ bag-decomp(v)
⊢ ({x} + as) = v ∈ bag(T)

2
1. T : Type
2. x : T
3. as : T List
4. v1 : T List
5. permutation(T;as;v1)
6. v : T List
7. bs : T List
8. permutation(T;v;bs)
9. ({x} + as) = v ∈ bag(T)
⊢ Ax ∈ <x, as> ↓∈ bag-decomp(v)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].  \mforall{}[b:bag(T)].    uiff(<x,  b>  \mdownarrow{}\mmember{}  bag-decomp(bs);(\{x\}  +  b)  =  bs)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  UseWitness  \mkleeneopen{}<Ax,  Ax>\mkleeneclose{}\mcdot{}  THEN  BagD  4  THEN  BagD  2  THEN  Auto)

---

Home Index