Basic theorems about bfr-listp$, generated by deflist.
Theorem:
(defthm bfr-listp$-of-cons (equal (bfr-listp$ (cons a x) bfrstate) (and (bfr-p a) (bfr-listp$ x bfrstate))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-cdr-when-bfr-listp$ (implies (bfr-listp$ (double-rewrite x) bfrstate) (bfr-listp$ (cdr x) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-when-not-consp (implies (not (consp x)) (bfr-listp$ x bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-p-of-car-when-bfr-listp$ (implies (bfr-listp$ x bfrstate) (bfr-p (car x))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-append (equal (bfr-listp$ (append a b) bfrstate) (and (bfr-listp$ a bfrstate) (bfr-listp$ b bfrstate))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-list-fix (equal (bfr-listp$ (list-fix x) bfrstate) (bfr-listp$ x bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-sfix (iff (bfr-listp$ (set::sfix x) bfrstate) (or (bfr-listp$ x bfrstate) (not (set::setp x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-insert (iff (bfr-listp$ (set::insert a x) bfrstate) (and (bfr-listp$ (set::sfix x) bfrstate) (bfr-p a))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-delete (implies (bfr-listp$ x bfrstate) (bfr-listp$ (set::delete k x) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-mergesort (iff (bfr-listp$ (set::mergesort x) bfrstate) (bfr-listp$ (list-fix x) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-union (iff (bfr-listp$ (set::union x y) bfrstate) (and (bfr-listp$ (set::sfix x) bfrstate) (bfr-listp$ (set::sfix y) bfrstate))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-intersect-1 (implies (bfr-listp$ x bfrstate) (bfr-listp$ (set::intersect x y) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-intersect-2 (implies (bfr-listp$ y bfrstate) (bfr-listp$ (set::intersect x y) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-difference (implies (bfr-listp$ x bfrstate) (bfr-listp$ (set::difference x y) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-duplicated-members (implies (bfr-listp$ x bfrstate) (bfr-listp$ (acl2::duplicated-members x) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-rev (equal (bfr-listp$ (rev x) bfrstate) (bfr-listp$ (list-fix x) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-rcons (iff (bfr-listp$ (acl2::rcons a x) bfrstate) (and (bfr-p a) (bfr-listp$ (list-fix x) bfrstate))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-p-when-member-equal-of-bfr-listp$ (and (implies (and (member-equal a x) (bfr-listp$ x bfrstate)) (bfr-p a)) (implies (and (bfr-listp$ x bfrstate) (member-equal a x)) (bfr-p a))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-when-subsetp-equal (and (implies (and (subsetp-equal x y) (bfr-listp$ y bfrstate)) (bfr-listp$ x bfrstate)) (implies (and (bfr-listp$ y bfrstate) (subsetp-equal x y)) (bfr-listp$ x bfrstate))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-set-equiv-congruence (implies (set-equiv x y) (equal (bfr-listp$ x bfrstate) (bfr-listp$ y bfrstate))) :rule-classes :congruence)
Theorem:
(defthm bfr-listp$-of-set-difference-equal (implies (bfr-listp$ x bfrstate) (bfr-listp$ (set-difference-equal x y) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-intersection-equal-1 (implies (bfr-listp$ (double-rewrite x) bfrstate) (bfr-listp$ (intersection-equal x y) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-intersection-equal-2 (implies (bfr-listp$ (double-rewrite y) bfrstate) (bfr-listp$ (intersection-equal x y) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-union-equal (equal (bfr-listp$ (union-equal x y) bfrstate) (and (bfr-listp$ (list-fix x) bfrstate) (bfr-listp$ (double-rewrite y) bfrstate))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-take (implies (bfr-listp$ (double-rewrite x) bfrstate) (iff (bfr-listp$ (take n x) bfrstate) (or (bfr-p nil) (<= (nfix n) (len x))))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-repeat (iff (bfr-listp$ (acl2::repeat n x) bfrstate) (or (bfr-p x) (zp n))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-p-of-nth-when-bfr-listp$ (implies (bfr-listp$ x bfrstate) (bfr-p (nth n x))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-update-nth (implies (bfr-listp$ (double-rewrite x) bfrstate) (iff (bfr-listp$ (update-nth n y x) bfrstate) (and (bfr-p y) (or (<= (nfix n) (len x)) (bfr-p nil))))) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-butlast (implies (bfr-listp$ (double-rewrite x) bfrstate) (bfr-listp$ (butlast x n) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-nthcdr (implies (bfr-listp$ (double-rewrite x) bfrstate) (bfr-listp$ (nthcdr n x) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-last (implies (bfr-listp$ (double-rewrite x) bfrstate) (bfr-listp$ (last x) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-remove (implies (bfr-listp$ x bfrstate) (bfr-listp$ (remove a x) bfrstate)) :rule-classes ((:rewrite)))
Theorem:
(defthm bfr-listp$-of-revappend (equal (bfr-listp$ (revappend x y) bfrstate) (and (bfr-listp$ (list-fix x) bfrstate) (bfr-listp$ y bfrstate))) :rule-classes ((:rewrite)))