PEXISTS_AND_CONV : conv

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Moves a paired existential quantification inwards through a conjunction.
- DESCRIPTION
- When applied to a term of the form ?p. t /\ u, where variables in p are not free in both t and u, PEXISTS_AND_CONV returns a theorem of one of three forms, depending on occurrences of variables from p in t and u. If p contains variables free in t but none in u, then the theorem:is returned. If p contains variables free in u but none in t, then the result is:
|- (?p. t /\ u) = (?p. t) /\ u

And if p does not contain any variable free in either t nor u, then the result is:|- (?p. t /\ u) = t /\ (?x. u)

|- (?p. t /\ u) = (?x. t) /\ (?x. u)

- FAILURE
- PEXISTS_AND_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 in p are free in both t and u.
- SEEALSO

HOL Kananaskis-14