		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-rewrite-memo-correct

Signature
(svex-rewrite-memo-correct x masks env) → *
Arguments: x — Guard (svex-svex-memo-p x).; masks — Guard (svex-mask-alist-p masks).; env — Guard (svex-env-p env).

Definitions and Theorems

Function: svex-rewrite-memo-correct

(defun svex-rewrite-memo-correct (x masks env)
  (declare (xargs :guard (and (svex-svex-memo-p x)
                              (svex-mask-alist-p masks)
                              (svex-env-p env))))
  (let ((__function__ 'svex-rewrite-memo-correct))
    (declare (ignorable __function__))
    (ec-call (svex-rewrite-memo-correct1 (svex-svex-memo-fix x)
                                         (svex-mask-alist-fix masks)
                                         (svex-env-fix env)))))

Theorem: svex-rewrite-memo-correct-of-empty

(defthm svex-rewrite-memo-correct-of-empty
  (implies (atom x)
           (svex-rewrite-memo-correct x masks env))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: svex-rewrite-memo-correct-implies

(defthm svex-rewrite-memo-correct-implies
  (implies
       (svex-rewrite-memo-correct x masks env)
       (b* ((lookup (hons-assoc-equal key (svex-svex-memo-fix x)))
            (mask (svex-mask-lookup key masks))
            (val (cdr lookup)))
         (implies lookup
                  (equal (4vec-mask mask (svex-eval val env))
                         (4vec-mask mask (svex-eval key env)))))))

Theorem: svex-rewrite-memo-correct-implies-fix

(defthm svex-rewrite-memo-correct-implies-fix
  (implies
       (svex-rewrite-memo-correct x masks env)
       (b* ((lookup (hons-assoc-equal (svex-fix key)
                                      (svex-svex-memo-fix x)))
            (mask (svex-mask-lookup key masks))
            (val (cdr lookup)))
         (implies lookup
                  (equal (4vec-mask mask (svex-eval val env))
                         (4vec-mask mask (svex-eval key env)))))))

Theorem: svex-rewrite-memo-correct-of-svex-svex-memo-fix-x

(defthm svex-rewrite-memo-correct-of-svex-svex-memo-fix-x
  (equal (svex-rewrite-memo-correct (svex-svex-memo-fix x)
                                    masks env)
         (svex-rewrite-memo-correct x masks env)))

Theorem: svex-rewrite-memo-correct-svex-svex-memo-equiv-congruence-on-x

(defthm
     svex-rewrite-memo-correct-svex-svex-memo-equiv-congruence-on-x
  (implies (svex-svex-memo-equiv x x-equiv)
           (equal (svex-rewrite-memo-correct x masks env)
                  (svex-rewrite-memo-correct x-equiv masks env)))
  :rule-classes :congruence)

Theorem: svex-rewrite-memo-correct-of-svex-mask-alist-fix-masks

(defthm svex-rewrite-memo-correct-of-svex-mask-alist-fix-masks
  (equal (svex-rewrite-memo-correct x (svex-mask-alist-fix masks)
                                    env)
         (svex-rewrite-memo-correct x masks env)))

Theorem: svex-rewrite-memo-correct-svex-mask-alist-equiv-congruence-on-masks

(defthm
 svex-rewrite-memo-correct-svex-mask-alist-equiv-congruence-on-masks
 (implies (svex-mask-alist-equiv masks masks-equiv)
          (equal (svex-rewrite-memo-correct x masks env)
                 (svex-rewrite-memo-correct x masks-equiv env)))
 :rule-classes :congruence)

Theorem: svex-rewrite-memo-correct-of-svex-env-fix-env

(defthm svex-rewrite-memo-correct-of-svex-env-fix-env
  (equal (svex-rewrite-memo-correct x masks (svex-env-fix env))
         (svex-rewrite-memo-correct x masks env)))

Theorem: svex-rewrite-memo-correct-svex-env-equiv-congruence-on-env

(defthm svex-rewrite-memo-correct-svex-env-equiv-congruence-on-env
  (implies (svex-env-equiv env env-equiv)
           (equal (svex-rewrite-memo-correct x masks env)
                  (svex-rewrite-memo-correct x masks env-equiv)))
  :rule-classes :congruence)

Theorem: svex-rewrite-memo-correct-cons

(defthm svex-rewrite-memo-correct-cons
  (implies (svex-rewrite-memo-correct x masks env)
           (iff (svex-rewrite-memo-correct (cons (cons y y1) x)
                                           masks env)
                (equal (4vec-mask (svex-mask-lookup y masks)
                                  (svex-eval y env))
                       (4vec-mask (svex-mask-lookup y masks)
                                  (svex-eval y1 env))))))