(aabf-integer-length-s x man) → (mv ilen new-man)
Function:
(defun aabf-integer-length-s (x man) (declare (xargs :guard (true-listp x))) (declare (xargs :guard (and (aabflist-p x man)))) (let ((__function__ 'aabf-integer-length-s)) (declare (ignorable __function__)) (b* (((mv ?changed res man) (aabf-integer-length-s1 1 x man))) (mv res man))))
Theorem:
(defthm trivial-theorem-about-aabf-integer-length-s (b* nil (b* ((?ignore (aabf-integer-length-s x man))) t)) :rule-classes nil)
Theorem:
(defthm true-listp-of-aabf-integer-length-s.ilen (b* (((mv ?ilen ?new-man) (aabf-integer-length-s x man))) (true-listp ilen)) :rule-classes :type-prescription)
Theorem:
(defthm aabf-extension-p-of-aabf-integer-length-s (b* (((mv ?ilen ?new-man) (aabf-integer-length-s x man))) (aabf-extension-p new-man man)))
Theorem:
(defthm aabf-p-of-aabf-integer-length-s (b* (((mv ilen new-man) (aabf-integer-length-s x man))) (implies (and (aabflist-p x man)) (and (aabflist-p ilen new-man)))))
Theorem:
(defthm aabf-eval-of-aabf-integer-length-s (b* (((mv ilen new-man) (aabf-integer-length-s x man))) (implies (and (aabflist-p x man)) (and (equal (bools->int (aabflist-eval ilen env new-man)) (integer-length (bools->int (aabflist-eval x env man))))))))
Theorem:
(defthm aabf-pred-of-aabf-integer-length-s (b* (((mv ilen new-man) (aabf-integer-length-s x man))) (implies (and (aabflist-p x man) (aabflist-pred x man)) (and (aabflist-pred ilen new-man)))))