---

Step * 2 1 1 3 1 1 1 1 1 of Lemma fps-compose-atom-neq


1. X : Type
2. {} ∈ bag(bag(X) List+)
3. valueall-type(X)
4. eq : EqDecider(X)
5. r : CRng
6. x : X
7. y : X
8. ¬(x = y ∈ X)
9. f : PowerSeries(X;r)
10. Comm(|r|;+r)
11. Assoc(|r|;*)
12. Comm(|r|;*)
13. IsMonoid(|r|;+r;0)
14. ∀L:bag(X) List+. (Πa ∈ tl(L). f a ∈ |r|)
15. b : bag(X)
16. u : bag(X)
17. (||[]|| + 1) ≥ 1 
18. ¬x ↓∈ hd([u])
19. (∀x∈tl([u]).¬(x = {} ∈ bag(X)))
20. bag-union([u]) = b ∈ bag(X)
21. (u + bag-rep(||[]||;x)) = {y} ∈ bag(X)
22. (||[]|| + 1) ≥ 1 
23. u = {y} ∈ bag(X)
24. bag-rep(||[]||;x) = {} ∈ bag(X)
25. ||[]|| = 0 ∈ ℤ
⊢ [{y}] ↓∈ if bag-null(bag-union([{y}])) then {}
if bag-eq(eq;bag-union([{y}]);{y}) then {[{y}]}
else {}
fi 
BY
{ Subst' bag-null(bag-union([{y}])) ~ ff 0 }

1
.....equality..... 
1. X : Type
2. {} ∈ bag(bag(X) List+)
3. valueall-type(X)
4. eq : EqDecider(X)
5. r : CRng
6. x : X
7. y : X
8. ¬(x = y ∈ X)
9. f : PowerSeries(X;r)
10. Comm(|r|;+r)
11. Assoc(|r|;*)
12. Comm(|r|;*)
13. IsMonoid(|r|;+r;0)
14. ∀L:bag(X) List+. (Πa ∈ tl(L). f a ∈ |r|)
15. b : bag(X)
16. u : bag(X)
17. (||[]|| + 1) ≥ 1 
18. ¬x ↓∈ hd([u])
19. (∀x∈tl([u]).¬(x = {} ∈ bag(X)))
20. bag-union([u]) = b ∈ bag(X)
21. (u + bag-rep(||[]||;x)) = {y} ∈ bag(X)
22. (||[]|| + 1) ≥ 1 
23. u = {y} ∈ bag(X)
24. bag-rep(||[]||;x) = {} ∈ bag(X)
25. ||[]|| = 0 ∈ ℤ
⊢ bag-null(bag-union([{y}])) ~ ff

2
1. X : Type
2. {} ∈ bag(bag(X) List+)
3. valueall-type(X)
4. eq : EqDecider(X)
5. r : CRng
6. x : X
7. y : X
8. ¬(x = y ∈ X)
9. f : PowerSeries(X;r)
10. Comm(|r|;+r)
11. Assoc(|r|;*)
12. Comm(|r|;*)
13. IsMonoid(|r|;+r;0)
14. ∀L:bag(X) List+. (Πa ∈ tl(L). f a ∈ |r|)
15. b : bag(X)
16. u : bag(X)
17. (||[]|| + 1) ≥ 1 
18. ¬x ↓∈ hd([u])
19. (∀x∈tl([u]).¬(x = {} ∈ bag(X)))
20. bag-union([u]) = b ∈ bag(X)
21. (u + bag-rep(||[]||;x)) = {y} ∈ bag(X)
22. (||[]|| + 1) ≥ 1 
23. u = {y} ∈ bag(X)
24. bag-rep(||[]||;x) = {} ∈ bag(X)
25. ||[]|| = 0 ∈ ℤ
⊢ [{y}] ↓∈ if ff then {}
if bag-eq(eq;bag-union([{y}]);{y}) then {[{y}]}
else {}
fi 

---

Latex:

---

Latex:

1.  X  :  Type
2.  \{\}  \mmember{}  bag(bag(X)  List\msupplus{})
3.  valueall-type(X)
4.  eq  :  EqDecider(X)
5.  r  :  CRng
6.  x  :  X
7.  y  :  X
8.  \mneg{}(x  =  y)
9.  f  :  PowerSeries(X;r)
10.  Comm(|r|;+r)
11.  Assoc(|r|;*)
12.  Comm(|r|;*)
13.  IsMonoid(|r|;+r;0)
14.  \mforall{}L:bag(X)  List\msupplus{}.  (\mPi{}a  \mmember{}  tl(L).  f  a  \mmember{}  |r|)
15.  b  :  bag(X)
16.  u  :  bag(X)
17.  (||[]||  +  1)  \mgeq{}  1 
18.  \mneg{}x  \mdownarrow{}\mmember{}  hd([u])
19.  (\mforall{}x\mmember{}tl([u]).\mneg{}(x  =  \{\}))
20.  bag-union([u])  =  b
21.  (u  +  bag-rep(||[]||;x))  =  \{y\}
22.  (||[]||  +  1)  \mgeq{}  1 
23.  u  =  \{y\}
24.  bag-rep(||[]||;x)  =  \{\}
25.  ||[]||  =  0
\mvdash{}  [\{y\}]  \mdownarrow{}\mmember{}  if  bag-null(bag-union([\{y\}]))  then  \{\}
if  bag-eq(eq;bag-union([\{y\}]);\{y\})  then  \{[\{y\}]\}
else  \{\}
fi 


By

---

Latex:
Subst'  bag-null(bag-union([\{y\}]))  \msim{}  ff  0

---

Home Index