----------------------------------------------------------------------
PEXISTS_AND_CONV                                           (PairRules)
----------------------------------------------------------------------
PEXISTS_AND_CONV : conv

KEYWORDS
conversion, quantifier, existential, conjunction.

LIBRARY
pair

SYNOPSIS
Moves a paired existential quantification inwards through a conjunction.

DESCRIBE
When applied to a term of the form {?p. t /\ u}, where variables in {p} are
not free in both {t} and {u}, {PEXISTS_AND_CONV} returns a theorem of one of
three forms, depending on occurrences of variables from {p} in {t} and {u}.
If {p} contains variables free in {t} but none in {u}, then the theorem:

   |- (?p. t /\ u) = (?p. t) /\ u

is returned.  If {p} contains variables free in {u} but none in {t},
then the result is:

   |- (?p. t /\ u) = t /\ (?x. u)

And if {p} does not contain any variable free in either {t} nor {u},
then the result is:

   |- (?p. t /\ u) = (?x. t) /\ (?x. u)




FAILURE
{PEXISTS_AND_CONV} fails if it is applied to a term not of the form
{?p. t /\ u}, or if it is applied to a term {?p. t /\ u} in which
variables in {p} are free in both {t} and {u}.

SEEALSO
Conv.EXISTS_AND_CONV, PairRules.AND_PEXISTS_CONV,
PairRules.LEFT_AND_PEXISTS_CONV, PairRules.RIGHT_AND_PEXISTS_CONV.

----------------------------------------------------------------------