1\DOC SET_SPEC_CONV 2 3\TYPE {SET_SPEC_CONV : conv} 4 5\SYNOPSIS 6Axiom-scheme of specification for set abstractions. 7 8\LIBRARY pred_set 9 10\DESCRIBE 11The conversion {SET_SPEC_CONV} expects its term argument to be an assertion of 12the form {t IN {E | P}}. Given such a term, the conversion returns a 13theorem that defines the condition under which this membership assertion holds. 14When {E} is just a variable {v}, the conversion returns: 15{ 16 |- t IN {v | P} = P[t/v] 17} 18and when {E} is not a variable but some other expression, the theorem 19returned is: 20{ 21 |- t IN {E | P} = ?x1...xn. (t = E) /\ P 22} 23where {x1}, ..., {xn} are the variables that occur free both in 24the expression {E} and in the proposition {P}. 25 26\EXAMPLE 27{ 28- SET_SPEC_CONV ``12 IN {n | n > N}``; 29|- 12 IN {n | n > N} = 12 > N 30 31- SET_SPEC_CONV ``p IN {(n,m) | n < m}``; 32|- p IN {(n,m) | n < m} = (?n m. (p = n,m) /\ n < m) 33} 34 35\FAILURE 36Fails if applied to a term that is not of the form {t IN {E | P}}. 37 38\ENDDOC 39