---

Step * of Lemma bag-decomp_wf

No Annotations
∀[T:Type]. ∀[bs:bag(T)].  (bag-decomp(bs) ∈ bag(T × bag(T)))
BY
{ (Auto THEN D -1 THEN Auto THEN Unfold `bag-decomp` 0 THEN EqTypeCD THEN Auto) }

1
.....antecedent..... 
1. T : Type
2. bs : Base
3. b1 : Base
4. bs = b1 ∈ (as,bs:T List//permutation(T;as;bs))
5. bs ∈ T List
6. b1 ∈ T List
7. permutation(T;bs;b1)
⊢ permutation(T × bag(T);map(λn.remove-nth(n;bs);upto(||bs||));map(λn.remove-nth(n;b1);upto(||b1||)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].    (bag-decomp(bs)  \mmember{}  bag(T  \mtimes{}  bag(T)))


By

---

Latex:
(Auto  THEN  D  -1  THEN  Auto  THEN  Unfold  `bag-decomp`  0  THEN  EqTypeCD  THEN  Auto)

---

Home Index