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.
