		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)