page 1
1
Div2 is an inverse operation of double operation
We want to prove
(
M : Nat ) div2(2 * M) = M .
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
.
We show
div2(2 * 0) = 0
by
reduction
.
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
div2(2 * n0) = n0
.
We show
div2(2 * (s n0)) = s n0
by
reduction
.
And thus the main goal is proved.
Left
Up
Down
Right
This page was generated by Kumo on Tue Feb 13 19:36:02 PST 2001.
M
: Nat
)
div2(2 * M) = M .
