Find a base-case within a translated term.
(find-a-base-case-translated-aux term fns prefer-then) → (mv erp all-base largest)
If none of
A term may have many base-cases. We bias our search toward larger
base-cases, and toward ``then'' branches if
If
Function:
(defun find-a-base-case-translated-aux (term fns prefer-then) (declare (xargs :guard (and (pseudo-termp term) (symbol-listp fns) (booleanp prefer-then)))) (let ((__function__ 'find-a-base-case-translated-aux)) (declare (ignorable __function__)) (b* (((unless (consp term)) (mv nil t nil)) ((unless (eq 'if (car term))) (if (acl2::expr-calls-some-fn fns term) (mv t nil nil) (mv nil t nil))) ((mv erp-then all-base-then largest-then) (find-a-base-case-translated-aux (farg2 term) fns prefer-then)) ((mv erp-else all-base-else largest-else) (find-a-base-case-translated-aux (farg3 term) fns prefer-then))) (cond (erp-then (if erp-else (mv erp-else nil nil) (mv nil nil (if all-base-else (farg3 term) largest-else)))) (erp-else (mv nil nil (if all-base-then (farg2 term) largest-then))) (all-base-then (if all-base-else (if (not (acl2::expr-calls-some-fn fns (farg1 term))) (mv nil t nil) (mv nil nil (if prefer-then (farg2 term) (farg3 term)))) (mv nil nil (farg2 term)))) (all-base-else (mv nil nil (farg3 term))) (prefer-then (mv nil nil largest-then)) (t (mv nil nil largest-else))))))
Theorem:
(defthm booleanp-of-find-a-base-case-translated-aux.all-base (b* (((mv ?erp ?all-base ?largest) (find-a-base-case-translated-aux term fns prefer-then))) (booleanp all-base)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-find-a-base-case-translated-aux.largest (implies (and (pseudo-termp term) (symbol-listp fns) (booleanp prefer-then)) (b* (((mv ?erp ?all-base ?largest) (find-a-base-case-translated-aux term fns prefer-then))) (pseudo-termp largest))) :rule-classes :rewrite)