		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

4veclist-from-bitlist-log-rec

Signature
(4veclist-from-bitlist-log-rec n origs bits) → (mv 4vecs rest-origs rest-bits)
Arguments: n — Guard (natp n).; origs — Guard (a4veclist-p origs).; bits — Guard (true-listp bits).
Returns: 4vecs — Type (true-listp 4vecs).; rest-origs — Type (implies (a4veclist-p origs) (a4veclist-p rest-origs)).; rest-bits — Type (implies (true-listp bits) (true-listp rest-bits)).

Definitions and Theorems

Function: 4veclist-from-bitlist-log-rec

(defun 4veclist-from-bitlist-log-rec (n origs bits)
 (declare (xargs :guard (and (natp n)
                             (a4veclist-p origs)
                             (true-listp bits))))
 (declare (xargs :guard (<= (nfix n) (len origs))))
 (let ((__function__ '4veclist-from-bitlist-log-rec))
  (declare (ignorable __function__))
  (b* (((when (zp n)) (mv nil origs bits))
       ((a4vec x) (car origs))
       (rest-origs (cdr origs))
       ((mv 4vec1 rest-bits)
        (4vec-from-bitlist (len x.upper)
                           (len x.lower)
                           bits))
       (n (1- n))
       (halfn (ash n -1))
       (restn (- n halfn))
       ((mv 4vecs-half1 rest-origs rest-bits)
        (4veclist-from-bitlist-log-rec halfn rest-origs rest-bits))
       ((mv 4vecs-half2 rest-origs rest-bits)
        (4veclist-from-bitlist-log-rec restn rest-origs rest-bits)))
    (mv (cons 4vec1 (append 4vecs-half1 4vecs-half2))
        rest-origs rest-bits))))

Theorem: true-listp-of-4veclist-from-bitlist-log-rec.4vecs

(defthm true-listp-of-4veclist-from-bitlist-log-rec.4vecs
  (b* (((mv ?4vecs ?rest-origs ?rest-bits)
        (4veclist-from-bitlist-log-rec n origs bits)))
    (true-listp 4vecs))
  :rule-classes :rewrite)

Theorem: return-type-of-4veclist-from-bitlist-log-rec.rest-origs

(defthm return-type-of-4veclist-from-bitlist-log-rec.rest-origs
  (b* (((mv ?4vecs ?rest-origs ?rest-bits)
        (4veclist-from-bitlist-log-rec n origs bits)))
    (implies (a4veclist-p origs)
             (a4veclist-p rest-origs)))
  :rule-classes :rewrite)

Theorem: return-type-of-4veclist-from-bitlist-log-rec.rest-bits

(defthm return-type-of-4veclist-from-bitlist-log-rec.rest-bits
  (b* (((mv ?4vecs ?rest-origs ?rest-bits)
        (4veclist-from-bitlist-log-rec n origs bits)))
    (implies (true-listp bits)
             (true-listp rest-bits)))
  :rule-classes :rewrite)

Theorem: 4veclist-from-bitlist-log-rec-nthcdrs-origs

(defthm 4veclist-from-bitlist-log-rec-nthcdrs-origs
  (b* (((mv ?4vecs ?rest-origs ?rest-bits)
        (4veclist-from-bitlist-log-rec n origs bits)))
    (equal rest-origs (nthcdr n origs))))

Theorem: 4veclist-from-bitlist-log-rec-rest-bits

(defthm 4veclist-from-bitlist-log-rec-rest-bits
  (b* (((mv ?4vecs ?rest-origs ?rest-bits)
        (4veclist-from-bitlist-log-rec n origs bits)))
    (equal rest-bits
           (nthcdr (a4veclist-length (take n origs))
                   bits))))

Theorem: 4veclist-from-bitlist-log-rec-correct

(defthm 4veclist-from-bitlist-log-rec-correct
  (b* (((mv ?4vecs ?rest-origs ?rest-bits)
        (4veclist-from-bitlist-log-rec n origs bits)))
    (implies (<= (nfix n) (len origs))
             (equal 4vecs
                    (4veclist-from-bitlist (take n origs)
                                           bits)))))

Theorem: 4veclist-from-bitlist-in-terms-of-4veclist-from-bitlist-log-rec

(defthm
    4veclist-from-bitlist-in-terms-of-4veclist-from-bitlist-log-rec
  (b* ((n (len origs))
       ((mv ?4vecs ?rest-origs ?rest-bits)
        (4veclist-from-bitlist-log-rec n origs bits)))
    (equal (4veclist-from-bitlist origs bits)
           4vecs)))