---

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