---

Step * of Lemma equal-bag-size-le1

∀[T:Type]. ∀[as,bs:bag(T)].
  uiff(as = bs ∈ bag(T);(as = {} ∈ bag(T) ⇐⇒ bs = {} ∈ bag(T))
  ∧ ((#(as) = 1 ∈ ℤ) ⇒ (#(bs) = 1 ∈ ℤ) ⇒ (only(as) = only(bs) ∈ T))) 
  supposing (#(as) ≤ 1) ∧ (#(bs) ≤ 1)
BY
{ (Auto THEN (Decide ⌜#(as) < 1⌝⋅ THENA Auto) THEN (Decide ⌜#(bs) < 1⌝⋅ THENA Auto)) }

1
1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. #(as) ≤ 1
5. #(bs) ≤ 1
6. (as = {} ∈ bag(T)) ⇒ (bs = {} ∈ bag(T))
7. (as = {} ∈ bag(T)) ⇐ bs = {} ∈ bag(T)
8. (#(as) = 1 ∈ ℤ) ⇒ (#(bs) = 1 ∈ ℤ) ⇒ (only(as) = only(bs) ∈ T)
9. #(as) < 1
10. #(bs) < 1
⊢ as = bs ∈ bag(T)

2
1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. #(as) ≤ 1
5. #(bs) ≤ 1
6. (as = {} ∈ bag(T)) ⇒ (bs = {} ∈ bag(T))
7. (as = {} ∈ bag(T)) ⇐ bs = {} ∈ bag(T)
8. (#(as) = 1 ∈ ℤ) ⇒ (#(bs) = 1 ∈ ℤ) ⇒ (only(as) = only(bs) ∈ T)
9. #(as) < 1
10. ¬#(bs) < 1
⊢ as = bs ∈ bag(T)

3
1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. #(as) ≤ 1
5. #(bs) ≤ 1
6. (as = {} ∈ bag(T)) ⇒ (bs = {} ∈ bag(T))
7. (as = {} ∈ bag(T)) ⇐ bs = {} ∈ bag(T)
8. (#(as) = 1 ∈ ℤ) ⇒ (#(bs) = 1 ∈ ℤ) ⇒ (only(as) = only(bs) ∈ T)
9. ¬#(as) < 1
10. #(bs) < 1
⊢ as = bs ∈ bag(T)

4
1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. #(as) ≤ 1
5. #(bs) ≤ 1
6. (as = {} ∈ bag(T)) ⇒ (bs = {} ∈ bag(T))
7. (as = {} ∈ bag(T)) ⇐ bs = {} ∈ bag(T)
8. (#(as) = 1 ∈ ℤ) ⇒ (#(bs) = 1 ∈ ℤ) ⇒ (only(as) = only(bs) ∈ T)
9. ¬#(as) < 1
10. ¬#(bs) < 1
⊢ as = bs ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:bag(T)].
    uiff(as  =  bs;(as  =  \{\}  \mLeftarrow{}{}\mRightarrow{}  bs  =  \{\})  \mwedge{}  ((\#(as)  =  1)  {}\mRightarrow{}  (\#(bs)  =  1)  {}\mRightarrow{}  (only(as)  =  only(bs)))) 
    supposing  (\#(as)  \mleq{}  1)  \mwedge{}  (\#(bs)  \mleq{}  1)


By

---

Latex:
(Auto  THEN  (Decide  \mkleeneopen{}\#(as)  <  1\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (Decide  \mkleeneopen{}\#(bs)  <  1\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index