		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Nat-bool-a4vec-vars

Signature
(nat-bool-a4vec-vars x) → *
Arguments: x — Guard (nat-bool-a4vec-p! x).

Definitions and Theorems

Function: nat-bool-a4vec-vars

(defun nat-bool-a4vec-vars (x)
  (declare (xargs :guard (nat-bool-a4vec-p! x)))
  (let ((__function__ 'nat-bool-a4vec-vars))
    (declare (ignorable __function__))
    (b* (((a4vec x) x))
      (append (nat-bool-list-nats x.upper)
              (nat-bool-list-nats x.lower)))))

Theorem: nat-bool-a4vec-vars-of-a4vec-fix-x

(defthm nat-bool-a4vec-vars-of-a4vec-fix-x
  (equal (nat-bool-a4vec-vars (a4vec-fix x))
         (nat-bool-a4vec-vars x)))

Theorem: nat-bool-a4vec-vars-a4vec-equiv-congruence-on-x

(defthm nat-bool-a4vec-vars-a4vec-equiv-congruence-on-x
  (implies (a4vec-equiv x x-equiv)
           (equal (nat-bool-a4vec-vars x)
                  (nat-bool-a4vec-vars x-equiv)))
  :rule-classes :congruence)