Determines whether a formula is in prenex normal form.
DESCRIPTION
This function returns true if the term it is given as argument is in prenex
normal form. If the term is not a formula the result will be true provided
there are no nested Boolean expressions involving quantifiers.
FAILURE
Never fails.
EXAMPLE
- is_prenex ``!x. ?y. x \/ y``;
> val it = true : bool
- is_prenex ``!x. x ==> (?y. x /\ y)``;
> val it = false : bool
USES
Useful for determining whether it is necessary to apply a prenex normaliser to
a formula before passing it to a function which requires the formula to be in
prenex normal form.