A commonly used measure for justifying recursion
All characters and symbols have
Function:
(defun acl2-count (x) (declare (xargs :guard t)) (if (consp x) (+ 1 (acl2-count (car x)) (acl2-count (cdr x))) (if (rationalp x) (if (integerp x) (integer-abs x) (+ (integer-abs (numerator x)) (denominator x))) (if (complex/complex-rationalp x) (+ 1 (acl2-count (realpart x)) (acl2-count (imagpart x))) (if (stringp x) (length x) 0)))))