PairRules.PEXISTS_AND

STRUCTURE

LIBRARY

pair

SYNOPSIS

Moves a paired existential quantification inwards through a conjunction.

DESCRIPTION

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

EXISTS_AND_CONV, AND_PEXISTS_CONV, LEFT_AND_PEXISTS_CONV, RIGHT_AND_PEXISTS_CONV