		Search-engine friendly clone of the ACL2 documentation.

Lhprobe/4vec-p

Lhprobe/4vec-eval

Evaluator for lhprobe/4vec-p objects

Signature
(lhprobe/4vec-eval x envs) → val
Arguments: x — Guard (lhprobe/4vec-p x).; envs — Guard (svex-envlist-p envs).
Returns: val — Type (4vec-p val).

Definitions and Theorems

Function: lhprobe/4vec-eval

(defun lhprobe/4vec-eval (x envs)
  (declare (xargs :guard (and (lhprobe/4vec-p x)
                              (svex-envlist-p envs))))
  (let ((__function__ 'lhprobe/4vec-eval))
    (declare (ignorable __function__))
    (lhprobe/4vec-case x
                       :lhprobe (lhprobe-eval x envs)
                       :4vec (4vec-fix x))))

Theorem: 4vec-p-of-lhprobe/4vec-eval

(defthm 4vec-p-of-lhprobe/4vec-eval
  (b* ((val (lhprobe/4vec-eval x envs)))
    (4vec-p val))
  :rule-classes :rewrite)

Theorem: lhprobe/4vec-eval-of-lhprobe/4vec-fix-x

(defthm lhprobe/4vec-eval-of-lhprobe/4vec-fix-x
  (equal (lhprobe/4vec-eval (lhprobe/4vec-fix x)
                            envs)
         (lhprobe/4vec-eval x envs)))

Theorem: lhprobe/4vec-eval-lhprobe/4vec-equiv-congruence-on-x

(defthm lhprobe/4vec-eval-lhprobe/4vec-equiv-congruence-on-x
  (implies (lhprobe/4vec-equiv x x-equiv)
           (equal (lhprobe/4vec-eval x envs)
                  (lhprobe/4vec-eval x-equiv envs)))
  :rule-classes :congruence)

Theorem: lhprobe/4vec-eval-of-svex-envlist-fix-envs

(defthm lhprobe/4vec-eval-of-svex-envlist-fix-envs
  (equal (lhprobe/4vec-eval x (svex-envlist-fix envs))
         (lhprobe/4vec-eval x envs)))

Theorem: lhprobe/4vec-eval-svex-envlist-equiv-congruence-on-envs

(defthm lhprobe/4vec-eval-svex-envlist-equiv-congruence-on-envs
  (implies (svex-envlist-equiv envs envs-equiv)
           (equal (lhprobe/4vec-eval x envs)
                  (lhprobe/4vec-eval x envs-equiv)))
  :rule-classes :congruence)