(bfr-list-fix x &optional (bfrstate 'bfrstate)) → new-x
Function:
(defun bfr-list-fix-fn (x bfrstate) (declare (xargs :guard (and (bfrstate-p bfrstate) (bfr-listp x)))) (let ((__function__ 'bfr-list-fix)) (declare (ignorable __function__)) (mbe :logic (if (atom x) x (cons (bfr-fix (car x)) (bfr-list-fix (cdr x)))) :exec x)))
Theorem:
(defthm bfr-listp-of-bfr-list-fix (b* ((new-x (bfr-list-fix-fn x bfrstate))) (bfr-listp new-x)) :rule-classes :rewrite)
Theorem:
(defthm bfr-list-fix-when-bfr-listp (b* nil (implies (bfr-listp x) (equal (bfr-list-fix x) x))))
Theorem:
(defthm car-of-bfr-list-fix (b* nil (implies (consp x) (equal (car (bfr-list-fix x)) (bfr-fix (car x))))))
Theorem:
(defthm cdr-of-bfr-list-fix (b* nil (implies (consp x) (equal (cdr (bfr-list-fix x)) (bfr-list-fix (cdr x))))))
Theorem:
(defthm consp-of-bfr-list-fix (b* nil (equal (consp (bfr-list-fix x)) (consp x))))
Theorem:
(defthm len-of-bfr-list-fix (b* nil (equal (len (bfr-list-fix x)) (len x))))
Theorem:
(defthm bfr-list-fix-fn-of-bfrstate-fix-bfrstate (equal (bfr-list-fix-fn x (bfrstate-fix bfrstate)) (bfr-list-fix-fn x bfrstate)))
Theorem:
(defthm bfr-list-fix-fn-bfrstate-equiv-congruence-on-bfrstate (implies (bfrstate-equiv bfrstate bfrstate-equiv) (equal (bfr-list-fix-fn x bfrstate) (bfr-list-fix-fn x bfrstate-equiv))) :rule-classes :congruence)