		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Svar/4vec-alist-eval

Signature
(svar/4vec-alist-eval x env) → val
Arguments: x — Guard (svar/4vec-alist-p x).; env — Guard (svex-env-p env).
Returns: val — Type (svex-env-p val).

Definitions and Theorems

Function: svar/4vec-alist-eval

(defun svar/4vec-alist-eval (x env)
  (declare (xargs :guard (and (svar/4vec-alist-p x)
                              (svex-env-p env))))
  (let ((__function__ 'svar/4vec-alist-eval))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((unless (mbt (and (consp (car x))
                            (svar-p (caar x)))))
          (svar/4vec-alist-eval (cdr x) env)))
      (cons (cons (caar x)
                  (svar/4vec-eval (cdar x) env))
            (svar/4vec-alist-eval (cdr x) env)))))

Theorem: svex-env-p-of-svar/4vec-alist-eval

(defthm svex-env-p-of-svar/4vec-alist-eval
  (b* ((val (svar/4vec-alist-eval x env)))
    (svex-env-p val))
  :rule-classes :rewrite)

Theorem: svar/4vec-alist-eval-in-terms-of-svex-alist-eval

(defthm svar/4vec-alist-eval-in-terms-of-svex-alist-eval
  (implies (svex-alist-noncall-p x)
           (equal (svar/4vec-alist-eval x env)
                  (svex-alist-eval x env))))

Theorem: svex-env-lookup-of-svar/4vec-alist-eval

(defthm svex-env-lookup-of-svar/4vec-alist-eval
  (b* ((?val (svar/4vec-alist-eval x env)))
    (equal (svex-env-lookup v val)
           (let ((look (hons-assoc-equal (svar-fix v)
                                         (svar/4vec-alist-fix x))))
             (if look (svar/4vec-eval (cdr look) env)
               (4vec-x))))))

Theorem: svar/4vec-alist-eval-of-svar/4vec-alist-fix-x

(defthm svar/4vec-alist-eval-of-svar/4vec-alist-fix-x
  (equal (svar/4vec-alist-eval (svar/4vec-alist-fix x)
                               env)
         (svar/4vec-alist-eval x env)))

Theorem: svar/4vec-alist-eval-svar/4vec-alist-equiv-congruence-on-x

(defthm svar/4vec-alist-eval-svar/4vec-alist-equiv-congruence-on-x
  (implies (svar/4vec-alist-equiv x x-equiv)
           (equal (svar/4vec-alist-eval x env)
                  (svar/4vec-alist-eval x-equiv env)))
  :rule-classes :congruence)

Theorem: svar/4vec-alist-eval-of-svex-env-fix-env

(defthm svar/4vec-alist-eval-of-svex-env-fix-env
  (equal (svar/4vec-alist-eval x (svex-env-fix env))
         (svar/4vec-alist-eval x env)))

Theorem: svar/4vec-alist-eval-svex-env-equiv-congruence-on-env

(defthm svar/4vec-alist-eval-svex-env-equiv-congruence-on-env
  (implies (svex-env-equiv env env-equiv)
           (equal (svar/4vec-alist-eval x env)
                  (svar/4vec-alist-eval x env-equiv)))
  :rule-classes :congruence)