		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Lhprobe-map-overridemux-eval

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

Definitions and Theorems

Function: lhprobe-map-overridemux-eval

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

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

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

Theorem: lookup-of-lhprobe-map-overridemux-eval

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

Theorem: boundp-of-lhprobe-map-overridemux-eval

(defthm boundp-of-lhprobe-map-overridemux-eval
  (b*
   ((common-lisp::?eval (lhprobe-map-overridemux-eval x envs outs)))
   (iff (svex-env-boundp v eval)
        (hons-assoc-equal (svar-fix v)
                          (lhprobe-map-fix x)))))

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

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

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

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

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

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

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

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

Theorem: lhprobe-map-overridemux-eval-of-svex-envlist-fix-outs

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

Theorem: lhprobe-map-overridemux-eval-svex-envlist-equiv-congruence-on-outs

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