Major Section: TAU-SYSTEM

General Form: (in-tau-intervalp e x)

Here, `x`

should be an interval (see `tau-intervalp`

). This function
returns `t`

or `nil`

indicating whether `e`

, which is generally but not
necessarily a number, is an element of interval `x`

. By that is meant that
`e`

satisfies the domain predicate of the interval and lies between the two
bounds.

Suppose `x`

is an interval with the components *dom*, *lo-rel*, *lo*,
*hi-rel* and *hi*. Suppose `(<? `

*rel u v*`)`

means `(< `

*u v*`)`

when *rel* is true and `(<= `

*u v*`)`

otherwise, with appropriate
treatment of infinities.

Then for `e`

to be in interval `x`

, it must be the case that `e`

satisfies the domain predicate *dom* (where where *dom*=`nil`

means
there is no restriction on the domain) and `(<? `

*lo-rel lo*` e)`

and
`(<? `

*hi-rel*` e `

*hi*`)`

. [Note: ``Appropriate treatment of
infinities'' is slightly awkward if both infinities are represented by the
same object, `nil`

. However, this is handled by coercing `e`

to a
number *after* checking that it is in the domain. By this trick, ```<?`

''
is presented with at most one ``infinity'' and it is always negative
when in the first argument and positive when in the second.]

Note that every element in an `INTEGERP`

interval is contained in the
analogous `RATIONALP`

interval (i.e., the interval obtained by just
replacing the domain `INTEGERP`

by `RATIONALP`

). That is because every
integer is a rational. Similarly, every rational is an ACL2 number.

Note that an interval in which the relations are weak and the bounds are equal rationals is the ``unit'' or ``identity'' interval containing exactly that rational.

Note that an interval in which the relations are strong and the bounds are equal rationals is empty: it contains no objects.

Note that the interval `(make-tau-interval nil nil nil nil nil)`

is the
``universal interval:'' it contains all ACL2 objects. It contains all
numbers because they statisfy the non-existent domain restriction and lie
between minus infinity and plus infinity. It contains all non-numbers
because the interval contains `0`

and ACL2's inequalities coerce
non-numbers to `0`

. The universal interval is useful if you are defining a
bounder (see bounders) for a function and do not wish to address a certain
case: return the universal interval.

Recall that `make-tau-interval`

constructs intervals. Using `make-tau-interval`

we give several self-explanatory examples of `in-tau-intervalp`

:

(in-tau-intervalp 3 (make-tau-interval 'INTEGERP nil 0 nil 10)) = t (in-tau-intervalp 3 (make-tau-interval 'RATIONALP nil 0 nil 10)) = t (in-tau-intervalp 3 (make-tau-interval NIL nil 0 nil 10)) = t (in-tau-intervalp -3 (make-tau-interval 'INTEGERP nil 0 nil 10)) = nil (in-tau-intervalp 30 (make-tau-interval 'INTEGERP nil 0 nil 10)) = nil (in-tau-intervalp 3/5 (make-tau-interval 'INTEGERP nil 0 nil 10)) = nil (in-tau-intervalp 3/5 (make-tau-interval 'RATIONALP nil 0 nil 10)) = t (in-tau-intervalp #c(3 5) (make-tau-interval 'RATIONALP nil 0 nil 10)) = nil (in-tau-intervalp #c(3 5) (make-tau-interval 'ACL2-NUMBERP nil 0 nil 10)) = t (in-tau-intervalp 'ABC (make-tau-interval NIL nil 0 nil 10)) = t