---

Step * of Lemma sum-l_sum

∀[n:ℕ]. ∀[a:ℕn ⟶ ℤ].  (Σ(a[i] | i < n) = l_sum(map(λi.a[i];upto(n))) ∈ ℤ)
BY
{ (Auto
   THEN (InstLemma `l_sum-sum` [⌜ℕn⌝;⌜upto(n)⌝;⌜λi.a[i]⌝]⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN Thin (-1)
   THEN Reduce 0) }

1
1. n : ℕ
2. a : ℕn ⟶ ℤ
⊢ Σ(a[i] | i < n) = Σ(a[upto(n)[i]] | i < ||upto(n)||) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].    (\mSigma{}(a[i]  |  i  <  n)  =  l\_sum(map(\mlambda{}i.a[i];upto(n))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `l\_sum-sum`  [\mkleeneopen{}\mBbbN{}n\mkleeneclose{};\mkleeneopen{}upto(n)\mkleeneclose{};\mkleeneopen{}\mlambda{}i.a[i]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  Thin  (-1)
  THEN  Reduce  0)

---

Home Index