-- adds two natural numbers
add :: Nat -> Nat -> Nat
add      Z          Z    =            Z
add      Z       (S Z)   =         (S Z)
add      Z     (S(S Z))  =       (S(S Z))
add      Z   (S(S(S Z))) =     (S(S(S Z)))
add   (S Z)         Z    =         (S Z)
add   (S Z)      (S Z)   =       (S(S Z))
add   (S Z)    (S(S Z))  =     (S(S(S Z)))
add   (S Z)  (S(S(S Z))) =   (S(S(S(S Z))))
add (S(S Z))     (S Z)   =     (S(S(S Z)))
add (S(S Z))        Z    =       (S(S Z))
add (S(S Z))   (S(S Z))  =   (S(S(S(S Z))))
add (S(S Z)) (S(S(S Z))) = (S(S(S(S(S Z)))))
