---

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


1. f : Base
2. m : ℕ
3. d : ℤ
4. s : ℤ
5. b : ℤ
6. s < s + 1
⊢ eval v' = f[s] + b in
  sum_aux(s + 1;v';s + 1;x.f[x]) ~ sum_aux(s + 0;b;s;x.f[x]) + f[s + 0]
BY
{ (RecUnfold `sum_aux` 0
   THEN RepeatFor 2 (AutoSplit)
   THEN (Subst' s + 0 ~ s 0 THENA Auto)
   THEN (GenConcl ⌜f[s] = x ∈ Base⌝⋅ THENA Auto)) }

1
1. f : Base
2. m : ℕ
3. d : ℤ
4. s : ℤ
5. ¬s < s + 0
6. ¬s + 1 < s + 1
7. b : ℤ
8. s < s + 1
9. x : Base
10. f[s] = x ∈ Base
⊢ eval v' = x + b in
  v' ~ b + x

---

Latex:

---

Latex:

1.  f  :  Base
2.  m  :  \mBbbN{}
3.  d  :  \mBbbZ{}
4.  s  :  \mBbbZ{}
5.  b  :  \mBbbZ{}
6.  s  <  s  +  1
\mvdash{}  eval  v'  =  f[s]  +  b  in
    sum\_aux(s  +  1;v';s  +  1;x.f[x])  \msim{}  sum\_aux(s  +  0;b;s;x.f[x])  +  f[s  +  0]


By

---

Latex:
(RecUnfold  `sum\_aux`  0
  THEN  RepeatFor  2  (AutoSplit)
  THEN  (Subst'  s  +  0  \msim{}  s  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}f[s]  =  x\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index