---

Step * 3 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 (-2) THEN RWO "7" 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.  \mneg{}\#(as)  <  1
10.  \#(bs)  <  1
\mvdash{}  as  =  bs


By

---

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

---

Home Index