----------------------------------------------------------------------
PSKOLEM_CONV                                               (PairRules)
----------------------------------------------------------------------
PSKOLEM_CONV : conv

KEYWORDS
conversion.

LIBRARY
pair

SYNOPSIS
Proves the existence of a pair of Skolem functions.

DESCRIBE
When applied to an argument of the form {!p1...pn. ?q. tm}, the conversion
{PSKOLEM_CONV} returns the theorem:

   |- (!p1...pn. ?q. tm) = (?q'. !p1...pn. tm[q' p1 ... pn/yq)

where {q'} is a primed variant of the pair {q} not free in the
input term.

FAILURE
{PSKOLEM_CONV tm} fails if {tm} is not a term of the form {!p1...pn. ?q. tm}.

EXAMPLE
Both {q} and any {pi} may be a paired structure of variables:

   - PSKOLEM_CONV
      (Term `!(x11:'a,x12:'a) (x21:'a,x22:'a).
             ?(y1:'a,y2:'a). tm x11 x12 x21 x21 y1 y2`);

   > val it =
    |- (!(x11,x12) (x21,x22). ?(y1,y2). tm x11 x12 x21 x21 y1 y2) =
       ?(y1,y2).
         !(x11,x12) (x21,x22).
           tm x11 x12 x21 x21 (y1 (x11,x12) (x21,x22)) (y2 (x11,x12) (x21,x22))
     : thm




SEEALSO
Conv.SKOLEM_CONV, PairRules.P_PSKOLEM_CONV.

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