Natural Numbers

We give an example of an induction proof over natural numbers generated automatically by our prover. In the following the symbol denotes the addition of the natural numbers, denotes the succesor of the natural number (i.e.) and 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:

PROPOSITION:

under the assumptions

,

.