		Search-engine friendly clone of the ACL2 documentation.

Fgl-bfr-object-bindings-p

Signature
(fgl-bfr-object-bindings-p x &optional (bfrstate 'bfrstate)) → *
Arguments: bfrstate — Guard (bfrstate-p bfrstate).

Definitions and Theorems

Function: fgl-bfr-object-bindings-p-fn

(defun fgl-bfr-object-bindings-p-fn (x bfrstate)
  (declare (xargs :guard (bfrstate-p bfrstate)))
  (let ((__function__ 'fgl-bfr-object-bindings-p))
    (declare (ignorable __function__))
    (if (atom x)
        (eq x nil)
      (and (consp (car x))
           (pseudo-var-p (caar x))
           (fgl-bfr-object-p (cdar x))
           (fgl-bfr-object-bindings-p (cdr x))))))

Theorem: fgl-bfr-object-bindings-p-implies-fgl-object-bindings-p

(defthm fgl-bfr-object-bindings-p-implies-fgl-object-bindings-p
  (implies (fgl-bfr-object-bindings-p x)
           (fgl-object-bindings-p x)))

Theorem: fgl-bfr-object-bindings-p-fn-of-bfrstate-fix-bfrstate

(defthm fgl-bfr-object-bindings-p-fn-of-bfrstate-fix-bfrstate
  (equal (fgl-bfr-object-bindings-p-fn x (bfrstate-fix bfrstate))
         (fgl-bfr-object-bindings-p-fn x bfrstate)))

Theorem: fgl-bfr-object-bindings-p-fn-bfrstate-equiv-congruence-on-bfrstate

(defthm
 fgl-bfr-object-bindings-p-fn-bfrstate-equiv-congruence-on-bfrstate
 (implies (bfrstate-equiv bfrstate bfrstate-equiv)
          (equal (fgl-bfr-object-bindings-p-fn x bfrstate)
                 (fgl-bfr-object-bindings-p-fn x bfrstate-equiv)))
 :rule-classes :congruence)