		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Lhatom-overridemux-eval

Signature
(lhatom-overridemux-eval x env out) → val
Arguments: x — Guard (lhatom-p x).; env — Guard (svex-env-p env).; out — Guard (svex-env-p out).
Returns: val — Type (4vec-p val).

Definitions and Theorems

Function: lhatom-overridemux-eval

(defun lhatom-overridemux-eval (x env out)
 (declare (xargs :guard (and (lhatom-p x)
                             (svex-env-p env)
                             (svex-env-p out))))
 (let ((__function__ 'lhatom-overridemux-eval))
  (declare (ignorable __function__))
  (lhatom-case
   x
   :z 0
   :var
   (4vec-rsh
     (2vec x.rsh)
     (if
       (svar-override-p x.name :val)
       (4vec-bit?!
            (svex-env-fastlookup (svar-change-override x.name :test)
                                 env)
            (svex-env-fastlookup x.name env)
            (svex-env-fastlookup (svar-change-override x.name nil)
                                 out))
       (svex-env-fastlookup x.name env))))))

Theorem: 4vec-p-of-lhatom-overridemux-eval

(defthm 4vec-p-of-lhatom-overridemux-eval
  (b* ((val (lhatom-overridemux-eval x env out)))
    (4vec-p val))
  :rule-classes :rewrite)

Theorem: lhatom-overridemux-eval-of-lhatom-fix-x

(defthm lhatom-overridemux-eval-of-lhatom-fix-x
  (equal (lhatom-overridemux-eval (lhatom-fix x)
                                  env out)
         (lhatom-overridemux-eval x env out)))

Theorem: lhatom-overridemux-eval-lhatom-equiv-congruence-on-x

(defthm lhatom-overridemux-eval-lhatom-equiv-congruence-on-x
  (implies (lhatom-equiv x x-equiv)
           (equal (lhatom-overridemux-eval x env out)
                  (lhatom-overridemux-eval x-equiv env out)))
  :rule-classes :congruence)

Theorem: lhatom-overridemux-eval-of-svex-env-fix-env

(defthm lhatom-overridemux-eval-of-svex-env-fix-env
  (equal (lhatom-overridemux-eval x (svex-env-fix env)
                                  out)
         (lhatom-overridemux-eval x env out)))

Theorem: lhatom-overridemux-eval-svex-env-equiv-congruence-on-env

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

Theorem: lhatom-overridemux-eval-of-svex-env-fix-out

(defthm lhatom-overridemux-eval-of-svex-env-fix-out
  (equal (lhatom-overridemux-eval x env (svex-env-fix out))
         (lhatom-overridemux-eval x env out)))

Theorem: lhatom-overridemux-eval-svex-env-equiv-congruence-on-out

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