		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-alist-maybe-rewrite-fixpoint

Rewrites the alist, but only if do-rewrite is non-nil.

Signature
(svex-alist-maybe-rewrite-fixpoint x do-rewrite &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-maybe-rewrite-fixpoint-fn

(defun svex-alist-maybe-rewrite-fixpoint-fn
       (x do-rewrite count verbosep)
  (declare (xargs :guard (and (svex-alist-p x) (natp count))))
  (let ((__function__ 'svex-alist-maybe-rewrite-fixpoint))
    (declare (ignorable __function__))
    (if do-rewrite (svex-alist-rewrite-fixpoint x
                                                :count count
                                                :verbosep verbosep)
      (svex-alist-fix x))))

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

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

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

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

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

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

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

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

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

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

Theorem: svex-alist-maybe-rewrite-fixpoint-correct

(defthm svex-alist-maybe-rewrite-fixpoint-correct
  (b* ((?xx (svex-alist-maybe-rewrite-fixpoint-fn
                 x do-rewrite count verbosep)))
    (equal (svex-alist-eval xx env)
           (svex-alist-eval x env))))

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

(defthm len-of-svex-alist-maybe-rewrite-fixpoint
  (b* ((?xx (svex-alist-maybe-rewrite-fixpoint-fn
                 x do-rewrite count verbosep)))
    (equal (len xx)
           (len (svex-alist-fix x)))))

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

(defthm vars-of-svex-alist-maybe-rewrite-fixpoint
  (b* ((?xx (svex-alist-maybe-rewrite-fixpoint-fn
                 x do-rewrite count verbosep)))
    (implies (not (member v (svex-alist-vars x)))
             (not (member v (svex-alist-vars xx))))))

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

(defthm keys-of-svex-alist-maybe-rewrite-fixpoint
  (b* ((?xx (svex-alist-maybe-rewrite-fixpoint-fn
                 x do-rewrite count verbosep)))
    (iff (svex-lookup v xx)
         (svex-lookup v x))))

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

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