We want to prove
(  N
: Nat
)
6 * sumsq(N) = (((2 * N) * N) * N) + (((3 * N) * N) + N) .
We use
induction on
N
to prove this goal.
For this, we use the
induction
scheme based on the signature
{
0, s
}
for
Nat.
Induction requires that we do the following:
-
Base case: prove the assertion for
N
=
0
.
-
We show
6 * sumsq(0) = (((2 * 0) * 0) * 0) + (((3 * 0) * 0) + 0)
by reduction.
-
Induction case: assume the assertion for
N
=
N0
,
and then prove it for
N
=
s N0
.
-
Quantifier
elimination introduces the new constant(s)
n0
:
Nat
.
-
Implication
elimination
assumes
| |
6 * sumsq(n0) = (((2 * n0) * n0) * n0) + (((3 * n0) * n0) + n0)
.
|
-
We show
6 * sumsq(s n0) = (((2 * (s n0)) * (s n0)) * (s n0)) + (((3 * (s n0)) * (s n0)) + (s n0))
by reduction.
And thus the main goal is proved.
|
