		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

4veclist-from-bitlist

Signature
(4veclist-from-bitlist origs bits) → 4vecs
Arguments: origs — Guard (a4veclist-p origs).; bits — Guard (true-listp bits).
Returns: 4vecs — Type (4veclist-p 4vecs).

Definitions and Theorems

Function: 4veclist-from-bitlist

(defun 4veclist-from-bitlist (origs bits)
  (declare (xargs :guard (and (a4veclist-p origs)
                              (true-listp bits))))
  (let ((__function__ '4veclist-from-bitlist))
    (declare (ignorable __function__))
    (b* (((when (atom origs)) nil)
         ((a4vec x) (car origs))
         ((mv first restbits)
          (4vec-from-bitlist (len x.upper)
                             (len x.lower)
                             bits)))
      (cons first
            (4veclist-from-bitlist (cdr origs)
                                   restbits)))))

Theorem: 4veclist-p-of-4veclist-from-bitlist

(defthm 4veclist-p-of-4veclist-from-bitlist
  (b* ((4vecs (4veclist-from-bitlist origs bits)))
    (4veclist-p 4vecs))
  :rule-classes :rewrite)

Theorem: 4veclist-from-bitlist-correct

(defthm 4veclist-from-bitlist-correct
 (equal (4veclist-from-bitlist x
                               (aig-eval-list (a4veclist->aiglist x)
                                              env))
        (a4veclist-eval x env)))

Theorem: 4veclist-from-bitlist-of-a4veclist-fix-origs

(defthm 4veclist-from-bitlist-of-a4veclist-fix-origs
  (equal (4veclist-from-bitlist (a4veclist-fix origs)
                                bits)
         (4veclist-from-bitlist origs bits)))

Theorem: 4veclist-from-bitlist-a4veclist-equiv-congruence-on-origs

(defthm 4veclist-from-bitlist-a4veclist-equiv-congruence-on-origs
  (implies (a4veclist-equiv origs origs-equiv)
           (equal (4veclist-from-bitlist origs bits)
                  (4veclist-from-bitlist origs-equiv bits)))
  :rule-classes :congruence)