(fgl-bfr-object-bindings-p x &optional (bfrstate 'bfrstate)) → *
Function:
(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:
(defthm fgl-bfr-object-bindings-p-implies-fgl-object-bindings-p (implies (fgl-bfr-object-bindings-p x) (fgl-object-bindings-p x)))
Theorem:
(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:
(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)