PEXISTS_AND_CONV
PairRules.PEXISTS_AND_CONV : conv
Moves a paired existential quantification inwards through a conjunction.
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.
See also
Conv.EXISTS_AND_CONV,
PairRules.AND_PEXISTS_CONV,
PairRules.LEFT_AND_PEXISTS_CONV,
PairRules.RIGHT_AND_PEXISTS_CONV