		Search-engine friendly clone of the ACL2 documentation.

Rewriting-concatenations

Svex-alist-normalize-concats

Signature
(svex-alist-normalize-concats x &key (verbosep 'nil)) → new-x
Arguments: x — Guard (svex-alist-p x).
Returns: new-x — Type (svex-alist-p new-x).

Definitions and Theorems

Function: svex-alist-normalize-concats-fn

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

Theorem: svex-alist-p-of-svex-alist-normalize-concats

(defthm svex-alist-p-of-svex-alist-normalize-concats
  (b* ((new-x (svex-alist-normalize-concats-fn x verbosep)))
    (svex-alist-p new-x))
  :rule-classes :rewrite)

Theorem: svex-alist-normalize-concats-fn-of-svex-alist-fix-x

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

Theorem: svex-alist-normalize-concats-fn-svex-alist-equiv-congruence-on-x

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

Theorem: svex-alist-normalize-concats-correct

(defthm svex-alist-normalize-concats-correct
 (equal
  (svex-alist-eval (svex-alist-normalize-concats x
                                                 :verbosep verbosep)
                   env)
  (svex-alist-eval x env)))

Theorem: len-of-svex-alist-normalize-concats

(defthm len-of-svex-alist-normalize-concats
  (equal (len (svex-alist-normalize-concats x
                                            :verbosep verbosep))
         (len (svex-alist-fix x))))

Theorem: svex-lookup-in-pairlis$

(defthm svex-lookup-in-pairlis$
  (implies (equal (len x) (len y))
           (iff (svex-lookup v (pairlis$ x y))
                (member (svar-fix v) x))))

Theorem: vars-of-svex-alist-normalize-concats

(defthm vars-of-svex-alist-normalize-concats
 (implies
  (not (member v (svex-alist-vars x)))
  (not
    (member
         v
         (svex-alist-vars
              (svex-alist-normalize-concats x
                                            :verbosep verbosep))))))

Theorem: keys-of-svex-alist-normalize-concats

(defthm keys-of-svex-alist-normalize-concats
 (iff
     (svex-lookup v
                  (svex-alist-normalize-concats x
                                                :verbosep verbosep))
     (svex-lookup v x)))

Theorem: svex-alist-keys-of-svex-alist-normalize-concats

(defthm svex-alist-keys-of-svex-alist-normalize-concats
  (b* ((?new-x (svex-alist-normalize-concats-fn x verbosep)))
    (equal (svex-alist-keys new-x)
           (svex-alist-keys x))))