(bfr-listp-witness x bfrstate) → *
Function:
(defun bfr-listp-witness (x bfrstate) (declare (xargs :guard (bfrstate-p bfrstate))) (let ((__function__ 'bfr-listp-witness)) (declare (ignorable __function__)) (if (atom x) 'not-a-bfr (if (bfr-p (car x)) (bfr-listp-witness (cdr x) bfrstate) (car x)))))
Theorem:
(defthm bfr-listp-witness-nonnil (bfr-listp-witness x bfrstate))
Theorem:
(defthm bfr-listp-witness-not-bfr-p (not (bfr-p (bfr-listp-witness x bfrstate) bfrstate)))
Theorem:
(defthm bfr-listp-when-not-member-witness (implies (not (member (bfr-listp-witness x bfrstate) x)) (bfr-listp x bfrstate)))
Theorem:
(defthm not-member-bfr-listp-witness-when-bfr-listp (implies (bfr-listp x bfrstate) (not (member (bfr-listp-witness y bfrstate) x))))
Theorem:
(defthm bfr-listp-witness-of-bfrstate-fix-bfrstate (equal (bfr-listp-witness x (bfrstate-fix bfrstate)) (bfr-listp-witness x bfrstate)))
Theorem:
(defthm bfr-listp-witness-bfrstate-equiv-congruence-on-bfrstate (implies (bfrstate-equiv bfrstate bfrstate-equiv) (equal (bfr-listp-witness x bfrstate) (bfr-listp-witness x bfrstate-equiv))) :rule-classes :congruence)