Square Sum of the First n Natural Number
We want to prove
N:Nat (squsum(N) * 6 = (N * N * N * 2) + (N * N * 3) + N)
.
We use induction on
Nat
to prove this goal. For this, we use the induction scheme based on signature
{0,s}
for
Nat
. Induction requires that we do the following:
Base case : prove assertion for
N = 0
.
Show
squsum(0) * 6 = (0 * 0 * 0 * 2) + (0 * 0 * 3) + 0
by reduction .
Induction case : prove assertion for
N = s M
assume it for
N = M
.
Quantifier elimination introduces new
constant m :Nat
.
Implication elimination assumes
squsum(m) * 6 = (m * m * m * 2) + (m * m * 3) + m
.
Change hypothesis
squsum(m) * 6 = (m * m * m * 2) + (m * m * 3) + m
to rewritng rule.
Show
squsum(s m) * 6 = (s m * s m * s m * 2) + (s m * s m * 3) + s m
by reduction .
This page was generated
by Kumo on
Mon May 04 15:21:47 PDT 1998