(bfr-integer-length-s x) → ilen
Function:
(defun bfr-integer-length-s (x) (declare (xargs :guard (true-listp x))) (let ((__function__ 'bfr-integer-length-s)) (declare (ignorable __function__)) (b* (((mv ?changed res) (bfr-integer-length-s1 1 x))) res)))
Theorem:
(defthm true-listp-of-bfr-integer-length-s (b* ((ilen (bfr-integer-length-s x))) (true-listp ilen)) :rule-classes :type-prescription)
Theorem:
(defthm bfr-integer-length-s-correct (b* ((ilen (bfr-integer-length-s x))) (and (equal (bfr-list->s ilen env) (integer-length (bfr-list->s x env))))))
Theorem:
(defthm bfr-integer-length-s-deps (b* ((ilen (bfr-integer-length-s x))) (implies (and (not (pbfr-list-depends-on varname param x))) (and (not (pbfr-list-depends-on varname param ilen))))))