		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

Aig-head-tail-concat-aux

Signature
(aig-head-tail-concat-aux rev-shift shift-len lsbs msbs msbs-len width const-rsh) → concat
Arguments: rev-shift — Guard (true-listp rev-shift).; shift-len — Guard (eql shift-len (len rev-shift)).; lsbs — Guard (true-listp lsbs).; msbs — Guard (true-listp msbs).; msbs-len — Guard (eql msbs-len (len msbs)).; width — Guard (posp width).; const-rsh — Guard (natp const-rsh).
Returns: concat — Type (true-listp concat).

Definitions and Theorems

Function: aig-head-tail-concat-aux

(defun aig-head-tail-concat-aux
       (rev-shift shift-len
                  lsbs msbs msbs-len width const-rsh)
 (declare (xargs :guard (and (true-listp rev-shift)
                             (true-listp lsbs)
                             (true-listp msbs)
                             (posp width)
                             (natp const-rsh)
                             (eql shift-len (len rev-shift))
                             (eql msbs-len (len msbs)))))
 (let ((__function__ 'aig-head-tail-concat-aux))
  (declare (ignorable __function__))
  (b*
   ((width (lposfix width))
    (const-rsh (lnfix const-rsh))
    ((when (atom rev-shift))
     (aig-logext-ns width (aig-logtail-ns const-rsh msbs)))
    (msbs-len (mbe :logic (len msbs) :exec msbs-len))
    (shift-len (1- (mbe :logic (len rev-shift)
                        :exec shift-len)))
    ((when (eq (car rev-shift) nil))
     (aig-head-tail-concat-aux (cdr rev-shift)
                               shift-len
                               lsbs msbs msbs-len width const-rsh))
    (width-plus-rsh (+ width const-rsh))
    (shift-too-widep
         (mbe :logic (<= width-plus-rsh (ash 1 shift-len))
              :exec (or (< (integer-length width-plus-rsh)
                           shift-len)
                        (<= width-plus-rsh (ash 1 shift-len)))))
    (shift-too-narrowp (and (not shift-too-widep)
                            (>= const-rsh
                                (+ msbs-len
                                   (1- (ash 1 (+ 1 shift-len)))))))
    ((when shift-too-narrowp)
     (aig-sterm (aig-sign-s msbs)))
    (rest1
     (if shift-too-widep (aig-logtail-ns const-rsh lsbs)
      (b* ((nshifted (ash 1 shift-len))
           ((when (<= nshifted const-rsh))
            (aig-head-tail-concat-aux
                 (cdr rev-shift)
                 shift-len (aig-logtail-ns nshifted lsbs)
                 msbs
                 msbs-len width (- const-rsh nshifted))))
       (aig-logapp-nss (- nshifted const-rsh)
                       (aig-logtail-ns const-rsh lsbs)
                       (aig-head-tail-concat-aux
                            (cdr rev-shift)
                            shift-len (aig-logtail-ns nshifted lsbs)
                            msbs
                            msbs-len (- width-plus-rsh nshifted)
                            0)))))
    ((when (eq (car rev-shift) t)) rest1)
    (rest0
     (aig-head-tail-concat-aux (cdr rev-shift)
                               shift-len
                               lsbs msbs msbs-len width const-rsh)))
   (aig-ite-bss (car rev-shift)
                rest1 rest0))))

Theorem: true-listp-of-aig-head-tail-concat-aux

(defthm true-listp-of-aig-head-tail-concat-aux
 (b*
  ((concat
     (aig-head-tail-concat-aux rev-shift shift-len
                               lsbs msbs msbs-len width const-rsh)))
  (true-listp concat))
 :rule-classes :rewrite)

Theorem: our-logext-identity

(defthm our-logext-identity
  (implies (signed-byte-p (pos-fix size) i)
           (equal (logext size i) i)))

Theorem: signed-byte-p-monotonic

(defthm signed-byte-p-monotonic
  (implies (and (signed-byte-p n x)
                (<= n m)
                (integerp m))
           (signed-byte-p m x)))

Theorem: aig-head-tail-concat-aux-correct

(defthm aig-head-tail-concat-aux-correct
 (implies
  (signed-byte-p (+ (pos-fix width) (nfix const-rsh))
                 (aig-list->s lsbs env))
  (equal
   (aig-list->s
       (aig-head-tail-concat-aux rev-shift shift-len
                                 lsbs msbs msbs-len width const-rsh)
       env)
   (logext width
           (logtail const-rsh
                    (logapp (aig-list->u (rev rev-shift) env)
                            (aig-list->s lsbs env)
                            (aig-list->s msbs env)))))))

Theorem: aig-head-tail-concat-aux-of-list-fix-rev-shift

(defthm aig-head-tail-concat-aux-of-list-fix-rev-shift
 (equal
     (aig-head-tail-concat-aux (list-fix rev-shift)
                               shift-len
                               lsbs msbs msbs-len width const-rsh)
     (aig-head-tail-concat-aux rev-shift shift-len
                               lsbs msbs msbs-len width const-rsh)))

Theorem: aig-head-tail-concat-aux-list-equiv-congruence-on-rev-shift

(defthm aig-head-tail-concat-aux-list-equiv-congruence-on-rev-shift
 (implies
  (list-equiv rev-shift rev-shift-equiv)
  (equal
     (aig-head-tail-concat-aux rev-shift shift-len
                               lsbs msbs msbs-len width const-rsh)
     (aig-head-tail-concat-aux rev-shift-equiv shift-len
                               lsbs msbs msbs-len width const-rsh)))
 :rule-classes :congruence)

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

(defthm aig-head-tail-concat-aux-of-list-fix-lsbs
 (equal
     (aig-head-tail-concat-aux rev-shift shift-len (list-fix lsbs)
                               msbs msbs-len width const-rsh)
     (aig-head-tail-concat-aux rev-shift shift-len
                               lsbs msbs msbs-len width const-rsh)))

Theorem: aig-head-tail-concat-aux-list-equiv-congruence-on-lsbs

(defthm aig-head-tail-concat-aux-list-equiv-congruence-on-lsbs
 (implies
  (list-equiv lsbs lsbs-equiv)
  (equal
       (aig-head-tail-concat-aux rev-shift shift-len
                                 lsbs msbs msbs-len width const-rsh)
       (aig-head-tail-concat-aux rev-shift shift-len lsbs-equiv
                                 msbs msbs-len width const-rsh)))
 :rule-classes :congruence)

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

(defthm aig-head-tail-concat-aux-of-list-fix-msbs
 (equal
  (aig-head-tail-concat-aux rev-shift shift-len lsbs (list-fix msbs)
                            msbs-len width const-rsh)
  (aig-head-tail-concat-aux rev-shift shift-len
                            lsbs msbs msbs-len width const-rsh)))

Theorem: aig-head-tail-concat-aux-list-equiv-congruence-on-msbs

(defthm aig-head-tail-concat-aux-list-equiv-congruence-on-msbs
 (implies
  (list-equiv msbs msbs-equiv)
  (equal
    (aig-head-tail-concat-aux rev-shift shift-len
                              lsbs msbs msbs-len width const-rsh)
    (aig-head-tail-concat-aux rev-shift shift-len lsbs
                              msbs-equiv msbs-len width const-rsh)))
 :rule-classes :congruence)

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

(defthm aig-head-tail-concat-aux-of-pos-fix-width
 (equal
     (aig-head-tail-concat-aux rev-shift shift-len
                               lsbs msbs msbs-len (pos-fix width)
                               const-rsh)
     (aig-head-tail-concat-aux rev-shift shift-len
                               lsbs msbs msbs-len width const-rsh)))

Theorem: aig-head-tail-concat-aux-pos-equiv-congruence-on-width

(defthm aig-head-tail-concat-aux-pos-equiv-congruence-on-width
 (implies
  (pos-equiv width width-equiv)
  (equal
    (aig-head-tail-concat-aux rev-shift shift-len
                              lsbs msbs msbs-len width const-rsh)
    (aig-head-tail-concat-aux rev-shift shift-len lsbs
                              msbs msbs-len width-equiv const-rsh)))
 :rule-classes :congruence)

Theorem: aig-head-tail-concat-aux-of-nfix-const-rsh

(defthm aig-head-tail-concat-aux-of-nfix-const-rsh
 (equal
     (aig-head-tail-concat-aux rev-shift shift-len lsbs
                               msbs msbs-len width (nfix const-rsh))
     (aig-head-tail-concat-aux rev-shift shift-len
                               lsbs msbs msbs-len width const-rsh)))

Theorem: aig-head-tail-concat-aux-nat-equiv-congruence-on-const-rsh

(defthm aig-head-tail-concat-aux-nat-equiv-congruence-on-const-rsh
 (implies
  (nat-equiv const-rsh const-rsh-equiv)
  (equal
    (aig-head-tail-concat-aux rev-shift shift-len
                              lsbs msbs msbs-len width const-rsh)
    (aig-head-tail-concat-aux rev-shift shift-len lsbs
                              msbs msbs-len width const-rsh-equiv)))
 :rule-classes :congruence)