---

Step * 2 of Lemma bag-append-is-empty


1. T : Type
2. as : T List
3. bs : T List
4. (as + bs) = {} ∈ bag(T)
5. (||as|| + ||bs||) = 0 ∈ ℤ
⊢ bs = {} ∈ bag(T)
BY
{ (Thin (-2) THEN D 3 THEN Try (Fold `empty-bag` 0) THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  (as  +  bs)  =  \{\}
5.  (||as||  +  ||bs||)  =  0
\mvdash{}  bs  =  \{\}


By

---

Latex:
(Thin  (-2)  THEN  D  3  THEN  Try  (Fold  `empty-bag`  0)  THEN  Auto')

---

Home Index