Hi Dan,
here's what I proved so far in constructing the add function.

By the way, I think it's remarkable that the function used in the
construction is "commutative" in its arguments, i.e. g(a,b)=g(b,a) for
all natural numbers a,b. (I proved this using the function definition
only!)

Regards,

Thomas

[Download proof at www.dcproof.com/AddFunction_new_TH.proof ]