Step
*
1
of Lemma
bag-summation-append
1. R : Type
2. add : R ⟶ R ⟶ R
3. zero : R
4. IsMonoid(R;add;zero)
5. Comm(R;add)
6. T : Type
7. f : T ⟶ R
8. c : bag(T)
9. bs : T List
⊢ Σ(x∈bs + c). f[x] = (Σ(x∈bs). f[x] add Σ(x∈c). f[x]) ∈ R
BY
{ (RenameVar `L' (-1)
THEN MoveToConcl (-2)
THEN MoveToConcl (-1)
THEN InductionOnLast
THEN Try (Fold `single-bag` 0)
THEN Folds ``single-bag empty-bag bag-append single-bag`` 0
THEN RWW "bag-combine-empty-left bag-summation-empty" 0
THEN Auto
THEN Try ((Reduce 0 THEN Symmetry THEN D 4 THEN CompleteAuto))⋅
THEN (Assert Σ(x∈firstn(||L|| - 1;L)). f[x] ∈ R BY
(GenConclAtAddrType ⌜bag(T)⌝ [2;3]⋅ THEN Auto))
THEN RWW "bag-append-assoc -3" 0
THEN Auto
THEN GenConclAtAddr [2;2]
THEN Thin (-1))⋅ }
1
1. R : Type
2. add : R ⟶ R ⟶ R
3. zero : R
4. IsMonoid(R;add;zero)
5. Comm(R;add)
6. T : Type
7. f : T ⟶ R
8. L : T List
9. ¬↑null(L)
10. ||L|| ≥ 1
11. ∀c:bag(T). (Σ(x∈firstn(||L|| - 1;L) + c). f[x] = (Σ(x∈firstn(||L|| - 1;L)). f[x] add Σ(x∈c). f[x]) ∈ R)
12. c : bag(T)
13. Σ(x∈firstn(||L|| - 1;L)). f[x] ∈ R
14. v : R
⊢ (v add Σ(x∈{last(L)} + c). f[x]) = ((v add Σ(x∈{last(L)}). f[x]) add Σ(x∈c). f[x]) ∈ R
Latex:
Latex:
1. R : Type
2. add : R {}\mrightarrow{} R {}\mrightarrow{} R
3. zero : R
4. IsMonoid(R;add;zero)
5. Comm(R;add)
6. T : Type
7. f : T {}\mrightarrow{} R
8. c : bag(T)
9. bs : T List
\mvdash{} \mSigma{}(x\mmember{}bs + c). f[x] = (\mSigma{}(x\mmember{}bs). f[x] add \mSigma{}(x\mmember{}c). f[x])
By
Latex:
(RenameVar `L' (-1)
THEN MoveToConcl (-2)
THEN MoveToConcl (-1)
THEN InductionOnLast
THEN Try (Fold `single-bag` 0)
THEN Folds ``single-bag empty-bag bag-append single-bag`` 0
THEN RWW "bag-combine-empty-left bag-summation-empty" 0
THEN Auto
THEN Try ((Reduce 0 THEN Symmetry THEN D 4 THEN CompleteAuto))\mcdot{}
THEN (Assert \mSigma{}(x\mmember{}firstn(||L|| - 1;L)). f[x] \mmember{} R BY
(GenConclAtAddrType \mkleeneopen{}bag(T)\mkleeneclose{} [2;3]\mcdot{} THEN Auto))
THEN RWW "bag-append-assoc -3" 0
THEN Auto
THEN GenConclAtAddr [2;2]
THEN Thin (-1))\mcdot{}
Home
Index