(aig-head-of-concat concat-width lsbs msbs width) → *
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)