		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-alist-subst-rw

Signature
(svex-alist-subst-rw x conf) → xx
Arguments: x — Guard (svex-alist-p x).; conf — Guard (svex-substconfig-p conf).
Returns: xx — Type (svex-alist-p xx).

Definitions and Theorems

Function: svex-alist-subst-rw

(defun svex-alist-subst-rw (x conf)
  (declare (xargs :guard (and (svex-alist-p x)
                              (svex-substconfig-p conf))))
  (let ((__function__ 'svex-alist-subst-rw))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (if (mbt (and (consp (car x)) (svar-p (caar x))))
          (cons (cons (caar x)
                      (svex-subst-rw (cdar x) conf))
                (svex-alist-subst-rw (cdr x) conf))
        (svex-alist-subst-rw (cdr x) conf)))))

Theorem: svex-alist-p-of-svex-alist-subst-rw

(defthm svex-alist-p-of-svex-alist-subst-rw
  (b* ((xx (svex-alist-subst-rw x conf)))
    (svex-alist-p xx))
  :rule-classes :rewrite)

Theorem: svex-alist-subst-rw-correct

(defthm svex-alist-subst-rw-correct
  (b* ((?xx (svex-alist-subst-rw x conf)))
    (equal (svex-alist-eval xx env)
           (svex-alist-eval
                (svex-alist-subst x (svex-substconfig->alist conf))
                env))))

Theorem: svex-alist-keys-of-svex-alist-subst-rw

(defthm svex-alist-keys-of-svex-alist-subst-rw
  (b* ((?xx (svex-alist-subst-rw x conf)))
    (equal (svex-alist-keys xx)
           (svex-alist-keys x))))

Theorem: svex-alist-subst-rw-of-svex-alist-fix-x

(defthm svex-alist-subst-rw-of-svex-alist-fix-x
  (equal (svex-alist-subst-rw (svex-alist-fix x)
                              conf)
         (svex-alist-subst-rw x conf)))

Theorem: svex-alist-subst-rw-svex-alist-equiv-congruence-on-x

(defthm svex-alist-subst-rw-svex-alist-equiv-congruence-on-x
  (implies (svex-alist-equiv x x-equiv)
           (equal (svex-alist-subst-rw x conf)
                  (svex-alist-subst-rw x-equiv conf)))
  :rule-classes :congruence)

Theorem: svex-alist-subst-rw-of-svex-substconfig-fix-conf

(defthm svex-alist-subst-rw-of-svex-substconfig-fix-conf
  (equal (svex-alist-subst-rw x (svex-substconfig-fix conf))
         (svex-alist-subst-rw x conf)))

Theorem: svex-alist-subst-rw-svex-substconfig-equiv-congruence-on-conf

(defthm
      svex-alist-subst-rw-svex-substconfig-equiv-congruence-on-conf
  (implies (svex-substconfig-equiv conf conf-equiv)
           (equal (svex-alist-subst-rw x conf)
                  (svex-alist-subst-rw x conf-equiv)))
  :rule-classes :congruence)