---

Step * 1 2 1 1 1 1 1 of Lemma empty-bag-union


∀T:Type. ∀v:bag(T) List.  ((reduce(λl,l'. (l + l');{};v) = {} ∈ bag(T)) ⇒ (∀x:Top List. ((x ∈ v) ⇒ (x ~ {}))))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN skip{((RWO "cons_member" (-1) THENM D -1) THEN Auto)}) }

1
1. T : Type
2. u : bag(T)
3. v : bag(T) List
4. (reduce(λl,l'. (l + l');{};v) = {} ∈ bag(T)) ⇒ (∀x:Top List. ((x ∈ v) ⇒ (x ~ {})))
5. (u + reduce(λl,l'. (l + l');{};v)) = {} ∈ bag(T)
6. x : Top List
7. (x ∈ [u / v])
⊢ x ~ {}

---

Latex:

---

Latex:

\mforall{}T:Type.  \mforall{}v:bag(T)  List.    ((reduce(\mlambda{}l,l'.  (l  +  l');\{\};v)  =  \{\})  {}\mRightarrow{}  (\mforall{}x:Top  List.  ((x  \mmember{}  v)  {}\mRightarrow{}  (x  \msim{}  \{\})\000C)))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  skip\{((RWO  "cons\_member"  (-1)  THENM  D  -1)  THEN  Auto)\})

---

Home Index