---

Step * of Lemma sum_aux-as-primrec

∀[v,i,k:ℤ]. ∀[f:{i..k-} ⟶ ℤ].  sum_aux(k;v;i;x.f[x]) ~ primrec(k - i;v;λj,x. (x + f[i + j])) supposing i ≤ k
BY
{ Assert ⌜∀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])))⌝⋅ }

1
.....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])))

2
1. ∀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])))
⊢ ∀[v,i,k:ℤ]. ∀[f:{i..k-} ⟶ ℤ].  sum_aux(k;v;i;x.f[x]) ~ primrec(k - i;v;λj,x. (x + f[i + j])) supposing i ≤ k

---

Latex:

---

Latex:
\mforall{}[v,i,k:\mBbbZ{}].  \mforall{}[f:\{i..k\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}].
    sum\_aux(k;v;i;x.f[x])  \msim{}  primrec(k  -  i;v;\mlambda{}j,x.  (x  +  f[i  +  j]))  supposing  i  \mleq{}  k


By

---

Latex:
Assert  \mkleeneopen{}\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])))\mkleeneclose{}\mcdot{}

---

Home Index