Basic theorems about matchstatelist-p, generated by std::deflist.
Theorem:
(defthm matchstatelist-p-of-cons (equal (matchstatelist-p (cons acl2::a acl2::x)) (and (matchstate-p acl2::a) (matchstatelist-p acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm matchstatelist-p-of-cdr-when-matchstatelist-p (implies (matchstatelist-p (double-rewrite acl2::x)) (matchstatelist-p (cdr acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm matchstatelist-p-when-not-consp (implies (not (consp acl2::x)) (equal (matchstatelist-p acl2::x) (not acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm matchstate-p-of-car-when-matchstatelist-p (implies (matchstatelist-p acl2::x) (iff (matchstate-p (car acl2::x)) (or (consp acl2::x) (matchstate-p nil)))) :rule-classes ((:rewrite)))
Theorem:
(defthm true-listp-when-matchstatelist-p-compound-recognizer (implies (matchstatelist-p acl2::x) (true-listp acl2::x)) :rule-classes :compound-recognizer)
Theorem:
(defthm matchstatelist-p-of-list-fix (implies (matchstatelist-p acl2::x) (matchstatelist-p (list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm matchstatelist-p-of-rev (equal (matchstatelist-p (rev acl2::x)) (matchstatelist-p (list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm matchstatelist-p-of-append (equal (matchstatelist-p (append acl2::a acl2::b)) (and (matchstatelist-p (list-fix acl2::a)) (matchstatelist-p acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm matchstatelist-p-of-rcons (iff (matchstatelist-p (rcons acl2::a acl2::x)) (and (matchstate-p acl2::a) (matchstatelist-p (list-fix acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm matchstate-p-when-member-equal-of-matchstatelist-p (and (implies (and (member-equal acl2::a acl2::x) (matchstatelist-p acl2::x)) (matchstate-p acl2::a)) (implies (and (matchstatelist-p acl2::x) (member-equal acl2::a acl2::x)) (matchstate-p acl2::a))) :rule-classes ((:rewrite)))
Theorem:
(defthm matchstatelist-p-when-subsetp-equal (and (implies (and (subsetp-equal acl2::x acl2::y) (matchstatelist-p acl2::y)) (equal (matchstatelist-p acl2::x) (true-listp acl2::x))) (implies (and (matchstatelist-p acl2::y) (subsetp-equal acl2::x acl2::y)) (equal (matchstatelist-p acl2::x) (true-listp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm matchstatelist-p-of-set-difference-equal (implies (matchstatelist-p acl2::x) (matchstatelist-p (set-difference-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm matchstatelist-p-of-intersection-equal-1 (implies (matchstatelist-p (double-rewrite acl2::x)) (matchstatelist-p (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm matchstatelist-p-of-intersection-equal-2 (implies (matchstatelist-p (double-rewrite acl2::y)) (matchstatelist-p (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm matchstatelist-p-of-union-equal (equal (matchstatelist-p (union-equal acl2::x acl2::y)) (and (matchstatelist-p (list-fix acl2::x)) (matchstatelist-p (double-rewrite acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm matchstatelist-p-of-undup (implies (matchstatelist-p x) (matchstatelist-p (undup x))) :rule-classes ((:rewrite)))