		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svar-boolmasks-limit-to-bound-vars

Signature
(svar-boolmasks-limit-to-bound-vars keys boolvars) → xx
Arguments: keys — Guard (svarlist-p keys).; boolvars — Guard (svar-boolmasks-p boolvars).
Returns: xx — Type (svar-boolmasks-p xx).

Definitions and Theorems

Function: svar-boolmasks-limit-to-bound-vars

(defun svar-boolmasks-limit-to-bound-vars (keys boolvars)
  (declare (xargs :guard (and (svarlist-p keys)
                              (svar-boolmasks-p boolvars))))
  (let ((__function__ 'svar-boolmasks-limit-to-bound-vars))
    (declare (ignorable __function__))
    (if (atom keys)
        nil
      (let* ((look (svar-boolmasks-lookup (car keys)
                                          boolvars)))
        (cons (cons (svar-fix (car keys)) look)
              (svar-boolmasks-limit-to-bound-vars (cdr keys)
                                                  boolvars))))))

Theorem: svar-boolmasks-p-of-svar-boolmasks-limit-to-bound-vars

(defthm svar-boolmasks-p-of-svar-boolmasks-limit-to-bound-vars
  (b* ((xx (svar-boolmasks-limit-to-bound-vars keys boolvars)))
    (svar-boolmasks-p xx))
  :rule-classes :rewrite)

Theorem: svar-boolmasks-limit-to-bound-vars-of-svarlist-fix-keys

(defthm svar-boolmasks-limit-to-bound-vars-of-svarlist-fix-keys
  (equal (svar-boolmasks-limit-to-bound-vars (svarlist-fix keys)
                                             boolvars)
         (svar-boolmasks-limit-to-bound-vars keys boolvars)))

Theorem: svar-boolmasks-limit-to-bound-vars-svarlist-equiv-congruence-on-keys

(defthm
 svar-boolmasks-limit-to-bound-vars-svarlist-equiv-congruence-on-keys
 (implies
   (svarlist-equiv keys keys-equiv)
   (equal (svar-boolmasks-limit-to-bound-vars keys boolvars)
          (svar-boolmasks-limit-to-bound-vars keys-equiv boolvars)))
 :rule-classes :congruence)

Theorem: svar-boolmasks-limit-to-bound-vars-of-svar-boolmasks-fix-boolvars

(defthm
  svar-boolmasks-limit-to-bound-vars-of-svar-boolmasks-fix-boolvars
  (equal (svar-boolmasks-limit-to-bound-vars
              keys (svar-boolmasks-fix boolvars))
         (svar-boolmasks-limit-to-bound-vars keys boolvars)))

Theorem: svar-boolmasks-limit-to-bound-vars-svar-boolmasks-equiv-congruence-on-boolvars

(defthm
 svar-boolmasks-limit-to-bound-vars-svar-boolmasks-equiv-congruence-on-boolvars
 (implies
   (svar-boolmasks-equiv boolvars boolvars-equiv)
   (equal (svar-boolmasks-limit-to-bound-vars keys boolvars)
          (svar-boolmasks-limit-to-bound-vars keys boolvars-equiv)))
 :rule-classes :congruence)