---

Step * of Lemma bag-append-is-empty

∀[T:Type]. ∀as,bs:bag(T).  uiff((as + bs) = {} ∈ bag(T);(as = {} ∈ bag(T)) ∧ (bs = {} ∈ bag(T)))
BY
{ (Auto
   THEN Try ((HypSubst' (-2) 0 THEN Reduce 0 THEN Auto))
   THEN (Assert #(as + bs) = #({}) ∈ ℤ BY
               Auto)
   THEN Reduce (-1)
   THEN RWO "bag-size-append" (-1)
   THEN Auto
   THEN Unfold `bag-size` -1
   THEN (BagToList 2 THEN Try (Fold `bag-size` 0) THEN Auto)
   THEN BagToList 3
   THEN Try (Fold `bag-size` 0)
   THEN Auto) }

1
1. T : Type
2. as : T List
3. bs : T List
4. (as + bs) = {} ∈ bag(T)
5. (||as|| + ||bs||) = 0 ∈ ℤ
⊢ as = {} ∈ bag(T)

2
1. T : Type
2. as : T List
3. bs : T List
4. (as + bs) = {} ∈ bag(T)
5. (||as|| + ||bs||) = 0 ∈ ℤ
⊢ bs = {} ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}as,bs:bag(T).    uiff((as  +  bs)  =  \{\};(as  =  \{\})  \mwedge{}  (bs  =  \{\}))


By

---

Latex:
(Auto
  THEN  Try  ((HypSubst'  (-2)  0  THEN  Reduce  0  THEN  Auto))
  THEN  (Assert  \#(as  +  bs)  =  \#(\{\})  BY
                          Auto)
  THEN  Reduce  (-1)
  THEN  RWO  "bag-size-append"  (-1)
  THEN  Auto
  THEN  Unfold  `bag-size`  -1
  THEN  (BagToList  2  THEN  Try  (Fold  `bag-size`  0)  THEN  Auto)
  THEN  BagToList  3
  THEN  Try  (Fold  `bag-size`  0)
  THEN  Auto)

---

Home Index