---

Step * 2 of Lemma equal-bag-size-le1


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)
BY
{ (D (-1) THEN RWO "6" 0 THEN Auto THEN (RWW "bag-size-zero" 0 THEN Auto THEN Reduce 0 THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  bag(T)
3.  bs  :  bag(T)
4.  \#(as)  \mleq{}  1
5.  \#(bs)  \mleq{}  1
6.  (as  =  \{\})  {}\mRightarrow{}  (bs  =  \{\})
7.  (as  =  \{\})  \mLeftarrow{}{}  bs  =  \{\}
8.  (\#(as)  =  1)  {}\mRightarrow{}  (\#(bs)  =  1)  {}\mRightarrow{}  (only(as)  =  only(bs))
9.  \#(as)  <  1
10.  \mneg{}\#(bs)  <  1
\mvdash{}  as  =  bs


By

---

Latex:
(D  (-1)  THEN  RWO  "6"  0  THEN  Auto  THEN  (RWW  "bag-size-zero"  0  THEN  Auto  THEN  Reduce  0  THEN  Auto)\mcdot{})

---

Home Index