1signature OmegaSymbolic =
2sig
3
4  include Abbrev
5
6  val eliminate_an_existential : conv
7  val sym_normalise : conv
8  val findelim_deep_existential : conv
9
10end
11
12(*
13    [eliminate_an_existential t] with t of the form
14       ?x1..xn. body
15    and body a conjunction of normalised <= and int_divides terms.
16    The latter may be negated.  Eliminates one of the existential
17    variables, picking the "best" one to eliminate.
18
19    [sym_normalise t] with t of the form
20       ?x1..xn. body
21    and with body of just about any quantifier-free form
22    as long as the leaves are relations over integer expressions.
23
24    [findelim_deep_existential t] with t of any form (other than that
25    leaves are relations over integer expressions), finds a quantifier
26    with scope over no others and eliminates it.
27
28*)
29