The function we'll project.
(f x) → *
Function: f
(defun f (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'f)) (declare (ignorable acl2::__function__)) (let ((x (ifix x))) (+ x x))))
