		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-argmasks-lookup

Signature
(svex-argmasks-lookup args mask-al) → argmasks
Arguments: args — Guard (svexlist-p args).; mask-al — Guard (svex-mask-alist-p mask-al).
Returns: argmasks — Type (4vmasklist-p argmasks).

Definitions and Theorems

Function: svex-argmasks-lookup

(defun svex-argmasks-lookup (args mask-al)
  (declare (xargs :guard (and (svexlist-p args)
                              (svex-mask-alist-p mask-al))))
  (let ((__function__ 'svex-argmasks-lookup))
    (declare (ignorable __function__))
    (if (atom args)
        nil
      (cons (svex-mask-lookup (car args) mask-al)
            (svex-argmasks-lookup (cdr args)
                                  mask-al)))))

Theorem: 4vmasklist-p-of-svex-argmasks-lookup

(defthm 4vmasklist-p-of-svex-argmasks-lookup
  (b* ((argmasks (svex-argmasks-lookup args mask-al)))
    (4vmasklist-p argmasks))
  :rule-classes :rewrite)

Theorem: len-of-svex-argmasks-lookup

(defthm len-of-svex-argmasks-lookup
  (equal (len (svex-argmasks-lookup args mask-al))
         (len args)))

Theorem: svex-argmasks-lookup-of-svexlist-fix-args

(defthm svex-argmasks-lookup-of-svexlist-fix-args
  (equal (svex-argmasks-lookup (svexlist-fix args)
                               mask-al)
         (svex-argmasks-lookup args mask-al)))

Theorem: svex-argmasks-lookup-svexlist-equiv-congruence-on-args

(defthm svex-argmasks-lookup-svexlist-equiv-congruence-on-args
  (implies (svexlist-equiv args args-equiv)
           (equal (svex-argmasks-lookup args mask-al)
                  (svex-argmasks-lookup args-equiv mask-al)))
  :rule-classes :congruence)

Theorem: svex-argmasks-lookup-of-svex-mask-alist-fix-mask-al

(defthm svex-argmasks-lookup-of-svex-mask-alist-fix-mask-al
  (equal (svex-argmasks-lookup args (svex-mask-alist-fix mask-al))
         (svex-argmasks-lookup args mask-al)))

Theorem: svex-argmasks-lookup-svex-mask-alist-equiv-congruence-on-mask-al

(defthm
   svex-argmasks-lookup-svex-mask-alist-equiv-congruence-on-mask-al
  (implies (svex-mask-alist-equiv mask-al mask-al-equiv)
           (equal (svex-argmasks-lookup args mask-al)
                  (svex-argmasks-lookup args mask-al-equiv)))
  :rule-classes :congruence)

Theorem: svex-argmasks-lookup-of-nil

(defthm svex-argmasks-lookup-of-nil
  (equal (svex-argmasks-lookup args nil)
         (replicate (len args) 0)))