Recognizer for char-val-set.
(char-val-setp x) → *
Function:
(defun char-val-setp (x) (declare (xargs :guard t)) (if (atom x) (null x) (and (char-val-p (car x)) (or (null (cdr x)) (and (consp (cdr x)) (acl2::fast-<< (car x) (cadr x)) (char-val-setp (cdr x)))))))
Theorem:
(defthm booleanp-ofchar-val-setp (booleanp (char-val-setp x)))
Theorem:
(defthm setp-when-char-val-setp (implies (char-val-setp x) (setp x)) :rule-classes (:rewrite))
Theorem:
(defthm char-val-p-of-head-when-char-val-setp (implies (char-val-setp x) (equal (char-val-p (head x)) (not (emptyp x)))))
Theorem:
(defthm char-val-setp-of-tail-when-char-val-setp (implies (char-val-setp x) (char-val-setp (tail x))))
Theorem:
(defthm char-val-setp-of-insert (equal (char-val-setp (insert a x)) (and (char-val-p a) (char-val-setp (sfix x)))))
Theorem:
(defthm char-val-p-when-in-char-val-setp-binds-free-x (implies (and (in a x) (char-val-setp x)) (char-val-p a)))
Theorem:
(defthm char-val-setp-of-union (equal (char-val-setp (union x y)) (and (char-val-setp (sfix x)) (char-val-setp (sfix y)))))
Theorem:
(defthm char-val-setp-of-intersect (implies (and (char-val-setp x) (char-val-setp y)) (char-val-setp (intersect x y))))
Theorem:
(defthm char-val-setp-of-difference (implies (char-val-setp x) (char-val-setp (difference x y))))
Theorem:
(defthm char-val-setp-of-delete (implies (char-val-setp x) (char-val-setp (delete a x))))