A
Function:
(defun abstract-dec-val (tree) (declare (xargs :guard (treep tree))) (b* (((fun (fail)) (prog2$ (abstract-fail) (num-val-direct (num-base-dec) nil))) ((unless (tree-case tree :nonleaf)) (fail)) (treess (tree-nonleaf->branches tree)) ((unless (and (consp treess) (consp (cdr treess)) (consp (cddr treess)))) (fail)) (trees-1st-num (cadr treess)) (1st-num (abstract-*digit trees-1st-num)) (trees-rest (caddr treess)) ((unless (consp trees-rest)) (fail)) (tree-rest (car trees-rest)) (rest (abstract-dec-val-rest tree-rest))) (if (nat-listp rest) (num-val-direct (num-base-dec) (cons 1st-num rest)) (num-val-range (num-base-dec) 1st-num rest))))
Theorem:
(defthm num-val-p-of-abstract-dec-val (b* ((num-val (abstract-dec-val tree))) (num-val-p num-val)) :rule-classes :rewrite)