		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-shl-place-ps

Generate a list of place-shifters, counting down from P to 1.

Signature
(vl-make-n-bit-shl-place-ps n p) → (mv shift-mods support-mods)
Arguments: n — Guard (posp n).; p — Guard (natp p).
Returns: shift-mods — Type (vl-modulelist-p shift-mods).; support-mods — Type (vl-modulelist-p support-mods).

Definitions and Theorems

Function: vl-make-n-bit-shl-place-ps

(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: vl-modulelist-p-of-vl-make-n-bit-shl-place-ps.shift-mods

(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: vl-modulelist-p-of-vl-make-n-bit-shl-place-ps.support-mods

(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: vl-make-n-bit-shl-place-ps-mvtypes-0

(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: vl-make-n-bit-shl-place-ps-mvtypes-1

(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: len-of-vl-make-n-bit-shl-place-ps-0

(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: vl-make-n-bit-shl-place-ps-of-pos-fix-n

(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: vl-make-n-bit-shl-place-ps-pos-equiv-congruence-on-n

(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: vl-make-n-bit-shl-place-ps-of-nfix-p

(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: vl-make-n-bit-shl-place-ps-nat-equiv-congruence-on-p

(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)