----------------------------------------------------------------------
PFORALL_OR_CONV                                            (PairRules)
----------------------------------------------------------------------
PFORALL_OR_CONV : conv

KEYWORDS
conversion, quantifier, universal, disjunction.

LIBRARY
pair

SYNOPSIS
Moves a paired universal quantification inwards through a disjunction.

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

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

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

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

And if no variable from {p} is free in either {t} nor {u},
then the result is:

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




FAILURE
{PFORALL_OR_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 from {p} are free in both {t} and {u}.

SEEALSO
Conv.FORALL_OR_CONV, PairRules.OR_PFORALL_CONV,
PairRules.LEFT_OR_PFORALL_CONV, PairRules.RIGHT_OR_PFORALL_CONV.

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