Step
*
of Lemma
sum-equal-terms
No Annotations
∀[n:ℕ]. ∀[a:ℕn ⟶ ℤ]. ∀[m:ℕ]. ∀[b:ℕm ⟶ ℤ].
Σ(a[i] | i < n) = Σ(b[j] | j < m) ∈ ℤ
supposing permutation(ℤ;filter(λx.(¬b(x =z 0));map(λi.a[i];upto(n)));filter(λx.(¬b(x =z 0));map(λj.b[j];upto(m))))
BY
{ (Auto THEN (RWO "sum-l_sum" 0 THEN Auto) THEN MoveToConcl (-1)) }
Latex:
Latex:
No Annotations
\mforall{}[n:\mBbbN{}]. \mforall{}[a:\mBbbN{}n {}\mrightarrow{} \mBbbZ{}]. \mforall{}[m:\mBbbN{}]. \mforall{}[b:\mBbbN{}m {}\mrightarrow{} \mBbbZ{}].
\mSigma{}(a[i] | i < n) = \mSigma{}(b[j] | j < m)
supposing permutation(\mBbbZ{};filter(\mlambda{}x.(\mneg{}\msubb{}(x =\msubz{} 0));map(\mlambda{}i.a[i];upto(n)));
filter(\mlambda{}x.(\mneg{}\msubb{}(x =\msubz{} 0));map(\mlambda{}j.b[j];upto(m))))
By
Latex:
(Auto THEN (RWO "sum-l\_sum" 0 THEN Auto) THEN MoveToConcl (-1))
Home
Index