PairRules.PFORALL_IMP

STRUCTURE

LIBRARY

pair

SYNOPSIS

Moves a paired universal quantification inwards through an implication.

DESCRIPTION

When applied to a term of the form !p. t ==> u, where variables from p are not free in both t and u, PFORALL_IMP_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 none are in u, then the theorem:

   |- (!p. t ==> u) = (?p. t) ==> u

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

   |- (!p. t ==> u) = t ==> (!p. 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_IMP_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

FORALL_IMP_CONV, LEFT_IMP_PEXISTS_CONV, RIGHT_IMP_PFORALL_CONV