		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

A4veclist-length

Signature
(a4veclist-length x) → len
Arguments: x — Guard (a4veclist-p x).
Returns: len — Type (natp len).

Definitions and Theorems

Function: a4veclist-length

(defun a4veclist-length (x)
  (declare (xargs :guard (a4veclist-p x)))
  (let ((__function__ 'a4veclist-length))
    (declare (ignorable __function__))
    (if (atom x)
        0
      (+ (len (a4vec->upper (car x)))
         (len (a4vec->lower (car x)))
         (a4veclist-length (cdr x))))))

Theorem: natp-of-a4veclist-length

(defthm natp-of-a4veclist-length
  (b* ((len (a4veclist-length x)))
    (natp len))
  :rule-classes :rewrite)

Theorem: a4veclist-length-of-append

(defthm a4veclist-length-of-append
  (equal (a4veclist-length (append x y))
         (+ (a4veclist-length x)
            (a4veclist-length y))))

Theorem: a4veclist-length-of-a4veclist-fix-x

(defthm a4veclist-length-of-a4veclist-fix-x
  (equal (a4veclist-length (a4veclist-fix x))
         (a4veclist-length x)))

Theorem: a4veclist-length-a4veclist-equiv-congruence-on-x

(defthm a4veclist-length-a4veclist-equiv-congruence-on-x
  (implies (a4veclist-equiv x x-equiv)
           (equal (a4veclist-length x)
                  (a4veclist-length x-equiv)))
  :rule-classes :congruence)