Step
*
1
1
1
1
1
of Lemma
sum-unroll
.....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])
BY
{ TACTIC:(InductionOnNat THEN (UnivCD THENA Auto)) }
1
1. f : Base
2. m : ℕ
3. d : ℤ
4. s : ℤ
5. b : ℤ
⊢ sum_aux(s + 0 + 1;b;s;x.f[x]) ~ sum_aux(s + 0;b;s;x.f[x]) + f[s + 0]
2
1. f : Base
2. m : ℕ
3. d : ℤ
4. 0 < d
5. ∀s,b:ℤ. (sum_aux(s + (d - 1) + 1;b;s;x.f[x]) ~ sum_aux(s + (d - 1);b;s;x.f[x]) + f[s + (d - 1)])
6. s : ℤ
7. b : ℤ
⊢ sum_aux(s + d + 1;b;s;x.f[x]) ~ sum_aux(s + d;b;s;x.f[x]) + f[s + d]
Latex:
Latex:
.....assertion.....
1. f : Base
2. m : \mBbbN{}
\mvdash{} \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])
By
Latex:
TACTIC:(InductionOnNat THEN (UnivCD THENA Auto))
Home
Index