Consider a simple language of sets, motivated by verification of programs that manipulate containers:
Question: how do we justify ?
We show that this language is decidable by reduction to universal class.
Convert formula to negation-normal form.
Express all operations using quantifiers.
Note: the resulting formula has a bounded number of universal quantifiers