(defun 4x^2 (x)
  (* 4 (* x x)))