---

Step * 1 1 1 1 2 of Lemma sum_aux-as-primrec


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. i : ℤ
5. f : {i..i + d-} ⟶ ℤ
6. i < i + d
7. k : ℤ
8. 0 < k
9. ∀v:ℤ. (primrec(k - 1;f[i] + v;λj,x. (x + f[(i + 1) + j])) ~ primrec(k - 1;v;λj,x. (x + f[i + j])) + f[i + (k - 1)])
10. v : ℤ
⊢ primrec(k;f[i] + v;λj,x. (x + f[(i + 1) + j])) ~ primrec(k;v;λj,x. (x + f[i + j])) + f[i + k]
BY
{ ((RWO  "primrec-unroll" 0 THENA Auto) THEN AutoSplit) }

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. i : ℤ
5. f : {i..i + d-} ⟶ ℤ
6. i < i + d
7. k : ℤ
8. ¬k < 1
9. 0 < k
10. ∀v:ℤ. (primrec(k - 1;f[i] + v;λj,x. (x + f[(i + 1) + j])) ~ primrec(k - 1;v;λj,x. (x + f[i + j])) + f[i + (k - 1)])
11. v : ℤ
⊢ primrec(k - 1;f[i] + v;λj,x. (x + f[(i + 1) + j])) + f[(i + 1) + (k - 1)] ~ (primrec(k - 1;v;λj,x. (x + f[i + j]))
+ f[i + (k - 1)])
+ f[i + k]

---

Latex:

---

Latex:

1.  d  :  \mBbbZ{}
2.  0  <  d
3.  \mforall{}[v,i:\mBbbZ{}].  \mforall{}[f:\{i..i  +  (d  -  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}].
          (sum\_aux(i  +  (d  -  1);v;i;x.f[x])  \msim{}  primrec(d  -  1;v;\mlambda{}j,x.  (x  +  f[i  +  j])))
4.  i  :  \mBbbZ{}
5.  f  :  \{i..i  +  d\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}
6.  i  <  i  +  d
7.  k  :  \mBbbZ{}
8.  0  <  k
9.  \mforall{}v:\mBbbZ{}
          (primrec(k  -  1;f[i]  +  v;\mlambda{}j,x.  (x  +  f[(i  +  1)  +  j]))  \msim{}  primrec(k  -  1;v;\mlambda{}j,x.  (x  +  f[i  +  j]))
          +  f[i  +  (k  -  1)])
10.  v  :  \mBbbZ{}
\mvdash{}  primrec(k;f[i]  +  v;\mlambda{}j,x.  (x  +  f[(i  +  1)  +  j]))  \msim{}  primrec(k;v;\mlambda{}j,x.  (x  +  f[i  +  j]))  +  f[i  +  k]


By

---

Latex:
((RWO    "primrec-unroll"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index