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