---

Step * of Lemma sum-unroll-1

∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  (Σ(f[x] | x < n) ~ if (n =z 0) then 0 else Σ(f[x] | x < n - 1) + f[n - 1] fi )
BY
{ (((UnivCD THENA Auto) THEN AutoSplit) THEN (RWO "sum-as-primrec" 0 THENA Auto)) }

1
1. n : ℕ
2. f : ℕn ⟶ ℤ
3. n = 0 ∈ ℤ
⊢ primrec(n;0;λj,x. (x + f[j])) ~ 0

2
1. n : {1...}
2. f : ℕn ⟶ ℤ
⊢ primrec(n;0;λj,x. (x + f[j])) ~ primrec(n - 1;0;λj,x. (x + f[j])) + f[n - 1]

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].
    (\mSigma{}(f[x]  |  x  <  n)  \msim{}  if  (n  =\msubz{}  0)  then  0  else  \mSigma{}(f[x]  |  x  <  n  -  1)  +  f[n  -  1]  fi  )


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  AutoSplit)  THEN  (RWO  "sum-as-primrec"  0  THENA  Auto))

---

Home Index