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