Boolean recognizer for tau intervals

General Form: (tau-intervalp x)

An interval is a structure of the form: *dom*
*lo-rel* *lo**hi-rel* *hi*

Restrictions on the components of an interval are as follows. For an
interpretation of the meaning of the components, see `in-tau-intervalp`
or `make-tau-interval`.

*Dom* (``domain'') must be one of four symbols:

The two ``relations,'' *lo-rel* and *hi-rel*, must be
Booleans.

*Lo* and *hi* must be either *Lo* must be no greater than *hi* (where *lo* and *hi*
respectively.

Finally, if the *dom* is *lo* and *hi* must be integers when they are
non-

Recall that `make-tau-interval` constructs intervals. The intervals
it constructs are well-formed only if the arguments to

; integers: 0 <= x <= 10: (tau-intervalp (make-tau-interval 'INTEGERP nil 0 nil 10)) = t ; integers: 0 <= x (i.e., the natural numbers): (tau-intervalp (make-tau-interval 'INTEGERP nil 0 nil nil)) = t ; violations of domain rules: (tau-intervalp (make-tau-interval 'INTEGERP t 0 t 10)) = nil (tau-intervalp (make-tau-interval 'INTEGERP nil 0 nil 10/11)) = nil ; violation of rule that bounds must be rational if non-nil: (tau-intervalp (make-tau-interval 'ACL2-NUMBERP t 0 t #c(3 5))) = nil ; violation of rule that lo <= hi: (tau-intervalp (make-tau-interval 'ACL2-NUMBERP t 0 t -10)) = nil ; rationals: 0 < x <= 22/7: (tau-intervalp (make-tau-interval 'RATIONALP t 0 nil 22/7)) = t ; numbers: -10 < x < 10: (tau-intervalp (make-tau-interval 'ACL2-NUMBERP t -10 t 10)) = t ; any: -10 < x < 10: (tau-intervalp (make-tau-interval nil t -10 t 10)) = t : any: (tau-intervalp (make-tau-interval nil nil nil nil nil)) = t

Note that the second-to-last interval, with domain

Note that the last interval contains all ACL2 objects. It is called the ``universal interval.''