		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svexlist-rewrite-fixpoint

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

Definitions and Theorems

Function: svexlist-rewrite-fixpoint-fn

(defun svexlist-rewrite-fixpoint-fn (x count verbosep)
  (declare (xargs :guard (and (svexlist-p x) (natp count))))
  (let ((__function__ 'svexlist-rewrite-fixpoint))
    (declare (ignorable __function__))
    (b* ((x (mbe :logic (svexlist-fix x) :exec x))
         ((when (zp count)) x)
         (newx (svexlist-rewrite-top x
                                     :verbosep verbosep))
         ((when (hons-equal x newx)) x))
      (svexlist-rewrite-fixpoint newx
                                 :count (1- count)
                                 :verbosep verbosep))))

Theorem: svexlist-p-of-svexlist-rewrite-fixpoint

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

Theorem: svexlist-rewrite-fixpoint-fn-of-svexlist-fix-x

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

Theorem: svexlist-rewrite-fixpoint-fn-svexlist-equiv-congruence-on-x

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

Theorem: svexlist-rewrite-fixpoint-fn-of-nfix-count

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

Theorem: svexlist-rewrite-fixpoint-fn-nat-equiv-congruence-on-count

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

Theorem: svexlist-rewrite-fixpoint-correct

(defthm svexlist-rewrite-fixpoint-correct
  (b* ((?xx (svexlist-rewrite-fixpoint-fn x count verbosep)))
    (equal (svexlist-eval xx env)
           (svexlist-eval x env))))

Theorem: len-of-svexlist-rewrite-fixpoint

(defthm len-of-svexlist-rewrite-fixpoint
  (b* ((?xx (svexlist-rewrite-fixpoint-fn x count verbosep)))
    (equal (len xx) (len x))))

Theorem: consp-of-svexlist-rewrite-fixpoint

(defthm consp-of-svexlist-rewrite-fixpoint
  (b* ((?xx (svexlist-rewrite-fixpoint-fn x count verbosep)))
    (equal (consp xx) (consp x))))

Theorem: vars-of-svexlist-rewrite-fixpoint

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