res_quanLib.RES_EXISTS_UNIQUE

RES_EXISTS_UNIQUE_CONV : conv

STRUCTURE

SYNOPSIS

Converts a restricted unique existential quantification to a conjunction.

DESCRIPTION

When applied to a term of the form ?!x::P. Q[x], the conversion RES_EXISTS_UNIQUE_CONV returns the theorem:

   |- ?!x::P. Q[x] = (?x::P. Q[x]) /\ (!x y::P. Q[x] /\ Q[y] ==> (x = y))

which is the underlying semantic representation of the restricted unique existential quantification.

FAILURE

Fails if applied to a term not of the form ?x!::P. Q.

SEEALSO