EXISTS_AND_REORDER_CONVConv.EXISTS_AND_REORDER_CONV : convMoves an existential quantification inwards through a conjunction, sorting the body.
When applied to a term of the form
?x. c1 /\ c2 /\ .. /\ cn, where x is not free
in at least one of the conjuncts ci, then
EXISTS_AND_REORDER_CONV returns a theorem of the form
|- (?x. ...) = (ci /\ cj /\ ck /\ ...) /\ (?x. cm /\ cn /\ cp /\ ...)where the conjuncts ci, cj and
ck do not have the bound variable x free, and
where the conjuncts cm, cn and cp
do.
EXISTS_AND_REORDER_CONV fails if it is applied to a term
that is not an existential. It raises UNCHANGED if the
existential’s body is not a conjunction, or if the body does not have
any conjuncts where the bound variable does not occur, or if none of the
body’s conjuncts have free occurrences of the bound variable.
The conjuncts in the resulting term are kept in the same relative
order as in the input term, but will all be right-associated in the two
groups (because they are re-assembled with list_mk_conj),
possibly destroying structure that existed in the original.