		Search-engine friendly clone of the ACL2 documentation.

Rewriting-concatenations

Svexlist-normalize-concats

Signature
(svexlist-normalize-concats x &key (verbosep 'nil)) → new-x
Arguments: x — Guard (svexlist-p x).
Returns: new-x — Type (and (svexlist-p new-x) (equal (len new-x) (len x))).

Definitions and Theorems

Function: svexlist-normalize-concats-fn

(defun svexlist-normalize-concats-fn (x verbosep)
 (declare (xargs :guard (svexlist-p x)))
 (let ((__function__ 'svexlist-normalize-concats))
  (declare (ignorable __function__))
  (b*
   ((- (and verbosep
            (cw "opcount before norm-concats: ~x0~%"
                (svexlist-opcount x))))
    (ctxalist
     (time$
        (svexlist-make-top-context-alist x nil)
        :mintime 1
        :msg "; norm-concats: context alist: ~st sec, ~sa bytes~%"))
    (res (time$ (svexlist-normalize-concats-aux x ctxalist)
                :mintime 1
                :msg "; norm-concats main: ~st sec, ~sa bytes~%")))
   (clear-memoize-table 'svex-normalize-concats-aux)
   (fast-alist-free ctxalist)
   (and verbosep
        (cw "opcount after norm-concats: ~x0~%"
            (svexlist-opcount res)))
   res)))

Theorem: return-type-of-svexlist-normalize-concats

(defthm return-type-of-svexlist-normalize-concats
  (b* ((new-x (svexlist-normalize-concats-fn x verbosep)))
    (and (svexlist-p new-x)
         (equal (len new-x) (len x))))
  :rule-classes :rewrite)

Theorem: svexlist-normalize-concats-correct

(defthm svexlist-normalize-concats-correct
  (b* ((?new-x (svexlist-normalize-concats-fn x verbosep)))
    (equal (svexlist-eval new-x env)
           (svexlist-eval x env))))

Theorem: vars-of-svexlist-normalize-concats

(defthm vars-of-svexlist-normalize-concats
  (b* ((?new-x (svexlist-normalize-concats-fn x verbosep)))
    (implies (not (member v (svexlist-vars x)))
             (not (member v (svexlist-vars new-x))))))

Theorem: svexlist-normalize-concats-fn-of-svexlist-fix-x

(defthm svexlist-normalize-concats-fn-of-svexlist-fix-x
  (equal (svexlist-normalize-concats-fn (svexlist-fix x)
                                        verbosep)
         (svexlist-normalize-concats-fn x verbosep)))

Theorem: svexlist-normalize-concats-fn-svexlist-equiv-congruence-on-x

(defthm svexlist-normalize-concats-fn-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-normalize-concats-fn x verbosep)
                  (svexlist-normalize-concats-fn x-equiv verbosep)))
  :rule-classes :congruence)