		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Lhs-eval-signx

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

Definitions and Theorems

Function: lhs-eval-signx

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

Theorem: 4vec-p-of-lhs-eval-signx

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

Theorem: svex-envs-similar-implies-equal-lhs-eval-signx-2

(defthm svex-envs-similar-implies-equal-lhs-eval-signx-2
  (implies (svex-envs-similar env env-equiv)
           (equal (lhs-eval-signx x env)
                  (lhs-eval-signx x env-equiv)))
  :rule-classes (:congruence))

Theorem: lhs-eval-signx-of-lhs-fix-x

(defthm lhs-eval-signx-of-lhs-fix-x
  (equal (lhs-eval-signx (lhs-fix x) env)
         (lhs-eval-signx x env)))

Theorem: lhs-eval-signx-lhs-equiv-congruence-on-x

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

Theorem: lhs-eval-signx-of-svex-env-fix-env

(defthm lhs-eval-signx-of-svex-env-fix-env
  (equal (lhs-eval-signx x (svex-env-fix env))
         (lhs-eval-signx x env)))

Theorem: lhs-eval-signx-svex-env-equiv-congruence-on-env

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