		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svex-a4vec-env-eval

Signature
(svex-a4vec-env-eval x env) → xx
Arguments: x — Guard (svex-a4vec-env-p x).
Returns: xx — Type (svex-env-p xx).

Definitions and Theorems

Function: svex-a4vec-env-eval

(defun svex-a4vec-env-eval (x env)
  (declare (xargs :guard (svex-a4vec-env-p x)))
  (let ((__function__ 'svex-a4vec-env-eval))
    (declare (ignorable __function__))
    (b* ((x (svex-a4vec-env-fix x)))
      (if (atom x)
          nil
        (cons (cons (svar-fix (caar x))
                    (a4vec-eval (cdar x) env))
              (svex-a4vec-env-eval (cdr x) env))))))

Theorem: svex-env-p-of-svex-a4vec-env-eval

(defthm svex-env-p-of-svex-a4vec-env-eval
  (b* ((xx (svex-a4vec-env-eval x env)))
    (svex-env-p xx))
  :rule-classes :rewrite)

Theorem: alist-keys-of-svex-a4vec-env-eval

(defthm alist-keys-of-svex-a4vec-env-eval
  (b* ((?xx (svex-a4vec-env-eval x env)))
    (equal (alist-keys xx)
           (alist-keys (svex-a4vec-env-fix x)))))

Theorem: svex-a4vec-env-eval-of-svex-a4vec-env-fix-x

(defthm svex-a4vec-env-eval-of-svex-a4vec-env-fix-x
  (equal (svex-a4vec-env-eval (svex-a4vec-env-fix x)
                              env)
         (svex-a4vec-env-eval x env)))

Theorem: svex-a4vec-env-eval-svex-a4vec-env-equiv-congruence-on-x

(defthm svex-a4vec-env-eval-svex-a4vec-env-equiv-congruence-on-x
  (implies (svex-a4vec-env-equiv x x-equiv)
           (equal (svex-a4vec-env-eval x env)
                  (svex-a4vec-env-eval x-equiv env)))
  :rule-classes :congruence)