		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-alist-rewrite-top

Signature
(svex-alist-rewrite-top x &key (verbosep 'nil)) → xx
Arguments: x — Guard (svex-alist-p x).
Returns: xx — Type (svex-alist-p xx).

Definitions and Theorems

Function: svex-alist-rewrite-top-fn

(defun svex-alist-rewrite-top-fn (x verbosep)
  (declare (xargs :guard (svex-alist-p x)))
  (let ((__function__ 'svex-alist-rewrite-top))
    (declare (ignorable __function__))
    (pairlis$ (svex-alist-keys x)
              (svexlist-rewrite-top (svex-alist-vals x)
                                    :verbosep verbosep))))

Theorem: svex-alist-p-of-svex-alist-rewrite-top

(defthm svex-alist-p-of-svex-alist-rewrite-top
  (b* ((xx (svex-alist-rewrite-top-fn x verbosep)))
    (svex-alist-p xx))
  :rule-classes :rewrite)

Theorem: svex-alist-rewrite-top-fn-of-svex-alist-fix-x

(defthm svex-alist-rewrite-top-fn-of-svex-alist-fix-x
  (equal (svex-alist-rewrite-top-fn (svex-alist-fix x)
                                    verbosep)
         (svex-alist-rewrite-top-fn x verbosep)))

Theorem: svex-alist-rewrite-top-fn-svex-alist-equiv-congruence-on-x

(defthm svex-alist-rewrite-top-fn-svex-alist-equiv-congruence-on-x
  (implies (svex-alist-equiv x x-equiv)
           (equal (svex-alist-rewrite-top-fn x verbosep)
                  (svex-alist-rewrite-top-fn x-equiv verbosep)))
  :rule-classes :congruence)

Theorem: svex-alist-rewrite-top-correct

(defthm svex-alist-rewrite-top-correct
 (equal (svex-alist-eval (svex-alist-rewrite-top x
                                                 :verbosep verbosep)
                         env)
        (svex-alist-eval x env)))

Theorem: len-of-svex-alist-rewrite-top

(defthm len-of-svex-alist-rewrite-top
  (equal (len (svex-alist-rewrite-top x
                                      :verbosep verbosep))
         (len (svex-alist-fix x))))

Theorem: vars-of-svex-alist-rewrite-top

(defthm vars-of-svex-alist-rewrite-top
 (implies
  (not (member v (svex-alist-vars x)))
  (not (member v
               (svex-alist-vars
                    (svex-alist-rewrite-top x
                                            :verbosep verbosep))))))

Theorem: keys-of-svex-alist-rewrite-top

(defthm keys-of-svex-alist-rewrite-top
  (iff (svex-lookup v
                    (svex-alist-rewrite-top x
                                            :verbosep verbosep))
       (svex-lookup v x)))