(find-a-base-case term fns fake-fns prefer-then state) → base-case
Function:
(defun find-a-base-case (term fns fake-fns prefer-then state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbol-listp fns) (and (symbol-alistp fake-fns) (nat-listp (strip-cdrs fake-fns))) (booleanp prefer-then)))) (let ((__function__ 'find-a-base-case)) (declare (ignorable __function__)) (mv-let (erp all-base largest) (find-a-base-case-aux term (append fns (strip-cars fake-fns)) prefer-then (acl2::add-fake-fns-to-world fake-fns (w state)) state) (cond (erp (hard-error 'find-a-base-case "Cannot find a base case!" nil)) (all-base term) (t largest)))))