(bfr-listp$ x bfrstate) recognizes lists where every element satisfies bfr-p.
(bfr-listp$ x bfrstate) → std::bool
This is an ordinary deflist. It is
"loose" in that it does not care whether
Function:
(defun bfr-listp$ (x bfrstate) (declare (xargs :guard (bfrstate-p bfrstate))) (let ((__function__ 'bfr-listp$)) (declare (ignorable __function__)) (if (consp x) (and (bfr-p (car x)) (bfr-listp$ (cdr x) bfrstate)) t)))
Theorem:
(defthm bfr-listp$-of-bfrstate-fix-bfrstate (equal (bfr-listp$ x (bfrstate-fix bfrstate)) (bfr-listp$ x bfrstate)))
Theorem:
(defthm bfr-listp$-bfrstate-equiv-congruence-on-bfrstate (implies (bfrstate-equiv bfrstate bfrstate-equiv) (equal (bfr-listp$ x bfrstate) (bfr-listp$ x bfrstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm bfr-listp-of-nil (bfr-listp nil))
Theorem:
(defthm bfr-listp-when-bfrstate>= (implies (and (bfrstate>= new old) (bfr-listp x old)) (bfr-listp x new)))