Step
*
of Lemma
rsum_linearity-rsub
∀[n,m:ℤ]. ∀[x,y:{n..m + 1-} ⟶ ℝ]. (Σ{x[k] - y[k] | n≤k≤m} = (Σ{x[k] | n≤k≤m} - Σ{y[k] | n≤k≤m}))
BY
{ (Auto
THEN Unfold `rsum` 0
THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
THEN (GenConcl ⌜[n, m + 1) = L ∈ ({n..m + 1-} List)⌝⋅ THENA Auto)
THEN ((CallByValueReduce 0 THENA Auto)
THEN Unfold `rsub` 0
THEN (RWO "radd-list-linearity1" 0⋅ THENA Auto)
THEN ((RWO "rminus-as-rmul" 0 THEN Auto)
THEN RWO "radd-list-linearity2<" 0
THEN Auto
THEN BLemma `radd_functionality`
THEN Auto)⋅)⋅) }
1
1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. y : {n..m + 1-} ⟶ ℝ
5. L : {n..m + 1-} List
6. [n, m + 1) = L ∈ ({n..m + 1-} List)
⊢ radd-list(map(λk.-(y[k]);L)) = radd-list(map(λk.(r(-1) * y[k]);L))
Latex:
Latex:
\mforall{}[n,m:\mBbbZ{}]. \mforall{}[x,y:\{n..m + 1\msupminus{}\} {}\mrightarrow{} \mBbbR{}]. (\mSigma{}\{x[k] - y[k] | n\mleq{}k\mleq{}m\} = (\mSigma{}\{x[k] | n\mleq{}k\mleq{}m\} - \mSigma{}\{y[k] | n\mleq{}k\mleq{}m\}))
By
Latex:
(Auto
THEN Unfold `rsum` 0
THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
THEN (GenConcl \mkleeneopen{}[n, m + 1) = L\mkleeneclose{}\mcdot{} THENA Auto)
THEN ((CallByValueReduce 0 THENA Auto)
THEN Unfold `rsub` 0
THEN (RWO "radd-list-linearity1" 0\mcdot{} THENA Auto)
THEN ((RWO "rminus-as-rmul" 0 THEN Auto)
THEN RWO "radd-list-linearity2<" 0
THEN Auto
THEN BLemma `radd\_functionality`
THEN Auto)\mcdot{})\mcdot{})
Home
Index