Computes a constant upper bound for the symbolic value of x.
(aig-list->s-upper-bound x) → upper-bound
Function:
(defun aig-list->s-upper-bound (x) (declare (xargs :guard (true-listp x))) (let ((__function__ 'aig-list->s-upper-bound)) (declare (ignorable __function__)) (b* (((mv first rest end) (gl::first/rest/end x)) ((when end) (if (eq first t) -1 0)) (rest-bound (aig-list->s-upper-bound rest))) (logcons (if (eq first nil) 0 1) rest-bound))))
Theorem:
(defthm integerp-of-aig-list->s-upper-bound (b* ((upper-bound (aig-list->s-upper-bound x))) (integerp upper-bound)) :rule-classes :type-prescription)
Theorem:
(defthm aig-list->s-upper-bound-correct (<= (aig-list->s x env) (aig-list->s-upper-bound x)) :rule-classes :linear)
Theorem:
(defthm aig-list->s-upper-bound-lower-bound-when-sign-bit-non-t (implies (not (equal (aig-sign-s x) t)) (<= 0 (aig-list->s-upper-bound x))) :rule-classes :linear)
Theorem:
(defthm aig-list->s-upper-bound-of-list-fix-x (equal (aig-list->s-upper-bound (list-fix x)) (aig-list->s-upper-bound x)))
Theorem:
(defthm aig-list->s-upper-bound-list-equiv-congruence-on-x (implies (list-equiv x x-equiv) (equal (aig-list->s-upper-bound x) (aig-list->s-upper-bound x-equiv))) :rule-classes :congruence)