---

Step * 1 1 of Lemma sub-bag_antisymmetry

.....equality..... 
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 + cs) ∈ bag(T)
11. #(bs) = (#(as) + #(cs)) ∈ ℤ
⊢ cs ~ []
BY
{ (Fold `empty-bag` 0 THEN (BLemma `bag-size-zero`   THEN Auto')⋅) }

---

Latex:

---

Latex:
.....equality..... 
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  +  cs)
11.  \#(bs)  =  (\#(as)  +  \#(cs))
\mvdash{}  cs  \msim{}  []


By

---

Latex:
(Fold  `empty-bag`  0  THEN  (BLemma  `bag-size-zero`      THEN  Auto')\mcdot{})

---

Home Index