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