Increasing by Adding Positive Number

page 1

Increasing by Adding Positive Number

We want to prove
( M : Nat )
( K : NzNat ) (M + K) > 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 introduce the lemma

( K : NzNat ) K > 0.

Click here to see its proof.
Quantifier elimination introduces the new constant(s) k : NzNat .
We show (0 + k) > 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

( K : NzNat ) (n0 + K) > n0 .
Quantifier elimination introduces the new constant(s) k : NzNat .
We show ((s n0) + k) > (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:09 PST 2001.