		Search-engine friendly clone of the ACL2 documentation.

Bfr-eval-cp

Instantiate-bfr-evals

Signature
(instantiate-bfr-evals a b vals) → *

Definitions and Theorems

Function: instantiate-bfr-evals

(defun instantiate-bfr-evals (a b vals)
 (declare (xargs :guard t))
 (let ((__function__ 'instantiate-bfr-evals))
  (declare (ignorable __function__))
  (if (atom vals)
      nil
   (cons
    (cons
      'not
      (cons (cons 'equal
                  (cons (cons 'bfr-eval
                              (cons a (cons (car vals) 'nil)))
                        (cons (cons 'bfr-eval
                                    (cons b (cons (car vals) 'nil)))
                              'nil)))
            'nil))
    (instantiate-bfr-evals a b (cdr vals))))))

Theorem: instantiate-bfr-evals-correct

(defthm instantiate-bfr-evals-correct
 (implies (equal (bfr-cp-ev x a) (bfr-cp-ev y a))
          (not (bfr-cp-ev (disjoin (instantiate-bfr-evals x y vals))
                          a))))

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

(defthm pseudo-term-listp-instantiate-bfr-evals
  (implies (and (pseudo-term-listp vals)
                (pseudo-termp a)
                (pseudo-termp b))
           (pseudo-term-listp (instantiate-bfr-evals a b vals))))