(bfr-integer-length-s1 offset x) → (mv not-done ilen)
Function:
(defun bfr-integer-length-s1 (offset x) (declare (xargs :guard (and (posp offset) (true-listp x)))) (let ((__function__ 'bfr-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) (bfr-integer-length-s1 (1+ offset) rest)) ((when (eq changed t)) (mv t res)) (change (bfr-xor first (car rest)))) (mv (bfr-or changed change) (bfr-ite-bss changed res (bfr-ite-bss change (i2v offset) nil))))))
Theorem:
(defthm true-listp-of-bfr-integer-length-s1.ilen (b* (((mv ?not-done ?ilen) (bfr-integer-length-s1 offset x))) (true-listp ilen)) :rule-classes :type-prescription)
Theorem:
(defthm bfr-integer-length-s1-correct (b* (((mv not-done ilen) (bfr-integer-length-s1 offset x))) (and (equal (bfr-eval not-done env) (and (not (equal (bfr-list->s x env) 0)) (not (equal (bfr-list->s x env) -1)))) (equal (bfr-list->s ilen env) (if (or (equal (bfr-list->s x env) 0) (equal (bfr-list->s x env) -1)) 0 (+ -1 (pos-fix offset) (integer-length (bfr-list->s x env))))))))
Theorem:
(defthm bfr-integer-length-s1-deps (b* (((mv not-done ilen) (bfr-integer-length-s1 offset x))) (implies (and (not (pbfr-list-depends-on varname param x))) (and (not (pbfr-depends-on varname param not-done)) (not (pbfr-list-depends-on varname param ilen))))))