		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Svdecomp-equal-svexlist-evals-metafun

Signature
(svdecomp-equal-svexlist-evals-metafun x mfc state) → newx
Arguments: x — Guard (pseudo-termp x).
Returns: newx — Type (pseudo-termp newx), given the guard.

Definitions and Theorems

Function: svdecomp-equal-svexlist-evals-metafun

(defun svdecomp-equal-svexlist-evals-metafun (x mfc state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (pseudo-termp x)))
 (declare (ignorable mfc))
 (let ((__function__ 'svdecomp-equal-svexlist-evals-metafun))
  (declare (ignorable __function__))
  (b*
   (((acl2::when-match
          x
          (equal (svexlist-eval '(:? svexes1) (:? env1))
                 (svexlist-eval '(:? svexes2)
                                (:? env2))))
     (cwtime
      (b*
       (((unless (and (svexlist-p svexes1)
                      (svexlist-p svexes2)))
         (cw
          "svdecomp-equal-svexlist-evals-meta failed because the svex was not svex-p~%")
         x)
        ((mv err symenv1)
         (map-alist-term-keys-to-val-terms env1))
        ((when err)
         (cw
          "svdecomp-equal-svexlist-evals-meta failed to process the environment term: ~@0~%"
          err)
         x)
        ((mv err symenv2)
         (map-alist-term-keys-to-val-terms env2))
        ((when err)
         (cw
          "svdecomp-equal-svexlist-evals-meta failed to process the environment term: ~@0~%"
          err)
         x)
        ((mv newsvexes1 newenv1)
         (svdecomp-normalize-svexlist-eval svexes1 symenv1 10))
        ((mv newsvexes2 newenv2)
         (svdecomp-normalize-svexlist-eval svexes2 symenv2 10))
        (limit (svdecomp-get-rewrite-limit state))
        ((mv newsvexes1 newsvexes2)
         (svexlists-rewrite-until-same
              newsvexes1 newsvexes2 limit)))
       (svdecomp-svex?-eval-compare-term
            newsvexes1 newsvexes2
            newenv1 newenv2 'svexlist-eval))
      :name svdecomp-equal-svexlist-evals-metafun)))
   x)))

Theorem: pseudo-termp-of-svdecomp-equal-svexlist-evals-metafun

(defthm pseudo-termp-of-svdecomp-equal-svexlist-evals-metafun
 (implies
    (and (state-p state) (pseudo-termp x))
    (b* ((newx (svdecomp-equal-svexlist-evals-metafun x mfc state)))
      (pseudo-termp newx)))
 :rule-classes :rewrite)

Theorem: svdecomp-equal-svexlist-evals-meta

(defthm svdecomp-equal-svexlist-evals-meta
 (equal
    (svdecomp-ev x a)
    (svdecomp-ev (svdecomp-equal-svexlist-evals-metafun x mfc state)
                 a))
 :rule-classes ((:meta :trigger-fns (equal))))