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