---

Step * 1 1 1 1 2 of Lemma sum-unroll


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]
BY
{ TACTIC:((InstHyp [⌜m⌝;⌜0⌝;⌜0⌝] (-1)⋅ THENA Auto) THEN NthHypSq (-1) THEN RepeatFor 2 (EqCD) THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Base
2.  m  :  \mBbbN{}
3.  \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])
\mvdash{}  sum\_aux(m  +  1;0;0;x.f[x])  \msim{}  sum\_aux(m;0;0;x.f[x])  +  f[m]


By

---

Latex:
TACTIC:((InstHyp  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                THEN  NthHypSq  (-1)
                THEN  RepeatFor  2  (EqCD)
                THEN  Auto)

---

Home Index