		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-integer-length-s1

Signature
(bfr-integer-length-s1 offset x) → (mv not-done ilen)
Arguments: offset — Guard (posp offset).; x — Guard (true-listp x).
Returns: ilen — Type (true-listp ilen).

Definitions and Theorems

Function: bfr-integer-length-s1

(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: true-listp-of-bfr-integer-length-s1.ilen

(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: bfr-integer-length-s1-correct

(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: bfr-integer-length-s1-deps

(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))))))