		Search-engine friendly clone of the ACL2 documentation.

Truth

Var-repetitions

Signature
(var-repetitions n val numvars) → rep-val
Arguments: n — Guard (natp n).; val — Guard (natp val).; numvars — Guard (natp numvars).
Returns: rep-val — Type (natp rep-val).

Definitions and Theorems

Function: var-repetitions

(defun var-repetitions (n val numvars)
  (declare (xargs :guard (and (natp n)
                              (natp val)
                              (natp numvars))))
  (declare (xargs :guard (and (<= n numvars)
                              (unsigned-byte-p (ash 1 n) val))))
  (let ((__function__ 'var-repetitions))
    (declare (ignorable __function__))
    (mbe :logic
         (logrepeat (ash 1 (- (nfix numvars) (nfix n)))
                    (ash 1 (nfix n))
                    (nfix val))
         :exec
         (b* ((shift (ash 1 n))
              ((when (mbe :logic (zp (- numvars n))
                          :exec (eql n numvars)))
               val))
           (var-repetitions (+ 1 n)
                            (logapp shift val val)
                            numvars)))))

Theorem: natp-of-var-repetitions

(defthm natp-of-var-repetitions
  (b* ((rep-val (var-repetitions n val numvars)))
    (natp rep-val))
  :rule-classes :type-prescription)

Theorem: var-repetitions-of-nfix-n

(defthm var-repetitions-of-nfix-n
  (equal (var-repetitions (nfix n) val numvars)
         (var-repetitions n val numvars)))

Theorem: var-repetitions-nat-equiv-congruence-on-n

(defthm var-repetitions-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (var-repetitions n val numvars)
                  (var-repetitions n-equiv val numvars)))
  :rule-classes :congruence)

Theorem: var-repetitions-of-nfix-val

(defthm var-repetitions-of-nfix-val
  (equal (var-repetitions n (nfix val) numvars)
         (var-repetitions n val numvars)))

Theorem: var-repetitions-nat-equiv-congruence-on-val

(defthm var-repetitions-nat-equiv-congruence-on-val
  (implies (nat-equiv val val-equiv)
           (equal (var-repetitions n val numvars)
                  (var-repetitions n val-equiv numvars)))
  :rule-classes :congruence)

Theorem: var-repetitions-of-nfix-numvars

(defthm var-repetitions-of-nfix-numvars
  (equal (var-repetitions n val (nfix numvars))
         (var-repetitions n val numvars)))

Theorem: var-repetitions-nat-equiv-congruence-on-numvars

(defthm var-repetitions-nat-equiv-congruence-on-numvars
  (implies (nat-equiv numvars numvars-equiv)
           (equal (var-repetitions n val numvars)
                  (var-repetitions n val numvars-equiv)))
  :rule-classes :congruence)