		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Lhs-overridemux-eval-zero

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

Definitions and Theorems

Function: lhs-overridemux-eval-zero

(defun lhs-overridemux-eval-zero (x env out)
  (declare (xargs :guard (and (lhs-p x)
                              (svex-env-p env)
                              (svex-env-p out))))
  (let ((__function__ 'lhs-overridemux-eval-zero))
    (declare (ignorable __function__))
    (if (atom x)
        0
      (4vec-concat (2vec (lhrange->w (car x)))
                   (lhatom-overridemux-eval (lhrange->atom (car x))
                                            env out)
                   (lhs-overridemux-eval-zero (cdr x)
                                              env out)))))

Theorem: 4vec-p-of-lhs-overridemux-eval-zero

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

Theorem: lhs-overridemux-eval-zero-of-lhs-fix-x

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

Theorem: lhs-overridemux-eval-zero-lhs-equiv-congruence-on-x

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

Theorem: lhs-overridemux-eval-zero-of-svex-env-fix-env

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

Theorem: lhs-overridemux-eval-zero-svex-env-equiv-congruence-on-env

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

Theorem: lhs-overridemux-eval-zero-of-svex-env-fix-out

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

Theorem: lhs-overridemux-eval-zero-svex-env-equiv-congruence-on-out

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