Step
*
of Lemma
bag-summation-cons
∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].
∀[T:Type]. ∀[f:T ⟶ R]. ∀[b:bag(T)]. ∀[a:T]. (Σ(x∈a.b). f[x] = (f[a] add Σ(x∈b). f[x]) ∈ R)
supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
BY
{ (Auto
THEN Subst' a.b ~ {a} + b 0
THEN Try (Complete ((RepUR ``cons-bag bag-append single-bag`` 0 THEN Auto)))
THEN RWW "bag-summation-append bag-summation-single" 0
THEN Auto) }
Latex:
Latex:
\mforall{}[R:Type]. \mforall{}[add:R {}\mrightarrow{} R {}\mrightarrow{} R]. \mforall{}[zero:R].
\mforall{}[T:Type]. \mforall{}[f:T {}\mrightarrow{} R]. \mforall{}[b:bag(T)]. \mforall{}[a:T]. (\mSigma{}(x\mmember{}a.b). f[x] = (f[a] add \mSigma{}(x\mmember{}b). f[x]))
supposing IsMonoid(R;add;zero) \mwedge{} Comm(R;add)
By
Latex:
(Auto
THEN Subst' a.b \msim{} \{a\} + b 0
THEN Try (Complete ((RepUR ``cons-bag bag-append single-bag`` 0 THEN Auto)))
THEN RWW "bag-summation-append bag-summation-single" 0
THEN Auto)
Home
Index