double(Z)    = Z
double(S(x)) = S(S(double(x)))