---

Step * of Lemma bag-remove-size-member-no-repeats

∀[T:Type]
  ∀eq:EqDecider(T). ∀bs:bag(T). ∀x:T.  (#(bs - x) = (#(bs) - 1) ∈ ℤ) supposing (x ↓∈ bs and bag-no-repeats(T;bs))
BY
{ xxx(InstLemma `bag-remove-size` []
      THEN RepeatFor 4 (ParallelLast')
      THEN D -1
      THEN Auto
      THEN HypSubst'(-3) 0
      THEN EqCD
      THEN EAuto 1)xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}bs:bag(T).  \mforall{}x:T.
        (\#(bs  -  x)  =  (\#(bs)  -  1))  supposing  (x  \mdownarrow{}\mmember{}  bs  and  bag-no-repeats(T;bs))


By

---

Latex:
xxx(InstLemma  `bag-remove-size`  []
        THEN  RepeatFor  4  (ParallelLast')
        THEN  D  -1
        THEN  Auto
        THEN  HypSubst'(-3)  0
        THEN  EqCD
        THEN  EAuto  1)xxx

---

Home Index