		Search-engine friendly clone of the ACL2 documentation.

Lhprobe

Lhprobe-eval

Evaluator for an lhprobe with respect to an envlist giving the values of signals over time.

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

Definitions and Theorems

Function: lhprobe-eval

(defun lhprobe-eval (x envs)
  (declare (xargs :guard (and (lhprobe-p x)
                              (svex-envlist-p envs))))
  (let ((__function__ 'lhprobe-eval))
    (declare (ignorable __function__))
    (b* (((lhprobe x)) (env (nth x.stage envs)))
      (if x.signedp (lhs-eval-signx x.lhs env)
        (lhs-eval-zx x.lhs env)))))

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

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

Theorem: lhprobe-eval-of-take

(defthm lhprobe-eval-of-take
  (implies (< (lhprobe->stage x) (nfix n))
           (equal (lhprobe-eval x (take n envs))
                  (lhprobe-eval x envs))))

Theorem: lhprobe-eval-of-lhprobe-fix-x

(defthm lhprobe-eval-of-lhprobe-fix-x
  (equal (lhprobe-eval (lhprobe-fix x) envs)
         (lhprobe-eval x envs)))

Theorem: lhprobe-eval-lhprobe-equiv-congruence-on-x

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

Theorem: lhprobe-eval-of-svex-envlist-fix-envs

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

Theorem: lhprobe-eval-svex-envlist-equiv-congruence-on-envs

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