Fromal Reasoning - Solution

We use induction over the natural numbers.

Base case:

  addNats 0
    = {addNats.1}
  0
    = {sumList.1} 
  sumList []
    = {natList.1} 
  sumList (natList 0)

Stepping case:

Provided that Equation holds for a fixed n >= 0, we now demonstrate that it also holds for n+1:

  addNats (n + 1)
    = {n+1>0   and  addNats.2} 
  (n + 1) + addNats (n + 1 - 1)}
    = {Arithmetic} 
  (n + 1) + addNats n
    = {Provision} 
  (n + 1) + sumList (natList n)
    = {sumList.2} 
  sumList ((n + 1) : (natList n))
    = {Arithmetic} 
  sumList ((n + 1) : (natList (n + 1 - 1)))
    = {natList}.2} 
  sumList (natList (n + 1))

QED

Gabriele Keller

Last modified: Mon Oct 29 13:51:55 EST 2001