We want to prove
(  M
: Nat
)
( N
: Nat
)
M = 2 * N
or
M = (2 * N) + 1 .
We use
induction on
M
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
M
=
0
.
-
Let
N
=
0
. Then we need to prove
| |
0 = 2 * 0
or
0 = (2 * 0) + 1
.
|
-
Disjunction
elimination
yields 2 subgoals:
-
0 = 2 * 0
-
0 = (2 * 0) + 1
-
Induction case: assume the assertion for
M
=
N0
,
and then prove it for
M
=
s N0
.
-
Quantifier
elimination introduces the new constant(s)
n0
:
Nat
.
-
Implication
elimination
assumes
| |
(N
: Nat
)
n0 = 2 * N
or
n0 = (2 * N) + 1
.
|
-
By skolemization,
we can get
| |
n0 = 2 * n1
or
n0 = (2 * n1) + 1
|
from the following hypothesis
| |
(N
: Nat
)
n0 = 2 * N
or
n0 = (2 * N) + 1
.
|
-
We do case analysis on
| |
n0 = 2 * n1
or
n0 = (2 * n1) + 1
,
|
and we get 2 cases:
-
Case:
n0 = 2 * n1
.
-
We change the equation
n0 = 2 * n1
to rewriting rule.
-
Let
N
=
n1
. Then we need to prove
| |
s n0 = 2 * n1
or
s n0 = (2 * n1) + 1
.
|
-
Disjunction
elimination
yields 2 subgoals:
-
s n0 = 2 * n1
-
s n0 = (2 * n1) + 1
-
Case:
n0 = (2 * n1) + 1
.
-
We change the equation
n0 = (2 * n1) + 1
to rewriting rule.
-
Let
N
=
n1 + 1
. Then we need to prove
| |
s n0 = 2 * (n1 + 1)
or
s n0 = (2 * (n1 + 1)) + 1
.
|
-
Disjunction
elimination
yields 2 subgoals:
-
s n0 = 2 * (n1 + 1)
-
s n0 = (2 * (n1 + 1)) + 1
And thus the main goal is proved.
|
