---

Step * 1 1 1 1 of Lemma sum-unroll


1. f : Base
2. m : ℕ
⊢ sum_aux(m + 1;0;0;x.f[x]) ~ sum_aux(m;0;0;x.f[x]) + f[m]
BY
{ TACTIC:Assert ⌜∀d:ℕ. ∀s,b:ℤ.  (sum_aux(s + d + 1;b;s;x.f[x]) ~ sum_aux(s + d;b;s;x.f[x]) + f[s + d])⌝⋅ }

1
.....assertion..... 
1. f : Base
2. m : ℕ
⊢ ∀d:ℕ. ∀s,b:ℤ.  (sum_aux(s + d + 1;b;s;x.f[x]) ~ sum_aux(s + d;b;s;x.f[x]) + f[s + d])

2
1. f : Base
2. m : ℕ
3. ∀d:ℕ. ∀s,b:ℤ.  (sum_aux(s + d + 1;b;s;x.f[x]) ~ sum_aux(s + d;b;s;x.f[x]) + f[s + d])
⊢ sum_aux(m + 1;0;0;x.f[x]) ~ sum_aux(m;0;0;x.f[x]) + f[m]

---

Latex:

---

Latex:

1.  f  :  Base
2.  m  :  \mBbbN{}
\mvdash{}  sum\_aux(m  +  1;0;0;x.f[x])  \msim{}  sum\_aux(m;0;0;x.f[x])  +  f[m]


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}s,b:\mBbbZ{}.
                                  (sum\_aux(s  +  d  +  1;b;s;x.f[x])  \msim{}  sum\_aux(s  +  d;b;s;x.f[x])  +  f[s  +  d])\mkleeneclose{}\mcdot{}

---

Home Index