1\DOC EXISTS_AND_REORDER_CONV
2
3\TYPE {EXISTS_AND_REORDER_CONV : conv}
4
5\SYNOPSIS
6Moves an existential quantification inwards through a conjunction,
7sorting the body.
8
9\KEYWORDS
10conversion, quantifier, existential, conjunction.
11
12\DESCRIBE
13When applied to a term of the form {?x. c1 /\ c2 /\ .. /\ cn}, where
14{x} is not free in at least one of the conjuncts {ci}, then
15{EXISTS_AND_REORDER_CONV} returns a theorem of the form
16{
17   |- (?x. ...) = (ci /\ cj /\ ck /\ ...) /\ (?x. cm /\ cn /\ cp /\ ...)
18}
19where the conjuncts {ci}, {cj} and {ck} do not have the bound variable
20{x} free, and where the conjuncts {cm}, {cn} and {cp} do.
21
22\FAILURE
23{EXISTS_AND_REORDER_CONV} fails if it is applied to a term that is not
24an existential.  It raises {UNCHANGED} if the existential's body is
25not a conjunction, or if the body does not have any conjuncts where
26the bound variable does not occur, or if none of the body's conjuncts
27have free occurrences of the bound variable.
28
29\COMMENTS
30The conjuncts in the resulting term are kept in the same relative
31order as in the input term, but will all be right-associated in the
32two groups (because they are re-assembled with {list_mk_conj}),
33possibly destroying structure that existed in the original.
34
35\SEEALSO
36Conv.EXISTS_AND_CONV.
37\ENDDOC
38