---

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


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 ~ {}
BY
{ ((RWO "bag-append-is-empty" (-3) THENA Auto) THEN (RWO "cons_member" (-1) THENM D -1) THEN Auto) }

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  bag(T)
3.  v  :  bag(T)  List
4.  (reduce(\mlambda{}l,l'.  (l  +  l');\{\};v)  =  \{\})  {}\mRightarrow{}  (\mforall{}x:Top  List.  ((x  \mmember{}  v)  {}\mRightarrow{}  (x  \msim{}  \{\})))
5.  (u  +  reduce(\mlambda{}l,l'.  (l  +  l');\{\};v))  =  \{\}
6.  x  :  Top  List
7.  (x  \mmember{}  [u  /  v])
\mvdash{}  x  \msim{}  \{\}


By

---

Latex:
((RWO  "bag-append-is-empty"  (-3)  THENA  Auto)  THEN  (RWO  "cons\_member"  (-1)  THENM  D  -1)  THEN  Auto)

---

Home Index