		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-rewrite-memo-vars-ok

Signature
(svex-rewrite-memo-vars-ok x var) → *
Arguments: x — Guard (svex-svex-memo-p x).

Definitions and Theorems

Function: svex-rewrite-memo-vars-ok

(defun svex-rewrite-memo-vars-ok (x var)
  (declare (xargs :guard (svex-svex-memo-p x)))
  (let ((__function__ 'svex-rewrite-memo-vars-ok))
    (declare (ignorable __function__))
    (ec-call (svex-rewrite-memo-vars-ok1 (svex-svex-memo-fix x)
                                         var))))

Theorem: svex-rewrite-memo-vars-ok-of-empty

(defthm svex-rewrite-memo-vars-ok-of-empty
  (implies (atom atom)
           (svex-rewrite-memo-vars-ok atom var))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: svex-rewrite-memo-vars-ok-implies

(defthm svex-rewrite-memo-vars-ok-implies
  (implies (svex-rewrite-memo-vars-ok x var)
           (b* ((x (svex-svex-memo-fix x))
                (lookup (hons-assoc-equal key x))
                (val (cdr lookup)))
             (implies (and lookup
                           (not (member var (svex-vars key))))
                      (not (member var (svex-vars val)))))))

Theorem: svex-rewrite-memo-vars-ok-of-svex-svex-memo-fix-x

(defthm svex-rewrite-memo-vars-ok-of-svex-svex-memo-fix-x
  (equal (svex-rewrite-memo-vars-ok (svex-svex-memo-fix x)
                                    var)
         (svex-rewrite-memo-vars-ok x var)))

Theorem: svex-rewrite-memo-vars-ok-svex-svex-memo-equiv-congruence-on-x

(defthm
     svex-rewrite-memo-vars-ok-svex-svex-memo-equiv-congruence-on-x
  (implies (svex-svex-memo-equiv x x-equiv)
           (equal (svex-rewrite-memo-vars-ok x var)
                  (svex-rewrite-memo-vars-ok x-equiv var)))
  :rule-classes :congruence)

Theorem: svex-rewrite-memo-vars-ok-cons-1

(defthm svex-rewrite-memo-vars-ok-cons-1
  (implies (and (svex-rewrite-memo-vars-ok x var)
                (member var (svex-vars y)))
           (svex-rewrite-memo-vars-ok (cons (cons y y1) x)
                                      var)))

Theorem: svex-rewrite-memo-vars-ok-cons-2

(defthm svex-rewrite-memo-vars-ok-cons-2
  (implies (and (svex-rewrite-memo-vars-ok x var)
                (not (member var (svex-vars y1))))
           (svex-rewrite-memo-vars-ok (cons (cons y y1) x)
                                      var)))