		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Lhprobe-map-eval

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

Definitions and Theorems

Function: lhprobe-map-eval

(defun lhprobe-map-eval (x envs)
  (declare (xargs :guard (and (lhprobe-map-p x)
                              (svex-envlist-p envs))))
  (let ((__function__ 'lhprobe-map-eval))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((unless (mbt (and (consp (car x))
                            (svar-p (caar x)))))
          (lhprobe-map-eval (cdr x) envs)))
      (cons (cons (caar x)
                  (lhprobe-eval (cdar x) envs))
            (lhprobe-map-eval (cdr x) envs)))))

Theorem: svex-env-p-of-lhprobe-map-eval

(defthm svex-env-p-of-lhprobe-map-eval
  (b* ((eval (lhprobe-map-eval x envs)))
    (svex-env-p eval))
  :rule-classes :rewrite)

Theorem: lookup-of-lhprobe-map-eval

(defthm lookup-of-lhprobe-map-eval
  (b* ((common-lisp::?eval (lhprobe-map-eval x envs)))
    (equal (svex-env-lookup v eval)
           (let ((look (hons-assoc-equal (svar-fix v)
                                         (lhprobe-map-fix x))))
             (if look (lhprobe-eval (cdr look) envs)
               (4vec-x))))))

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

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

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

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

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

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

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

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