1\DOC AND_EXISTS_CONV 2 3\TYPE {AND_EXISTS_CONV : conv} 4 5\SYNOPSIS 6Moves an existential quantification outwards through a conjunction. 7 8\KEYWORDS 9conversion, quantifier. 10 11\DESCRIBE 12When applied to a term of the form {(?x.P) /\ (?x.Q)}, where {x} is free 13in neither {P} nor {Q}, {AND_EXISTS_CONV} returns the theorem: 14{ 15 |- (?x. P) /\ (?x. Q) = (?x. P /\ Q) 16} 17 18 19\FAILURE 20{AND_EXISTS_CONV} fails if it is applied to a term not of the form 21{(?x.P) /\ (?x.Q)}, or if it is applied to a term {(?x.P) /\ (?x.Q)} 22in which the variable {x} is free in either {P} or {Q}. 23 24\COMMENTS 25It may be easier to use higher order rewriting with some of 26{BOTH_EXISTS_AND_THM}, {LEFT_EXISTS_AND_THM}, and 27{RIGHT_EXISTS_AND_THM}. 28 29 30 31\SEEALSO 32Conv.EXISTS_AND_CONV, Conv.LEFT_AND_EXISTS_CONV, Conv.RIGHT_AND_EXISTS_CONV. 33 34\ENDDOC 35