(defun f1 (x)
  (declare (xargs :guard (and (integerp x)
                              (evenp x))))
  (/ x 2))

(defun f2 (x)
  (f1 (/ x 2)))

(defun f3 (x)
  (f2 (/ x 2)))

(f3 12)

(wet (f3 12))

; Warning: The rest of this demo is intended to give a sense of
; the programming capabilities provided by ACL2.  Don't feel
; obliged to understand any of this in depth; we're going for
; flavor here....

; ACL2 is programmed in itself.  We'll get a sense of how that
; goes by looking at the source definition of wet and
; books/misc/wet.lisp.