Natural Numbers

We give an example of an induction proof over natural numbers generated automatically by our prover. In the following the symbol [Graphics:submitted.nbgr261.gif] denotes the addition of the natural numbers, [Graphics:submitted.nbgr262.gif]denotes the succesor of the natural number [Graphics:submitted.nbgr263.gif](i.e.[Graphics:submitted.nbgr264.gif]) and [Graphics:submitted.nbgr265.gif] denotes the equality predicate.

The theorem that we are proving states that adding 0 to the left of a natural numer, leaves the number unchanged. (Note that the definition of the addition of natural numbers states that adding 0 to the right of a natural number leaves this one unchanged (0 is neutral element wrt. the adition of the natural numbers). The proof of the theorem follows:


[Graphics:submitted.nbgr266.gif] [Graphics:submitted.nbgr267.gif]

under the assumptions

[Graphics:submitted.nbgr268.gif] [Graphics:submitted.nbgr269.gif],

[Graphics:submitted.nbgr270.gif] [Graphics:submitted.nbgr271.gif].