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