		Search-engine friendly clone of the ACL2 documentation.

Bfr-listp$

(bfr-listp$ x bfrstate) recognizes lists where every element satisfies bfr-p.

Signature
(bfr-listp$ x bfrstate) → std::bool

This is an ordinary deflist. It is "loose" in that it does not care whether x is nil-terminated.

Definitions and Theorems

Function: bfr-listp$

(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: bfr-listp$-of-bfrstate-fix-bfrstate

(defthm bfr-listp$-of-bfrstate-fix-bfrstate
  (equal (bfr-listp$ x (bfrstate-fix bfrstate))
         (bfr-listp$ x bfrstate)))

Theorem: bfr-listp$-bfrstate-equiv-congruence-on-bfrstate

(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: bfr-listp-of-nil

(defthm bfr-listp-of-nil
  (bfr-listp nil))

Theorem: bfr-listp-when-bfrstate>=

(defthm bfr-listp-when-bfrstate>=
  (implies (and (bfrstate>= new old)
                (bfr-listp x old))
           (bfr-listp x new)))

Subtopics

Bfr-listp$-basics: Basic theorems about bfr-listp$, generated by deflist.