---

Step * of Lemma sum_split

∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[m:ℕn + 1].  (Σ(f[x] | x < n) = (Σ(f[x] | x < m) + Σ(f[x + m] | x < n - m)) ∈ ℤ)
BY
{ (SumToPrimrec
   THEN Auto
   THEN (InstLemma `primrec_add` [⌜ℤ⌝;⌜n - m⌝;⌜m⌝;⌜0⌝;⌜λj,x. (x + f[j])⌝]⋅ THENA Auto)
   THEN (Subst' (n - m) + m ~ n -1 THENA Auto)
   THEN HypSubst' (-1) 0
   THEN Reduce 0
   THEN (GenConclTerm ⌜primrec(m;0;λj,x. (x + f[j]))⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(n - m) = k ∈ ℕ⌝⋅ THENA Auto)) }

1
1. n : ℕ
2. f : ℕn ⟶ ℤ
3. m : ℕn + 1
4. primrec(n;0;λj,x. (x + f[j])) ~ primrec(n - m;primrec(m;0;λj,x. (x + f[j]));λi,t. ((λj,x. (x + f[j])) (i + m) t))
5. v : ℤ
6. primrec(m;0;λj,x. (x + f[j])) = v ∈ ℤ
7. k : ℕ
8. (n - m) = k ∈ ℕ
⊢ primrec(k;v;λi,t. (t + f[i + m])) = (v + primrec(k;0;λj,x. (x + f[j + m]))) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[m:\mBbbN{}n  +  1].    (\mSigma{}(f[x]  |  x  <  n)  =  (\mSigma{}(f[x]  |  x  <  m)  +  \mSigma{}(f[x  +  m]  |  x  <  n  -  m)))


By

---

Latex:
(SumToPrimrec
  THEN  Auto
  THEN  (InstLemma  `primrec\_add`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}n  -  m\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}\mlambda{}j,x.  (x  +  f[j])\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  (n  -  m)  +  m  \msim{}  n  -1  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  Reduce  0
  THEN  (GenConclTerm  \mkleeneopen{}primrec(m;0;\mlambda{}j,x.  (x  +  f[j]))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(n  -  m)  =  k\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index