Generate a list of place-shifters, counting down from P to 1.
(vl-make-n-bit-shl-place-ps n p) → (mv shift-mods support-mods)
Function:
(defun vl-make-n-bit-shl-place-ps (n p) (declare (xargs :guard (and (posp n) (natp p)))) (let ((__function__ 'vl-make-n-bit-shl-place-ps)) (declare (ignorable __function__)) (b* (((when (zp p)) (mv nil nil)) ((cons car-shifter car-support) (vl-make-n-bit-shl-place-p n p)) ((mv cdr-shifters cdr-support) (vl-make-n-bit-shl-place-ps n (- p 1)))) (mv (cons car-shifter cdr-shifters) (append car-support cdr-support)))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-shl-place-ps.shift-mods (b* (((mv ?shift-mods ?support-mods) (vl-make-n-bit-shl-place-ps n p))) (vl-modulelist-p shift-mods)) :rule-classes :rewrite)
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-shl-place-ps.support-mods (b* (((mv ?shift-mods ?support-mods) (vl-make-n-bit-shl-place-ps n p))) (vl-modulelist-p support-mods)) :rule-classes :rewrite)
Theorem:
(defthm vl-make-n-bit-shl-place-ps-mvtypes-0 (true-listp (mv-nth 0 (vl-make-n-bit-shl-place-ps n p))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-shl-place-ps-mvtypes-1 (true-listp (mv-nth 1 (vl-make-n-bit-shl-place-ps n p))) :rule-classes :type-prescription)
Theorem:
(defthm len-of-vl-make-n-bit-shl-place-ps-0 (equal (len (mv-nth 0 (vl-make-n-bit-shl-place-ps n p))) (nfix p)))
Theorem:
(defthm vl-make-n-bit-shl-place-ps-of-pos-fix-n (equal (vl-make-n-bit-shl-place-ps (pos-fix n) p) (vl-make-n-bit-shl-place-ps n p)))
Theorem:
(defthm vl-make-n-bit-shl-place-ps-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-make-n-bit-shl-place-ps n p) (vl-make-n-bit-shl-place-ps n-equiv p))) :rule-classes :congruence)
Theorem:
(defthm vl-make-n-bit-shl-place-ps-of-nfix-p (equal (vl-make-n-bit-shl-place-ps n (nfix p)) (vl-make-n-bit-shl-place-ps n p)))
Theorem:
(defthm vl-make-n-bit-shl-place-ps-nat-equiv-congruence-on-p (implies (acl2::nat-equiv p p-equiv) (equal (vl-make-n-bit-shl-place-ps n p) (vl-make-n-bit-shl-place-ps n p-equiv))) :rule-classes :congruence)