PSELECT_CONV : conv

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Eliminates a paired epsilon term by introducing an existential quantifier.
- DESCRIPTION
- The conversion PSELECT_CONV expects a boolean term of the form "t[@p.t[p]/p]", which asserts that the epsilon term @p.t[p] denotes a pair, p say, for which t[p] holds. This assertion is equivalent to saying that there exists such a pair, and PSELECT_CONV applied to a term of this form returns the theorem |- t[@p.t[p]/p] = ?p. t[p].
- FAILURE
- Fails if applied to a term that is not of the form "p[@p.t[p]/p]".
- SEEALSO

HOL Kananaskis-14