---

Step * 2 of Lemma single-valued-bag-append


1. A : Type
2. as : bag(A)
3. bs : bag(A)
4. ∀x,y:A.  (x ↓∈ bs ⇒ y ↓∈ bs ⇒ (x = y ∈ A))
5. ∀x,y:A.  (x ↓∈ as ⇒ y ↓∈ as ⇒ (x = y ∈ A))
6. ∀a:A. (a ↓∈ as ∧ 0 < #(bs) ⇐⇒ a ↓∈ bs ∧ 0 < #(as))
7. x : A
8. y : A
9. x ↓∈ as
10. y ↓∈ bs
11. #(as) = 0 ∈ ℤ
12. #(bs) = 0 ∈ ℤ
⊢ x = y ∈ A
BY
{ ((InstLemma `bag-size-zero` [⌜A⌝;⌜as⌝]⋅ THENA Auto) THEN (RWO "-1" 9 THENA Auto) THEN BagMemberD 9) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  as  :  bag(A)
3.  bs  :  bag(A)
4.  \mforall{}x,y:A.    (x  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  y  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  (x  =  y))
5.  \mforall{}x,y:A.    (x  \mdownarrow{}\mmember{}  as  {}\mRightarrow{}  y  \mdownarrow{}\mmember{}  as  {}\mRightarrow{}  (x  =  y))
6.  \mforall{}a:A.  (a  \mdownarrow{}\mmember{}  as  \mwedge{}  0  <  \#(bs)  \mLeftarrow{}{}\mRightarrow{}  a  \mdownarrow{}\mmember{}  bs  \mwedge{}  0  <  \#(as))
7.  x  :  A
8.  y  :  A
9.  x  \mdownarrow{}\mmember{}  as
10.  y  \mdownarrow{}\mmember{}  bs
11.  \#(as)  =  0
12.  \#(bs)  =  0
\mvdash{}  x  =  y


By

---

Latex:
((InstLemma  `bag-size-zero`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (RWO  "-1"  9  THENA  Auto)  THEN  BagMemberD  9)

---

Home Index