---

Step * 1 2 1 1 1 of Lemma empty-bag-union


1. T : Type
2. bag(T) List ∈ Type
3. ∀as,b1:bag(T) List.  (permutation(bag(T);as;b1) ∈ Type)
4. ∀as:bag(T) List. permutation(bag(T);as;as)
5. a : Base
6. b : Base
7. c : a = b ∈ pertype(λas,bs. ((as ∈ bag(T) List) ∧ (bs ∈ bag(T) List) ∧ permutation(bag(T);as;bs)))
8. a ∈ bag(T) List
9. b ∈ bag(T) List
10. permutation(bag(T);a;b)
11. bag-union(a) = {} ∈ bag(T)
12. ||a|| = ||b|| ∈ ℤ
13. i : ℕ
14. i < ||a||
⊢ a[i] = b[i] ∈ (Top List)
BY
{ Assert ⌜∀x:Top List. ((x ∈ a) ⇒ (x ~ []))⌝⋅ }

1
.....assertion..... 
1. T : Type
2. bag(T) List ∈ Type
3. ∀as,b1:bag(T) List.  (permutation(bag(T);as;b1) ∈ Type)
4. ∀as:bag(T) List. permutation(bag(T);as;as)
5. a : Base
6. b : Base
7. c : a = b ∈ pertype(λas,bs. ((as ∈ bag(T) List) ∧ (bs ∈ bag(T) List) ∧ permutation(bag(T);as;bs)))
8. a ∈ bag(T) List
9. b ∈ bag(T) List
10. permutation(bag(T);a;b)
11. bag-union(a) = {} ∈ bag(T)
12. ||a|| = ||b|| ∈ ℤ
13. i : ℕ
14. i < ||a||
⊢ ∀x:Top List. ((x ∈ a) ⇒ (x ~ []))

2
1. T : Type
2. bag(T) List ∈ Type
3. ∀as,b1:bag(T) List.  (permutation(bag(T);as;b1) ∈ Type)
4. ∀as:bag(T) List. permutation(bag(T);as;as)
5. a : Base
6. b : Base
7. c : a = b ∈ pertype(λas,bs. ((as ∈ bag(T) List) ∧ (bs ∈ bag(T) List) ∧ permutation(bag(T);as;bs)))
8. a ∈ bag(T) List
9. b ∈ bag(T) List
10. permutation(bag(T);a;b)
11. bag-union(a) = {} ∈ bag(T)
12. ||a|| = ||b|| ∈ ℤ
13. i : ℕ
14. i < ||a||
15. ∀x:Top List. ((x ∈ a) ⇒ (x ~ []))
⊢ a[i] = b[i] ∈ (Top List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  bag(T)  List  \mmember{}  Type
3.  \mforall{}as,b1:bag(T)  List.    (permutation(bag(T);as;b1)  \mmember{}  Type)
4.  \mforall{}as:bag(T)  List.  permutation(bag(T);as;as)
5.  a  :  Base
6.  b  :  Base
7.  c  :  a  =  b
8.  a  \mmember{}  bag(T)  List
9.  b  \mmember{}  bag(T)  List
10.  permutation(bag(T);a;b)
11.  bag-union(a)  =  \{\}
12.  ||a||  =  ||b||
13.  i  :  \mBbbN{}
14.  i  <  ||a||
\mvdash{}  a[i]  =  b[i]


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}x:Top  List.  ((x  \mmember{}  a)  {}\mRightarrow{}  (x  \msim{}  []))\mkleeneclose{}\mcdot{}

---

Home Index