We want to prove
(  M
N
: Nat
)
(2 * M) * M = N * N
implies
( K
: Nat
)
N = 2 * K .
We take the following steps:
-
Quantifier
elimination introduces the new constant(s)
m, n
:
Nat
.
-
Implication
elimination
assumes
-
We introduce the lemma
| |
( M
: Nat
)
(N
: Nat
)
M = 2 * N
or
M = (2 * N) + 1.
|
Click here to see its proof.
-
In the following hypothesis
| |
( M
: Nat
)
(N
: Nat
)
M = 2 * N
or
M = (2 * N) + 1
,
|
let
M
=
n
, we get
| |
(N
: Nat
)
n = 2 * N
or
n = (2 * N) + 1
,
|
-
By skolemization,
we can get
| |
n = 2 * n1
or
n = (2 * n1) + 1
|
from the following hypothesis
| |
(N
: Nat
)
n = 2 * N
or
n = (2 * N) + 1
.
|
-
We do case analysis on
| |
n = 2 * n1
or
n = (2 * n1) + 1
,
|
and we get 2 cases:
-
Case:
n = 2 * n1
.
-
We change the equation
n = 2 * n1
to rewriting rule.
-
Let
K
=
n1
. Then we need to prove
-
We show
n = 2 * n1
by reduction.
Case:
n = (2 * n1) + 1
.
-
Then we apply equation
n = (2 * n1) + 1
to the hypothesis
and get
| |
(2 * m) * m = s (((((n1 * n1) + (n1 * n1)) + ((n1 * n1) + (n1 * n1))) + (n1 + n1)) + (n1 + n1))
,
|
-
We introduce the lemma
| |
( M
: Nat
)
mod2(2 * M) = 0.
|
Click here to see its proof.
-
We introduce the lemma
| |
( M
: Nat
)
mod2((2 * M) + 1) = 1.
|
Click here to see its proof.
-
We apply an operation
mod2
to the both sides of the equation in the hypothesis:
(2 * m) * m = s (((((n1 * n1) + (n1 * n1)) + ((n1 * n1) + (n1 * n1))) + (n1 + n1)) + (n1 + n1))
,
and get
0 = s 0
.
-
We show
0 = s 0
is false by
reduction.
And thus the main goal is proved.
|
