26 lines
443 B
Plaintext
26 lines
443 B
Plaintext
sum: THEORY
|
|
BEGIN
|
|
n: VAR nat
|
|
f, g: VAR [nat -> nat]
|
|
|
|
sum(f, n): RECURSIVE nat =
|
|
IF n = 0
|
|
THEN 0
|
|
ELSE f(n-1) + sum(f, n - 1)
|
|
ENDIF
|
|
MEASURE n
|
|
|
|
sum_plus: LEMMA
|
|
sum((lambda n: f(n) + g(n)), n) = sum(f, n) + sum(g, n)
|
|
|
|
square(n): nat = n*n
|
|
|
|
sum_of_squares: LEMMA
|
|
6 * sum(square, n+1) = n * (n + 1) * (2*n + 1)
|
|
|
|
cube(n): nat = n*n*n
|
|
|
|
sum_of_cubes: LEMMA
|
|
4 * sum(cube, n+1) = n*n*(n+1)*(n+1)
|
|
END sum
|