		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-alist-rewrite-fixpoint

Signature
(svex-alist-rewrite-fixpoint x &key (count '4) (verbosep 'nil)) → xx
Arguments: x — Guard (svex-alist-p x).; count — Guard (natp count).
Returns: xx — Type (svex-alist-p xx).

Definitions and Theorems

Function: svex-alist-rewrite-fixpoint-fn

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

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

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

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

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

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

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

Theorem: svex-alist-rewrite-fixpoint-fn-of-nfix-count

(defthm svex-alist-rewrite-fixpoint-fn-of-nfix-count
  (equal (svex-alist-rewrite-fixpoint-fn x (nfix count)
                                         verbosep)
         (svex-alist-rewrite-fixpoint-fn x count verbosep)))

Theorem: svex-alist-rewrite-fixpoint-fn-nat-equiv-congruence-on-count

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

Theorem: svex-alist-rewrite-fixpoint-correct

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

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

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

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

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

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

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

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

(defthm svex-alist-keys-of-svex-alist-rewrite-fixpoint
  (b* ((?xx (svex-alist-rewrite-fixpoint-fn x count verbosep)))
    (equal (svex-alist-keys xx)
           (svex-alist-keys x))))