---

Step * 1 of Lemma bag-remove-size


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) ∈ ℤ))
BY
{ xxxxxxxxx((InstLemma `decidable__bag-member` [⌜T⌝;⌜x⌝;⌜bs⌝]⋅ THENA Auto)
            THEN xxx(UnfoldTopAb (-1) THEN ParallelLast THEN Auto)xxx
            )xxxxxxxxx }

1
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. x : T
5. x ↓∈ bs
6. x ↓∈ bs
⊢ #(bs - x) = (#(bs) - (#x in bs)) ∈ ℤ

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  eq  :  EqDecider(T)
3.  bs  :  bag(T)
4.  x  :  T
\mvdash{}  (x  \mdownarrow{}\mmember{}  bs  \mwedge{}  (\#(bs  -  x)  =  (\#(bs)  -  (\#x  in  bs))))  \mvee{}  ((\mneg{}x  \mdownarrow{}\mmember{}  bs)  \mwedge{}  (\#(bs  -  x)  =  \#(bs)))


By

---

Latex:
xxxxxxxxx((InstLemma  `decidable\_\_bag-member`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
                    THEN  xxx(UnfoldTopAb  (-1)  THEN  ParallelLast  THEN  Auto)xxx
                    )xxxxxxxxx

---

Home Index