---

Step * 1 of Lemma sum1


1. f : ℕ1 ⟶ ℤ
⊢ primrec(1 - 0;0;λj,x. (x + f[0 + j])) = f[0] ∈ ℤ
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}1  {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  primrec(1  -  0;0;\mlambda{}j,x.  (x  +  f[0  +  j]))  =  f[0]


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index