---

Step * of Lemma bag-size-partition

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  (#(bs) = Σ(x∈bag-remove-repeats(eq;bs)). (#x in bs) ∈ ℤ)
BY
{ TACTIC:(Auto
          THEN (InstLemma `bag-summation-partition`
                 [⌜T⌝;⌜ℤ⌝;⌜T⌝;⌜λx,y. (x + y)⌝;⌜0⌝;⌜bs⌝;⌜eq⌝;⌜λ2x.1⌝;⌜bag-remove-repeats(eq;bs)⌝]⋅
                THENA (RepUR ``so_apply`` 0
                       THEN Auto
                       THEN Try (RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto)))
                       THEN Try (((RW assert_pushdownC (-2) THENA Auto) THEN RW assert_pushdownC (-1) THEN Auto))
                       THEN D -1
                       THEN With ⌜x⌝ (D 0)⋅
                       THEN EAuto 1)
                )
          ) }

1
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. Σ(x∈bs). 1 = Σ(z∈bag-remove-repeats(eq;bs)). Σ(x∈[x∈bs|eq[x;z]]). 1 ∈ ℤ
⊢ #(bs) = Σ(x∈bag-remove-repeats(eq;bs)). (#x in bs) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].    (\#(bs)  =  \mSigma{}(x\mmember{}bag-remove-repeats(eq;bs)).  (\#x  in  bs))


By

---

Latex:
TACTIC:(Auto
                THEN  (InstLemma  `bag-summation-partition`
                              [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  (x  +  y)\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.1\mkleeneclose{};\mkleeneopen{}bag-remove-repeats(eq;bs)\mkleeneclose{}]\mcdot{}
                            THENA  (RepUR  ``so\_apply``  0
                                          THEN  Auto
                                          THEN  Try  (RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto)))
                                          THEN  Try  (((RW  assert\_pushdownC  (-2)  THENA  Auto)
                                                                THEN  RW  assert\_pushdownC  (-1)
                                                                THEN  Auto))
                                          THEN  D  -1
                                          THEN  With  \mkleeneopen{}x\mkleeneclose{}  (D  0)\mcdot{}
                                          THEN  EAuto  1)
                            )
                )

---

Home Index