A Relation between Sum and Subtract

page 1

A Relation between Sum and Subtract

We want to prove
( N M : Nat ) (M + N) - N = M .
We use induction on N 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 N = 0 .

Quantifier elimination introduces the new constant(s) m : Nat .
We show (m + 0) - 0 = m by reduction.

Induction case: assume the assertion for N = N0 , and then prove it for N = s N0 .

Quantifier elimination introduces the new constant(s) n0 : Nat .
Implication elimination assumes

( M : Nat ) (M + n0) - n0 = M .
Quantifier elimination introduces the new constant(s) m : Nat .
We show (m + (s n0)) - (s n0) = m 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:06 PST 2001.