		Search-engine friendly clone of the ACL2 documentation.

Bfr-eval-cp

Instantiate-equals-with-bfr-evals

Signature
(instantiate-equals-with-bfr-evals clause vals bfr-terms patterns) → *

Definitions and Theorems

Function: instantiate-equals-with-bfr-evals

(defun instantiate-equals-with-bfr-evals
       (clause vals bfr-terms patterns)
 (declare (xargs :guard t))
 (let ((__function__ 'instantiate-equals-with-bfr-evals))
  (declare (ignorable __function__))
  (if (atom clause)
      nil
   (let*
    ((rst-clause
        (instantiate-equals-with-bfr-evals (cdr clause)
                                           vals bfr-terms patterns))
     (lit (car clause)))
    (mv-let (a b)
            (case-match lit
              (('not ('equal a b)) (mv a b))
              (a (mv a ''nil))
              (& (mv nil nil)))
      (if (and (bfr-termp a bfr-terms patterns)
               (bfr-termp b bfr-terms patterns))
          (cons (disjoin (instantiate-bfr-evals a b vals))
                rst-clause)
        (cons lit rst-clause)))))))

Theorem: instantiate-equals-with-bfr-evals-correct

(defthm instantiate-equals-with-bfr-evals-correct
  (implies (bfr-cp-ev (disjoin (instantiate-equals-with-bfr-evals
                                    clause vals bfr-terms patterns))
                      a)
           (bfr-cp-ev (disjoin clause) a)))

Theorem: pseudo-term-listp-instantiate-equals-with-bfr-evals

(defthm pseudo-term-listp-instantiate-equals-with-bfr-evals
 (implies (and (pseudo-term-listp clause)
               (pseudo-term-listp vals))
          (pseudo-term-listp (instantiate-equals-with-bfr-evals
                                  clause vals bfr-terms patterns))))