add(S(x),y) = S(add(x,y))
add(Z,y)    = y
