---

Step * 1 of Lemma sum_aux_wf

.....assertion..... 
∀d:ℕ. ∀[v,i:ℤ]. ∀[f:{i..i + d-} ⟶ ℤ].  (sum_aux(i + d;v;i;x.f[x]) ∈ ℤ)
BY
{ (InductionOnNat THEN Auto THEN RecUnfold `sum_aux` 0 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]) ∈ ℤ)
4. v : ℤ
5. i : ℤ
6. f : {i..i + d-} ⟶ ℤ
7. i < i + d
⊢ eval v' = f[i] + v in
  eval i' = i + 1 in
    sum_aux(i + d;v';i';x.f[x]) ∈ ℤ

---

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])  \mmember{}  \mBbbZ{})


By

---

Latex:
(InductionOnNat  THEN  Auto  THEN  RecUnfold  `sum\_aux`  0  THEN  AutoSplit)

---

Home Index