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