(fgl-object-bindings-bfrlist x) → bfrlist
Function:
(defun fgl-object-bindings-bfrlist (x) (declare (xargs :guard (fgl-object-bindings-p x))) (let ((__function__ 'fgl-object-bindings-bfrlist)) (declare (ignorable __function__)) (if (atom x) nil (append (and (mbt (and (consp (car x)) (pseudo-var-p (caar x)))) (fgl-object-bfrlist (cdar x))) (fgl-object-bindings-bfrlist (cdr x))))))
Theorem:
(defthm fgl-object-bindings-bfrlist-of-cons (implies (pseudo-var-p var) (equal (fgl-object-bindings-bfrlist (cons (cons var val) rest)) (append (fgl-object-bfrlist val) (fgl-object-bindings-bfrlist rest)))))
Theorem:
(defthm bfr-listp-of-fgl-object-bindings-bfrlist (implies (fgl-object-bindings-p x) (equal (fgl-bfr-object-bindings-p x) (bfr-listp (fgl-object-bindings-bfrlist x)))))
Theorem:
(defthm fgl-object-bindings-bfrlist-of-fgl-object-bindings-fix-x (equal (fgl-object-bindings-bfrlist (fgl-object-bindings-fix x)) (fgl-object-bindings-bfrlist x)))
Theorem:
(defthm fgl-object-bindings-bfrlist-fgl-object-bindings-equiv-congruence-on-x (implies (fgl-object-bindings-equiv x x-equiv) (equal (fgl-object-bindings-bfrlist x) (fgl-object-bindings-bfrlist x-equiv))) :rule-classes :congruence)