		Search-engine friendly clone of the ACL2 documentation.

Utilities

Add-to-each

Add an offset to each member of a list.

Signature
(add-to-each offset x) → *
Arguments: offset — Guard (integerp offset).; x — Guard (integer-listp x).

This is used in the development of bitset-members.

Definitions and Theorems

Function: add-to-each

(defun add-to-each (offset x)
  (declare (xargs :guard (and (integerp offset)
                              (integer-listp x))))
  (let ((__function__ 'add-to-each))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (+ offset (car x))
            (add-to-each offset (cdr x))))))

Theorem: add-to-each-when-atom

(defthm add-to-each-when-atom
  (implies (atom x)
           (equal (add-to-each offset x) nil)))

Theorem: add-to-each-of-cons

(defthm add-to-each-of-cons
  (equal (add-to-each offset (cons a x))
         (cons (+ offset a)
               (add-to-each offset x))))

Theorem: add-to-each-of-zero

(defthm add-to-each-of-zero
  (implies (integer-listp x)
           (equal (add-to-each 0 x) x)))

Theorem: add-to-each-of-append

(defthm add-to-each-of-append
  (equal (add-to-each offset (append x y))
         (append (add-to-each offset x)
                 (add-to-each offset y))))

Theorem: add-to-each-of-add-to-each

(defthm add-to-each-of-add-to-each
  (equal (add-to-each a (add-to-each b x))
         (add-to-each (+ a b) x)))