(aig-head-tail-concat-aux rev-shift shift-len lsbs msbs msbs-len width const-rsh) → concat
Function:
(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:
(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:
(defthm our-logext-identity (implies (signed-byte-p (pos-fix size) i) (equal (logext size i) i)))
Theorem:
(defthm signed-byte-p-monotonic (implies (and (signed-byte-p n x) (<= n m) (integerp m)) (signed-byte-p m x)))
Theorem:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)