		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

Aig-head-of-concat

Signature
(aig-head-of-concat concat-width lsbs msbs width) → *
Arguments: concat-width — Guard (true-listp concat-width).; lsbs — Guard (true-listp lsbs).; msbs — Guard (true-listp msbs).; width — Guard (posp width).

Definitions and Theorems

Function: aig-head-of-concat

(defun aig-head-of-concat (concat-width lsbs msbs width)
 (declare (xargs :guard (and (true-listp concat-width)
                             (true-listp lsbs)
                             (true-listp msbs)
                             (posp width))))
 (let ((__function__ 'aig-head-of-concat))
  (declare (ignorable __function__))
  (b* ((width (lposfix width))
       ((when (atom concat-width))
        (aig-logext-ns width msbs))
       (rev-shift (rev concat-width))
       (sign-bit (car rev-shift))
       (rev-shift (cdr rev-shift))
       (msbs-len (len msbs)))
   (aig-ite-bss
    sign-bit
    (b* ((const-rsh (ash 1 (len rev-shift)))
         (lsbs (aig-logext-ns (+ width const-rsh)
                              lsbs)))
      (aig-head-tail-concat-aux rev-shift (len rev-shift)
                                lsbs msbs msbs-len width const-rsh))
    (b* ((lsbs (aig-logext-ns width lsbs)))
      (aig-head-tail-concat-aux rev-shift (len rev-shift)
                                lsbs msbs msbs-len width 0))))))

Theorem: aig-head-of-concat-correct

(defthm aig-head-of-concat-correct
 (equal
      (aig-list->s (aig-head-of-concat concat-width lsbs msbs width)
                   env)
      (b* ((concat-width (aig-list->s concat-width env))
           (lsbs (aig-list->s lsbs env))
           (msbs (aig-list->s msbs env)))
        (logext width
                (if (< concat-width 0)
                    (ash msbs concat-width)
                  (logapp concat-width lsbs msbs))))))

Theorem: aig-head-of-concat-of-list-fix-concat-width

(defthm aig-head-of-concat-of-list-fix-concat-width
  (equal (aig-head-of-concat (list-fix concat-width)
                             lsbs msbs width)
         (aig-head-of-concat concat-width lsbs msbs width)))

Theorem: aig-head-of-concat-list-equiv-congruence-on-concat-width

(defthm aig-head-of-concat-list-equiv-congruence-on-concat-width
 (implies
    (list-equiv concat-width concat-width-equiv)
    (equal (aig-head-of-concat concat-width lsbs msbs width)
           (aig-head-of-concat concat-width-equiv lsbs msbs width)))
 :rule-classes :congruence)

Theorem: aig-head-of-concat-of-list-fix-lsbs

(defthm aig-head-of-concat-of-list-fix-lsbs
  (equal (aig-head-of-concat concat-width (list-fix lsbs)
                             msbs width)
         (aig-head-of-concat concat-width lsbs msbs width)))

Theorem: aig-head-of-concat-list-equiv-congruence-on-lsbs

(defthm aig-head-of-concat-list-equiv-congruence-on-lsbs
 (implies
    (list-equiv lsbs lsbs-equiv)
    (equal (aig-head-of-concat concat-width lsbs msbs width)
           (aig-head-of-concat concat-width lsbs-equiv msbs width)))
 :rule-classes :congruence)

Theorem: aig-head-of-concat-of-list-fix-msbs

(defthm aig-head-of-concat-of-list-fix-msbs
  (equal (aig-head-of-concat concat-width lsbs (list-fix msbs)
                             width)
         (aig-head-of-concat concat-width lsbs msbs width)))

Theorem: aig-head-of-concat-list-equiv-congruence-on-msbs

(defthm aig-head-of-concat-list-equiv-congruence-on-msbs
 (implies
    (list-equiv msbs msbs-equiv)
    (equal (aig-head-of-concat concat-width lsbs msbs width)
           (aig-head-of-concat concat-width lsbs msbs-equiv width)))
 :rule-classes :congruence)

Theorem: aig-head-of-concat-of-pos-fix-width

(defthm aig-head-of-concat-of-pos-fix-width
  (equal (aig-head-of-concat concat-width lsbs msbs (pos-fix width))
         (aig-head-of-concat concat-width lsbs msbs width)))

Theorem: aig-head-of-concat-pos-equiv-congruence-on-width

(defthm aig-head-of-concat-pos-equiv-congruence-on-width
 (implies
    (pos-equiv width width-equiv)
    (equal (aig-head-of-concat concat-width lsbs msbs width)
           (aig-head-of-concat concat-width lsbs msbs width-equiv)))
 :rule-classes :congruence)