-- multiplies two numbers
mult :: Nat -> Nat -> Nat
mult        Z           Z    =                      Z
mult        Z        (S Z)   =                      Z
mult        Z      (S(S Z))  =                      Z
mult        Z    (S(S(S Z))) =                      Z
mult     (S Z)          Z    =                      Z
mult     (S Z)       (S Z)   =                   (S Z)
mult     (S Z)     (S(S Z))  =                 (S(S Z))
mult     (S Z)   (S(S(S Z))) =               (S(S(S Z)))
mult   (S(S Z))         Z    =                      Z
mult   (S(S Z))      (S Z)   =                 (S(S Z))
mult   (S(S Z))    (S(S Z))  =             (S(S(S(S Z))))
mult   (S(S Z))  (S(S(S Z))) =         (S(S(S(S(S(S Z))))))
mult (S(S(S Z)))        Z    =                      Z
mult (S(S(S Z)))     (S Z)   =               (S(S(S Z)))
mult (S(S(S Z)))   (S(S Z))  =         (S(S(S(S(S(S Z))))))
mult (S(S(S Z))) (S(S(S Z))) =   (S(S(S(S(S(S(S(S(S Z)))))))))

-- BK for mult
multAdd :: Nat -> Nat -> Nat
multAdd (Z) (Z) = Z
multAdd (S Z) (Z) = S Z
multAdd (S Z) (S(Z)) = S(S Z)
multAdd (S Z) (S(S(Z))) = S (S(S Z))
multAdd (S(S Z)) (Z) = S(S Z)
multAdd (S(S Z)) (S(S(Z))) = S(S(S(S Z)))
multAdd (S(S Z)) (S(S(S(S(Z))))) = S (S(S(S(S(S(S Z))))))
multAdd (S(S(S Z))) (Z) = S(S(S Z))
multAdd (S(S(S Z))) (S(S(S(Z)))) = S (S(S(S(S(S(S Z))))))
multAdd (S(S(S Z))) (S(S(S(S(S(S(S(Z)))))))) = S (S(S(S(S(S(S(S(S(S Z)))))))))