---

Step * 1 of Lemma sum_aux-as-primrec

.....assertion..... 
∀d:ℕ. ∀[v,i:ℤ]. ∀[f:{i..i + d-} ⟶ ℤ].  (sum_aux(i + d;v;i;x.f[x]) ~ primrec(d;v;λj,x. (x + f[i + j])))
BY
{ (InductionOnNat
   THEN (UnivCD THENA Auto)
   THEN RecUnfold `sum_aux` 0⋅
   THEN (RWO  "primrec-unroll" 0 THENA Auto)
   THEN Reduce 0
   THEN AutoSplit
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) }

1
1. d : ℤ
2. 0 < d
3. ∀[v,i:ℤ]. ∀[f:{i..i + (d - 1)-} ⟶ ℤ].  (sum_aux(i + (d - 1);v;i;x.f[x]) ~ primrec(d - 1;v;λj,x. (x + f[i + j])))
4. v : ℤ
5. i : ℤ
6. f : {i..i + d-} ⟶ ℤ
7. i < i + d
⊢ sum_aux(i + d;f[i] + v;i + 1;x.f[x]) ~ primrec(d - 1;v;λj,x. (x + f[i + j])) + f[i + (d - 1)]

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}d:\mBbbN{}
    \mforall{}[v,i:\mBbbZ{}].  \mforall{}[f:\{i..i  +  d\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}].    (sum\_aux(i  +  d;v;i;x.f[x])  \msim{}  primrec(d;v;\mlambda{}j,x.  (x  +  f[i  +  j])))


By

---

Latex:
(InductionOnNat
  THEN  (UnivCD  THENA  Auto)
  THEN  RecUnfold  `sum\_aux`  0\mcdot{}
  THEN  (RWO    "primrec-unroll"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index