---

Step * of Lemma bag-count-drop

∀[T:Type]
  ∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).
    ((x ↓∈ bs ∧ ((#x in bag-drop(eq;bs;x)) = ((#x in bs) - 1) ∈ ℕ))
    ∨ ((¬x ↓∈ bs) ∧ ((#x in bag-drop(eq;bs;x)) = (#x in bs) ∈ ℕ)))
BY
{ TACTIC:(Auto
          THEN (InstLemma `bag-remove1-property` [⌜T⌝;⌜eq⌝;⌜x⌝;⌜bs⌝]⋅ THENA Auto)
          THEN ParallelLast
          THEN ExRepD
          THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)@i
3. x : T@i
4. bs : bag(T)@i
5. as : bag(T)
6. bs = ({x} + as) ∈ bag(T)
7. bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?)
⊢ x ↓∈ bs

2
1. T : Type
2. eq : EqDecider(T)@i
3. x : T@i
4. bs : bag(T)@i
5. as : bag(T)
6. bs = ({x} + as) ∈ bag(T)
7. bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?)
8. x ↓∈ bs
⊢ (#x in bag-drop(eq;bs;x)) = ((#x in bs) - 1) ∈ ℕ

3
1. T : Type
2. eq : EqDecider(T)@i
3. x : T@i
4. bs : bag(T)@i
5. ¬x ↓∈ bs
6. bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?)
7. ¬x ↓∈ bs
⊢ (#x in bag-drop(eq;bs;x)) = (#x in bs) ∈ ℕ

---

Latex:

---

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


By

---

Latex:
TACTIC:(Auto
                THEN  (InstLemma  `bag-remove1-property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ParallelLast
                THEN  ExRepD
                THEN  Auto)

---

Home Index