A
Function:
(defun abstract-*digit-star-*digit (tree) (declare (xargs :guard (treep tree))) (b* (((fun (fail)) (prog2$ (abstract-fail) (mv 0 (nati-finite 0)))) ((unless (tree-case tree :nonleaf)) (fail)) (treess (tree-nonleaf->branches tree)) ((unless (and (consp treess) (consp (cdr treess)) (consp (cddr treess)))) (fail)) (trees-min (car treess)) (trees-max (caddr treess)) (min (abstract-*digit trees-min)) (max (if (consp trees-max) (nati-finite (abstract-*digit trees-max)) (nati-infinity)))) (mv min max)))
Theorem:
(defthm natp-of-abstract-*digit-star-*digit.min (b* (((mv common-lisp::?min common-lisp::?max) (abstract-*digit-star-*digit tree))) (natp min)) :rule-classes :rewrite)
Theorem:
(defthm natip-of-abstract-*digit-star-*digit.max (b* (((mv common-lisp::?min common-lisp::?max) (abstract-*digit-star-*digit tree))) (natip max)) :rule-classes :rewrite)