---

Step * 2 1 of Lemma bag-member-decomp


1. T : Type
2. x : T
3. as : T List
4. v1 : T List
5. permutation(T;as;v1)
6. [x / as] ∈ T List
7. Z : T List
8. permutation(T;[x / as];Z)
⊢ ∃L:(T × bag(T)) List. ((L = bag-decomp(Z) ∈ bag(T × bag(T))) ∧ (<x, as> ∈ L))
BY
{ With ⌜bag-decomp(Z)⌝ (D 0)⋅ }

1
.....wf..... 
1. T : Type
2. x : T
3. as : T List
4. v1 : T List
5. permutation(T;as;v1)
6. [x / as] ∈ T List
7. Z : T List
8. permutation(T;[x / as];Z)
⊢ bag-decomp(Z) ∈ (T × bag(T)) List

2
1. T : Type
2. x : T
3. as : T List
4. v1 : T List
5. permutation(T;as;v1)
6. [x / as] ∈ T List
7. Z : T List
8. permutation(T;[x / as];Z)
⊢ (bag-decomp(Z) = bag-decomp(Z) ∈ bag(T × bag(T))) ∧ (<x, as> ∈ bag-decomp(Z))

3
.....wf..... 
1. T : Type
2. x : T
3. as : T List
4. v1 : T List
5. permutation(T;as;v1)
6. [x / as] ∈ T List
7. Z : T List
8. permutation(T;[x / as];Z)
9. L : (T × bag(T)) List
⊢ (L = bag-decomp(Z) ∈ bag(T × bag(T))) ∧ (<x, as> ∈ L) ∈ ℙ

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  as  :  T  List
4.  v1  :  T  List
5.  permutation(T;as;v1)
6.  [x  /  as]  \mmember{}  T  List
7.  Z  :  T  List
8.  permutation(T;[x  /  as];Z)
\mvdash{}  \mexists{}L:(T  \mtimes{}  bag(T))  List.  ((L  =  bag-decomp(Z))  \mwedge{}  (<x,  as>  \mmember{}  L))


By

---

Latex:
With  \mkleeneopen{}bag-decomp(Z)\mkleeneclose{}  (D  0)\mcdot{}

---

Home Index