---

Step * 1 2 of Lemma sub-bag_antisymmetry


1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. c1 : bag(T)
5. as = (bs + c1) ∈ bag(T)
6. cs : bag(T)
7. bs = (as + cs) ∈ bag(T)
8. as = (bs + c1) ∈ bag(T)
9. #(as) = (#(bs) + #(c1)) ∈ ℤ
10. bs = (as + []) ∈ bag(T)
11. #(bs) = (#(as) + #(cs)) ∈ ℤ
⊢ as = bs ∈ bag(T)
BY
{ (Fold `empty-bag` (-2) THEN RWO "bag-append-empty" (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  bag(T)
3.  bs  :  bag(T)
4.  c1  :  bag(T)
5.  as  =  (bs  +  c1)
6.  cs  :  bag(T)
7.  bs  =  (as  +  cs)
8.  as  =  (bs  +  c1)
9.  \#(as)  =  (\#(bs)  +  \#(c1))
10.  bs  =  (as  +  [])
11.  \#(bs)  =  (\#(as)  +  \#(cs))
\mvdash{}  as  =  bs


By

---

Latex:
(Fold  `empty-bag`  (-2)  THEN  RWO  "bag-append-empty"  (-2)  THEN  Auto)

---

Home Index