---

Step * 4 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
{ ((Assert (#(as) = 1 ∈ ℤ) ∧ (#(bs) = 1 ∈ ℤ) BY
          Auto)
   THEN D -1
   THEN RepeatFor 2 (ThinTrivial)
   THEN RWO "bag-size-one" 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.  \mneg{}\#(bs)  <  1
\mvdash{}  as  =  bs


By

---

Latex:
((Assert  (\#(as)  =  1)  \mwedge{}  (\#(bs)  =  1)  BY
                Auto)
  THEN  D  -1
  THEN  RepeatFor  2  (ThinTrivial)
  THEN  RWO  "bag-size-one"  0
  THEN  Auto)

---

Home Index