		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Svdecomp-svex?-eval-compare-term

Signature
(svdecomp-svex?-eval-compare-term x y env1 env2 eval-fn) → eq
Arguments: env1 — Guard (svdecomp-symenv-p env1).; env2 — Guard (svdecomp-symenv-p env2).
Returns: eq — Type (pseudo-termp eq), given (and (svdecomp-symenv-p env1) (svdecomp-symenv-p env2) (symbolp eval-fn) (not (eq eval-fn 'quote))) .

Definitions and Theorems

Function: svdecomp-svex?-eval-compare-term

(defun svdecomp-svex?-eval-compare-term (x y env1 env2 eval-fn)
 (declare (xargs :guard (and (svdecomp-symenv-p env1)
                             (svdecomp-symenv-p env2))))
 (let ((__function__ 'svdecomp-svex?-eval-compare-term))
  (declare (ignorable __function__))
  (if (and (hons-equal x y)
           (hons-equal env1 env2))
      (prog2$ (cw "Resulting svexes are equal~%")
              ''t)
   (prog2$
    (cw "Resulting svexes aren't equal~%")
    (cons 'svdecomp-equal
          (cons (cons eval-fn
                      (cons (cons 'quote (cons x 'nil))
                            (cons (svdecomp-symenv->term env1)
                                  'nil)))
                (cons (cons eval-fn
                            (cons (cons 'quote (cons y 'nil))
                                  (cons (svdecomp-symenv->term env2)
                                        'nil)))
                      'nil)))))))

Theorem: pseudo-termp-of-svdecomp-svex?-eval-compare-term

(defthm pseudo-termp-of-svdecomp-svex?-eval-compare-term
 (implies
   (and (svdecomp-symenv-p env1)
        (svdecomp-symenv-p env2)
        (symbolp eval-fn)
        (not (eq eval-fn 'quote)))
   (b*
     ((eq (svdecomp-svex?-eval-compare-term x y env1 env2 eval-fn)))
     (pseudo-termp eq)))
 :rule-classes :rewrite)

Theorem: svdecomp-svex?-eval-compare-term-correct

(defthm svdecomp-svex?-eval-compare-term-correct
 (equal
  (svdecomp-ev
       (svdecomp-svex?-eval-compare-term x y env1 env2 eval-fn)
       a)
  (equal (svdecomp-ev (cons eval-fn
                            (cons (cons 'quote (cons x 'nil))
                                  (cons (svdecomp-symenv->term env1)
                                        'nil)))
                      a)
         (svdecomp-ev (cons eval-fn
                            (cons (cons 'quote (cons y 'nil))
                                  (cons (svdecomp-symenv->term env2)
                                        'nil)))
                      a))))