CMPU-145, Spring 2013
Proof from class
March 6, 2013


Theorem.  Given the following rules for the addition function:

              (1) x + 0 = x          for all natural numbers x
              (2) x + Sy = S(x+y)    for all natural numbers x and y

          it follows that 0 + x = x for all natural numbers x.

Proof.  Let P(x) be the proposition:  0 + x = x.  

        We want to show that P(x) holds for all natural numbers x.

        Base Case:  P(0):  0 + 0 = 0.

          LHS = 0 + 0
              = 0,          by rule 1
              = RHS

        Recursive Case:  Assume P(k):  0 + k = k.

          Prove that P(Sk):  0 + Sk = Sk.

            LHS = 0 + Sk
                = S(0+k),   by rule 2
                = Sk,       by P(k)
                = RHS