---

Step * of Lemma bag-remove-size

∀[T:Type]
  ∀eq:EqDecider(T). ∀bs:bag(T). ∀x:T.
    ((x ↓∈ bs ∧ (#(bs - x) = (#(bs) - (#x in bs)) ∈ ℤ)) ∨ ((¬x ↓∈ bs) ∧ (#(bs - x) = #(bs) ∈ ℤ)))
BY
{ Auto }

1
1. [T] : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. x : T
⊢ (x ↓∈ bs ∧ (#(bs - x) = (#(bs) - (#x in bs)) ∈ ℤ)) ∨ ((¬x ↓∈ bs) ∧ (#(bs - x) = #(bs) ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}bs:bag(T).  \mforall{}x:T.
        ((x  \mdownarrow{}\mmember{}  bs  \mwedge{}  (\#(bs  -  x)  =  (\#(bs)  -  (\#x  in  bs))))  \mvee{}  ((\mneg{}x  \mdownarrow{}\mmember{}  bs)  \mwedge{}  (\#(bs  -  x)  =  \#(bs))))


By

---

Latex:
Auto

---

Home Index