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