(aabf-integer-length-s1 offset x man) → (mv not-done ilen new-man)
Function:
(defun aabf-integer-length-s1 (offset x man) (declare (xargs :guard (and (posp offset) (true-listp x)))) (declare (xargs :guard (and (aabflist-p x man)))) (let ((__function__ 'aabf-integer-length-s1)) (declare (ignorable __function__)) (b* (((mv first rest end) (aabf-first/rest/end x)) (offset (lposfix offset)) ((when end) (mv (aabf-false) nil man)) ((mv changed rest-len man) (aabf-integer-length-s1 (1+ offset) rest man)) ((when (aabf-syntactically-equal changed (aabf-true))) (mv (aabf-true) rest-len man)) ((mv change man) (aabf-xor first (aabf-car rest) man)) ((mv ans man) (aabf-nest (aabf-ite-bss-fn changed rest-len (aabf-ite-bss-fn change (int->aabflist offset) nil)) man)) ((mv full-change man) (aabf-nest (aabf-or changed change) man))) (mv full-change ans man))))
Theorem:
(defthm trivial-theorem-about-aabf-integer-length-s1 (b* nil (b* ((?ignore (aabf-integer-length-s1 offset x man))) t)) :rule-classes nil)
Theorem:
(defthm true-listp-of-aabf-integer-length-s1.ilen (b* (((mv ?not-done ?ilen ?new-man) (aabf-integer-length-s1 offset x man))) (true-listp ilen)) :rule-classes :type-prescription)
Theorem:
(defthm aabf-extension-p-of-aabf-integer-length-s1 (b* (((mv ?not-done ?ilen ?new-man) (aabf-integer-length-s1 offset x man))) (aabf-extension-p new-man man)))
Theorem:
(defthm aabf-p-of-aabf-integer-length-s1 (b* (((mv not-done ilen new-man) (aabf-integer-length-s1 offset x man))) (implies (and (aabflist-p x man)) (and (aabf-p not-done new-man) (aabflist-p ilen new-man)))))
Theorem:
(defthm aabf-eval-of-aabf-integer-length-s1 (b* (((mv not-done ilen new-man) (aabf-integer-length-s1 offset x man))) (implies (and (aabflist-p x man)) (and (equal (aabf-eval not-done env new-man) (and (not (equal (bools->int (aabflist-eval x env man)) 0)) (not (equal (bools->int (aabflist-eval x env man)) -1)))) (equal (bools->int (aabflist-eval ilen env new-man)) (if (or (equal (bools->int (aabflist-eval x env man)) 0) (equal (bools->int (aabflist-eval x env man)) -1)) 0 (+ -1 (pos-fix offset) (integer-length (bools->int (aabflist-eval x env man))))))))))
Theorem:
(defthm aabf-pred-of-aabf-integer-length-s1 (b* (((mv not-done ilen new-man) (aabf-integer-length-s1 offset x man))) (implies (and (aabflist-p x man) (aabflist-pred x man)) (and (aabf-pred not-done new-man) (aabflist-pred ilen new-man)))))