---

Step * of Lemma sum-as-primrec

∀[k:ℕ]. ∀[f:ℕk ⟶ ℤ].  (Σ(f[x] | x < k) ~ primrec(k;0;λj,x. (x + f[j])))
BY
{ (Auto THEN Unfold `sum` 0 THEN RWO "sum_aux-as-primrec" 0 THEN Try (EqCD) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[f:\mBbbN{}k  {}\mrightarrow{}  \mBbbZ{}].    (\mSigma{}(f[x]  |  x  <  k)  \msim{}  primrec(k;0;\mlambda{}j,x.  (x  +  f[j])))


By

---

Latex:
(Auto  THEN  Unfold  `sum`  0  THEN  RWO  "sum\_aux-as-primrec"  0  THEN  Try  (EqCD)  THEN  Auto)

---

Home Index