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