(sv::aig-integer-length-s1 offset x) → (mv not-done ilen)
Function:
(defun sv::aig-integer-length-s1 (offset x) (declare (xargs :guard (and (posp offset) (true-listp x)))) (let ((__function__ 'sv::aig-integer-length-s1)) (declare (ignorable __function__)) (b* (((mv first rest end) (first/rest/end x)) (offset (lposfix offset)) ((when end) (mv nil nil)) ((mv changed res) (sv::aig-integer-length-s1 (1+ offset) rest)) ((when (eq changed t)) (mv t res)) (change (acl2::aig-xor first (car rest)))) (mv (acl2::aig-or changed change) (sv::aig-ite-bss changed res (sv::aig-ite-bss change (i2v offset) nil))))))
Theorem:
(defthm sv::true-listp-of-aig-integer-length-s1.ilen (b* (((mv ?not-done ?ilen) (sv::aig-integer-length-s1 offset x))) (true-listp ilen)) :rule-classes :type-prescription)
Theorem:
(defthm sv::aig-integer-length-s1-correct (b* (((mv not-done ilen) (sv::aig-integer-length-s1 offset x))) (and (equal (acl2::aig-eval not-done env) (and (not (equal (sv::aig-list->s x env) 0)) (not (equal (sv::aig-list->s x env) -1)))) (equal (sv::aig-list->s ilen env) (if (or (equal (sv::aig-list->s x env) 0) (equal (sv::aig-list->s x env) -1)) 0 (+ -1 (pos-fix offset) (integer-length (sv::aig-list->s x env))))))))