PEXISTS_CONV
PairRules.PEXISTS_CONV : conv
Eliminates paired existential quantifier by introducing a paired choice-term.
The conversion PEXISTS_CONV expects a boolean term of the form
(?p. t[p]), where p may be a paired structure or variables, and
converts it to the form (t [@p. t[p]]).
--------------------------------- PEXISTS_CONV "(?p. t[p])"
(|- (?p. t[p]) = (t [@p. t[p]])
Failure
Fails if applied to a term that is not a paired existential quantification.
See also
PairRules.PSELECT_RULE,
PairRules.PSELECT_CONV,
PairRules.PEXISTS_RULE,
PairRules.PSELECT_INTRO,
PairRules.PSELECT_ELIM