?

Log in

XAN YOU LOSE - Ari's Journal [entries|archive|friends|userinfo]
Ari

[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

XAN YOU LOSE [Jun. 7th, 2006|02:15 pm]
Ari
They do do the proofs that way!

|------
(FORALL (n: nat):
sum(n, square) = (n * (n + 1) * (2 * n + 1)) / 6)

Rerunning step: (INDUCT-AND-SIMPLIFY "n")
square rewrites square(0)
to 0
sum rewrites sum(0, square)
to 0
square rewrites square(1+j!1)
to 1+j!1+(j!1*j!1+j!1)
sum rewrites sum(1+j!1, square)
to 1+sum(j!1, square)+j!1*j!1+j!1+j!1
By induction on n, and by repeatedly rewriting and simplifying,
Q.E.D.
linkReply