resolution procedure. Conversely, the same formula but written using RIS is
(correctly) found to be unsatisfiable by $\mathit{SAT}_{\mathcal{RIS}}$.

A very general proposal providing real _intensional set constraints_ , where
intensional set processing is embedded within a general set constraint solver,
is CLP($\\{\mathcal{D}\\}$) [Dovier et al. (2003)]. CLP($\\{\mathcal{D}\\}$)
is a CLP language offering arbitrarily nested extensional and intensional sets
of elements over a generic constraint domain $\mathcal{D}$. No working
implementation of this proposal, however, has been developed. As observed in
[Dovier et al. (2003)], the presence of undecidable constraints such as
$\\{x:p(x)\\}=\\{x:q(x)\\}$ (where $p$ and $q$ can have an infinite number of
solutions) “prevents us from developing a parametric and complete solver”.
Conversely, this problem can be “approximated” using RIS as $\\{x:D_{1}\mid
p(x)\\}=\\{x:D_{2}\mid q(x)\\}$, $D_{1}$, $D_{2}$ variables. For
$\mathit{SAT}_{\mathcal{RIS}}$, this is a solved form formula admitting at
least one solution, namely $D_{1}=D_{2}=\emptyset$; hence, it is simply
returned unchanged by the solver. Generally speaking, finding a fragment of
intensional sets that is both decidable and expressive is a key issue for the
development of an effective tool for reasoning with intensional sets. RIS, as
presented here, may be one step toward this goal.

The usefulness of “a direct support for reasoning about set comprehension” in
the context of SMT solvers has been also recently advocated by Lam and
Cervesato [Lam and Cervesato (2014)]. In their approach, however, no ad-hoc
solver for intensional set constraints is indeed developed; rather, the
satisfiability problem for formulas featuring intensional sets over a standard
theory (e.g., linear integer arithmetic) is reduced to solving satisfiability
constraints over this same theory, extended with an uninterpreted sort for
sets and an uninterpreted binary predicate encoding set membership.

A number of works in the area of Computable Set Theory (CST) have studied the
satisfiability problem of different fragments of set theory with quantifiers.
Clearly, the availability of quantifiers plus set constraints opens the door
to intensional sets. Cantone and Zarba [Cantone and Zarba (2000)] introduce
the language 2LS($\mathcal{L}$) which is parametric w.r.t. a first-order
language $\mathcal{L}$. 2LS($\mathcal{L}$) extends $\mathcal{L}$ with set
constants, functional symbols, standard Boolean set operators, set membership
and equality. The authors show that, if the first-order theory underlying
$\mathcal{L}$, $\mathcal{T}$, is ground-decidable and the collection of ground
terms of $\mathcal{T}$ is finite, then the $\mathcal{T}$-satisfiability
problem for $\exists\forall$-sentences of 2LS($\mathcal{L}$), i.e., formulas
where all terms not involving any set-theoretic symbol are _ground_ , is
decidable.

In another work Cantone and Longo present the $\forall_{0,2}^{\pi}$ language
[Cantone and Longo (2014)]. $\forall_{0,2}^{\pi}$ is a two-sorted quantified
fragment of set theory which allows restricted quantifiers of the forms
$(\forall x\in A)$, $(\exists x\in A)$, $(\forall(x,y)\in R)$,
$(\exists(x,y)\in R)$ and literals of the forms $x\in A$, $(x,y)\in R$, $A=B$,
$R=S$, where $A$ and $B$ are set variables (i.e., variables ranging over sets)
and $R$ and $S$ are relation variables (i.e., variables ranging over binary
relations). $\forall_{0,2}^{\pi}$-formulas can be conjunctions of RUQ and
conjunctions of Restricted Existential Quantifiers (REQ), with some mild
restrictions. This language is expressive enough as to describe all the
Boolean set operators and disequalities of relational operators such as
composition, domain and relational image (e.g., $R\circ S\subseteq T$ but not
$T\subseteq R\circ S$). Although $\forall_{0,2}^{\pi}$ is not parametric
w.r.t. a first-order language, certain forms of intensional sets can be
described as well. Cantone and Longo show that $\forall_{0,2}^{\pi}$ is
decidable.

One important difference between our work and those on CST is that the later
is mainly concerned with decidability results for fragments of set theory,
while the rewriting systems used in our works are also able to generate a
finite representation of all the (possibly infinitely many) solutions of each
input formula.

Several logics (e.g., [Dragoi et al. (2014), Veanes and Saabas (2008), Wies et
al. (2009)]) provide some forms of intensional sets. However, in some cases,
for the formula to be inside the decision procedure, the intensional sets must
have a ground domain; in others, set operators do not include set equality;
and in others, they present a semi-decision procedure. Handling intensional
sets can be related also to handling universal quantifiers in a logical
setting, since intensional sets “hide” a universal quantifier. Tools such as
SMT solvers deal with this kind of problems (see, e.g., [Deharbe et al.
(2011)] and [Bjørner et al. (2013)]), although in general they are complete
only in quite restricted cases [Ge and de Moura (2009)]. Recently, a language
admitting some forms of quantified formulas over sets was proven to be
decidable in the context of separation logic [Gao et al. (2019)].

Our decision procedure finds models for formulas with _finite_ but _unbounded_
domains, i.e., their cardinalities are not constrained by a fixed value. The
field of finite model finding faces a similar problem but usually with
_bounded_ domains. There are two basic styles of model finding: the MACE-style
in which the formula is transformed into a SAT problem [Claessen and Sörensson
(2003)]; and the SEM-style which uses constraint solving techniques [Zhang and
Zhang (1996)]. Our approach is closer to the SEM-style as it is based on
constraint programming. However, since both styles do not deal with quantified
domains as sets, then they cannot reduce the domain every time an element is
identified, as we do with RIS—for instance, in rule (5). Instead, they set a
size for the domain and try to find a model at most as large as that.

Ideas from finite model finding were taken as inspiration by Reynolds et al.
[Reynolds et al. (2013)] for handling universal quantifiers in SMT. These
authors propose to find finite models for infinite universally quantified
formulas by considering finite domains. In particular, Reynolds et al. make
use of the cardinality operator for the sorts of quantified variables and
propose a solver for a theory based on this operator. Then, they make a guess
of the cardinality for a quantified sort and use the solver to try to find a
model there. In the default strategy, the initial guess is 1 and it is
incremented in 1. Note that our approach does not need a cardinality operator
because it operates directly over a theory of sets.

##  10 Concluding Remarks

In this paper we have shown a decision procedure for an expressive class of
intensional sets, called Restricted Intensional Sets (RIS). Key features of
this procedure are: it returns a finite representation of all possible
solutions of the input formula; it allows set elements to be variables; it is
parametric with respect to any first-order theory endowed with a decision
procedure; and it is implemented as part of the $\\{log\\}$ tool. Besides, we
have shown through a number of examples and two case studies that, although
RIS are a subclass of general intensional sets, they are still sufficiently
expressive as to encode and solve many interesting problems. Finally, an
extensive empirical evaluation provides evidence that the tool can be used in
practice.

We foresee some promising lines of work concerning RIS:

  * •

Some set-theoretic operators (e.g., intersection), which are provided in
$\mathcal{L}_{\mathcal{RIS}}$ as derived constraints, are first rewritten into
a $\mathcal{L}_{\mathcal{RIS}}$ formula and then
$\mathit{SAT}_{\mathcal{RIS}}$ is applied to the resulting formula. This
threatens the efficiency of $\mathit{SAT}_{\mathcal{RIS}}$. Hence, a future
work is to implement specific rewriting procedures for some widely used
constraints such as intersection.

  * •

The relational operators available in $\mathcal{BR}$ could be extended to
allow for RIS as arguments.

  * •

As it is now, $\mathcal{L}_{\mathcal{RIS}}$ admits only RUQ of the form
$\forall x\in A(\phi(x))$, that is, a single bound variable and its domain.
Extending $\mathcal{L}_{\mathcal{RIS}}$ to allow multiple bound variables,
each with its own domain, would require to admit certain
$\mathcal{RIS}$-formulas as RIS filters. For example, $\forall x\in A(\forall
y\in B(\phi(x,y)))$ can be encoded as:

$A\subseteq\\{x:A\mid B\subseteq\\{y:B\mid\phi(x,y)\\}\\}$

but this is not a $\mathcal{RIS}$-formula because the filter of the outermost
RIS is a $\mathcal{RIS}$-formula. Our intuition is that this would not only be
decidable but relatively efficient too, which, in the end, would be aligned
with some results of CST.

An alternative way of encoding RUQ with multiple variables is by allowing the
recently added Cartesian products [Cristiá and Rossi (2018)] as RIS domains.
We plan to assess both approaches.

## References

  * [1]
  * Abrial (1996) J.-R. Abrial. 1996.  The B-book: Assigning Programs to Meanings.  Cambridge University Press, New York, NY, USA.
  * Beeri et al. (1991) Catriel Beeri, Shamim A. Naqvi, Oded Shmueli, and Shalom Tsur. 1991.  Set Constructors in a Logic Database Language.  J. Log. Program. 10, 3&4 (1991), 181–232.
  * Bell and LaPadula (1973a) D. Elliot Bell and Leonard LaPadula. 1973a.  Secure computer systems: Mathematical foundations.  MTR 2547. The MITRE Corporation.
  * Bell and LaPadula (1973b) D. Elliot Bell and Leonard LaPadula. 1973b.  Secure computer systems: Mathematical model.  ESD-TR 73-278. The MITRE Corporation.
  * Bjørner et al. (2013) Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko. 2013.  On Solving Universally Quantified Horn Clauses. In Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings (Lecture Notes in Computer Science), Francesco Logozzo and Manuel Fähndrich (Eds.), Vol. 7935\. Springer, 105–125.  DOI:http://dx.doi.org/10.1007/978-3-642-38856-9_8
  * Bruscoli et al. (1994) Paola Bruscoli, Agostino Dovier, Enrico Pontelli, and Gianfranco Rossi. 1994.  Compiling Intensional Sets in CLP. In Logic Programming, Proceedings of the Eleventh International Conference on Logic Programming, Santa Marherita Ligure, Italy, June 13-18, 1994, Pascal Van Hentenryck (Ed.). MIT Press, 647–661.
  * Cantone and Longo (2014) Domenico Cantone and Cristiano Longo. 2014.  A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions.  Theor. Comput. Sci. 560 (2014), 307–325.  DOI:http://dx.doi.org/10.1016/j.tcs.2014.03.021
  * Cantone and Zarba (2000) Domenico Cantone and Calogero G. Zarba. 2000.  A Tableau Calculus for Integrating First-Order and Elementary Set Theory Reasoning. In Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings (Lecture Notes in Computer Science), Roy Dyckhoff (Ed.), Vol. 1847. Springer, 143–159.  DOI:http://dx.doi.org/10.1007/10722086\\_14
  * Claessen and Sörensson (2003) K. Claessen and N. Sörensson. 2003.  New techniques that improve MACE-style finite model building. In CADE-19 Workshop: Model Computation – Principles, Algorithms, Applications. 11–27.
  * Cristiá and Rossi (2017) Maximiliano Cristiá and Gianfranco Rossi. 2017.  A Decision Procedure for Restricted Intensional Sets. In Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings (Lecture Notes in Computer Science), Leonardo de Moura (Ed.), Vol. 10395. Springer, 185–201.  DOI:http://dx.doi.org/10.1007/978-3-319-63046-5\\_12
  * Cristiá and Rossi (2018) Maximiliano Cristiá and Gianfranco Rossi. 2018.  A Set Solver for Finite Set Relation Algebra. In Relational and Algebraic Methods in Computer Science - 17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29 \- November 1, 2018, Proceedings (Lecture Notes in Computer Science), Jules Desharnais, Walter Guttmann, and Stef Joosten (Eds.), Vol. 11194\. Springer, 333–349.  DOI:http://dx.doi.org/10.1007/978-3-030-02149-8\\_20
  * Cristiá and Rossi (2019) Maximiliano Cristiá and Gianfranco Rossi. 2019.  Rewrite Rules for a Solver for Sets, Binary Relations and Partial Functions.  (2019).  http://people.dmi.unipr.it/gianfranco.rossi/SETLOG/calculus.pdf
  * Cristiá and Rossi (2019) Maximiliano Cristiá and Gianfranco Rossi. 2019.  Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations.  Journal of Automated Reasoning (08 Apr 2019).  DOI:http://dx.doi.org/10.1007/s10817-019-09520-4
  * Cristiá et al. (2015) Maximiliano Cristiá, Gianfranco Rossi, and Claudia S. Frydman. 2015\.  Adding partial functions to Constraint Logic Programming with sets.  TPLP 15, 4-5 (2015), 651–665.  DOI:http://dx.doi.org/10.1017/S1471068415000290
  * Dal Palú et al. (2003) A. Dal Palú, A. Dovier, E. Pontelli, and G. Rossi. 2003.  Integrating Finite Domain Constraints and CLP with Sets. In Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming (PPDP ’03). ACM, New York, NY, USA, 219–229.  DOI:http://dx.doi.org/10.1145/888251.888272
  * Deharbe et al. (2011) David Deharbe, Pascal Fontaine, and Bruno Woltzenlogel Paleo. 2011.  Quantifier Inference Rules for SMT proofs. In Workshop on Proof eXchange for Theorem Proving.
  * Dovier et al. (1996) Agostino Dovier, Eugenio G. Omodeo, Enrico Pontelli, and Gianfranco Rossi. 1996.  A Language for Programming in Logic with Finite Sets.  J. Log. Program. 28, 1 (1996), 1–44.  DOI:http://dx.doi.org/10.1016/0743-1066(95)00147-6
  * Dovier et al. (2000) Agostino Dovier, Carla Piazza, Enrico Pontelli, and Gianfranco Rossi. 2000\.  Sets and constraint logic programming.  ACM Trans. Program. Lang. Syst. 22, 5 (2000), 861–931.
  * Dovier et al. (2001) Agostino Dovier, Enrico Pontelli, and Gianfranco Rossi. 2001.  Constructive Negation and Constraint Logic Programming with Sets.  New Generation Comput. 19, 3 (2001), 209–256.  DOI:http://dx.doi.org/10.1007/BF03037598
  * Dovier et al. (2003) Agostino Dovier, Enrico Pontelli, and Gianfranco Rossi. 2003.  Intensional Sets in CLP. In Logic Programming, 19th International Conference, ICLP 2003, Mumbai, India, December 9-13, 2003, Proceedings (Lecture Notes in Computer Science), Catuscia Palamidessi (Ed.), Vol. 2916. Springer, 284–299.  DOI:http://dx.doi.org/10.1007/978-3-540-24599-5_20
  * Dovier et al. (2006) Agostino Dovier, Enrico Pontelli, and Gianfranco Rossi. 2006.  Set Unification.  Theory Pract. Log. Program. 6, 6 (Nov. 2006), 645–701.  DOI:http://dx.doi.org/10.1017/S1471068406002730
  * Dragoi et al. (2014) Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. 2014.  A Logic-Based Framework for Verifying Consensus Algorithms. In Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings (Lecture Notes in Computer Science), Kenneth L. McMillan and Xavier Rival (Eds.), Vol. 8318. Springer, 161–181.  DOI:http://dx.doi.org/10.1007/978-3-642-54013-4_10
  * Gao et al. (2019) Chong Gao, Taolue Chen, and Zhilin Wu. 2019.  Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints. In SOFSEM 2019: Theory and Practice of Computer Science - 45th International Conference on Current Trends in Theory and Practice of Computer Science, Nový Smokovec, Slovakia, January 27-30, 2019, Proceedings (Lecture Notes in Computer Science), Barbara Catania, Rastislav Královic, Jerzy R. Nawrocki, and Giovanni Pighizzini (Eds.), Vol. 11376. Springer, 206–220.  DOI:http://dx.doi.org/10.1007/978-3-030-10801-4\\_17
  * Ge and de Moura (2009) Yeting Ge and Leonardo Mendonça de Moura. 2009.  Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009\. Proceedings (Lecture Notes in Computer Science), Ahmed Bouajjani and Oded Maler (Eds.), Vol. 5643. Springer, 306–320.  DOI:http://dx.doi.org/10.1007/978-3-642-02658-4_25
  * Hill and Lloyd (1994) Patricia M. Hill and John W. Lloyd. 1994.  The Gödel programming language.  MIT Press. I–XX, 1–348 pages.
  * Jackson (2006) Daniel Jackson. 2006.  Software Abstractions: Logic, Language, and Analysis.  The MIT Press.
  * Lam and Cervesato (2014) Edmund S. L. Lam and Iliano Cervesato. 2014.  Reasoning About Set Comprehensions. In Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, SMT 2014, affiliated with the 26th International Conference on Computer Aided Verification (CAV 2014), the 7th International Joint Conference on Automated Reasoning (IJCAR 2014), and the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), Vienna, Austria, July 17-18, 2014. (CEUR Workshop Proceedings), Philipp Rümmer and Christoph M. Wintersteiger (Eds.), Vol. 1163. CEUR-WS.org, 27–37.  http://ceur-ws.org/Vol-1163/paper-05.pdf
  * Leuschel and Butler (2003) Michael Leuschel and Michael Butler. 2003.  ProB: A Model Checker for B. In FME (Lecture Notes in Computer Science), Araki Keijiro, Stefania Gnesi, and Dino Mandrioli (Eds.), Vol. 2805. Springer-Verlag, 855–874.
  * Nethercote et al. (2007) Nicholas Nethercote, Peter J. Stuckey, Ralph Becket, Sebastian Brand, Gregory J. Duck, and Guido Tack. 2007.  MiniZinc: Towards a Standard CP Modelling Language. In Principles and Practice of Constraint Programming - CP 2007, 13th International Conference, CP 2007, Providence, RI, USA, September 23-27, 2007, Proceedings (Lecture Notes in Computer Science), Christian Bessiere (Ed.), Vol. 4741. Springer, 529–543.  DOI:http://dx.doi.org/10.1007/978-3-540-74970-7_38
  * Reynolds et al. (2013) Andrew Reynolds, Cesare Tinelli, Amit Goel, and Sava Krstic. 2013.  Finite Model Finding in SMT. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044\. Springer, 640–655.  DOI:http://dx.doi.org/10.1007/978-3-642-39799-8_42
  * Rossi (2008) Gianfranco Rossi. 2008.  $\\{log\\}$.  (2008).  http://people.dmi.unipr.it/gianfranco.rossi/setlog.Home.html
  * Schneider (2001) S. Schneider. 2001.  The B-method: An Introduction.  Palgrave.  http://books.google.com.ar/books?id=Krs0OQAACAAJ
  * Schwartz et al. (1986) Jacob T. Schwartz, Robert B. K. Dewar, Ed Dubinsky, and Edith Schonberg. 1986.  Programming with Sets - An Introduction to SETL.  Springer.  DOI:http://dx.doi.org/10.1007/978-1-4613-9575-1
  * Spivey (1992) J. M. Spivey. 1992.  The Z notation: a reference manual.  Prentice Hall International (UK) Ltd., Hertfordshire, UK, UK.
  * Sutcliffe (2009) G. Sutcliffe. 2009.  The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0.  Journal of Automated Reasoning 43, 4 (2009), 337–362.
  * Veanes and Saabas (2008) Margus Veanes and Ando Saabas. 2008.  On Bounded Reachability of Programs with Set Comprehensions. In Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings (Lecture Notes in Computer Science), Iliano Cervesato, Helmut Veith, and Andrei Voronkov (Eds.), Vol. 5330. Springer, 305–317.  DOI:http://dx.doi.org/10.1007/978-3-540-89439-1_22
  * Wies et al. (2009) Thomas Wies, Ruzica Piskac, and Viktor Kuncak. 2009.  Combining Theories with Shared Set Operations. In Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009. Proceedings (Lecture Notes in Computer Science), Silvio Ghilardi and Roberto Sebastiani (Eds.), Vol. 5749. Springer, 366–382.  DOI:http://dx.doi.org/10.1007/978-3-642-04222-5_23
  * Woodcock and Davies (1996) Jim Woodcock and Jim Davies. 1996.  Using Z: specification, refinement, and proof.  Prentice-Hall, Inc., Upper Saddle River, NJ, USA.
  * Zhang and Zhang (1996) Jian Zhang and Hantao Zhang. 1996.  System Description: Generating Models by SEM. In Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings (Lecture Notes in Computer Science), Michael A. McRobbie and John K. Slaney (Eds.), Vol. 1104. Springer, 308–312.  DOI:http://dx.doi.org/10.1007/3-540-61511-3_96

##  Appendix A Rewrite rules

This section lists all the $\mathcal{L}_{\mathcal{RIS}}$ rewrite rules for
$=$, $\neq$, $\in$ and $\notin$ constraints not given in Section 3.2, along
with the rules for $\mathit{set}$ and $\mathit{isX}$ constraints; rules for
$\mathit{un}$ and $\mathit{disj}$ constraints are instead all shown in Section
3.2 and are not repeated here. Many of the rules listed in this appendix are
borrowed directly from [Dovier et al. (2000)].

We adopt the following notational conventions: $s,t,u$ (possibly subscripted)
stand for arbitrary $\mathcal{X}$-terms; $A,B,C,D$ stand for arbitrary
$\mathcal{RIS}$-terms of sort $\mathsf{Set}$ (either extensional or
intensional, variable or not); $\bar{D},\bar{E}$ represent either variables of
sort $\mathsf{Set}$ or variable-RIS; $X,N$ are variables of sort
$\mathsf{Set}$ representing extensional sets (not RIS) while $x$ is a variable
of sort $\mathsf{X}$; $\varnothing$ represents either $\emptyset$ or a RIS
with empty domain (e.g., $\\{\emptyset\mid\phi\mathbin{\bullet}u\\}$);
finally, X represents either the variable $X$ or a set term containing $X$ as
its innermost variable set part, i.e., $\\{t_{1},\dots,t_{n}\sqcup X\\}$. Note
that, when $n=0$, $\\{t_{1},\dots,t_{n}\sqcup X\\}$ is just $X$.

In all rules, variables appearing in the right-hand side but not in the left-
hand side are assumed to be fresh variables.

Besides, recall that: a) the rules are given for RIS whose domain is not
another RIS (see Appendix A.1 for further details); b) the control term of RIS
terms is assumed to be a _variable_ in all cases (see Appendix A.2 for further
details); c) $\phi(d)$, $\gamma(d)$, $u(d)$ and $v(d)$ are shorthands for
$\phi[x\mapsto d]$, $\gamma[x\mapsto d]$, $u[x\mapsto d]$ and $v[x\mapsto d]$,
respectively, where $[x\mapsto d]$ represents variable substitution; and d) we
use $=$ and $\in$ in place of $=_{\mathcal{X}}$ and $\in_{\mathcal{X}}$
whenever it is clear from the context.

### Equality

$\displaystyle\varnothing=\varnothing\longrightarrow\mathit{true}$ ($=_{1}$)
$\displaystyle X=X\longrightarrow\mathit{true}$ ($=_{2}$) If $S\equiv X$ or
$S\equiv\\{c:\textbf{{X}}\mid\phi\mathbin{\bullet}u\\}$ with $c\equiv u$:
$\displaystyle
X=\\{t_{0},\dots,t_{k}\mathbin{\scriptstyle\sqcup}S\\}\longrightarrow
X=\\{t_{0},\dots,t_{k}\mathbin{\scriptstyle\sqcup}S[X\mapsto N]\\}$ ($=_{3}$)
If $X$ occurs in other constraints in the input formula and
$A\not\equiv\\{\\{d\sqcup D\\}\mid\phi\mathbin{\bullet}u\\}$: $\displaystyle
X=A\longrightarrow X=A\text{ and substitute $X$ by $A$ in the rest of the
formula}$ ($=_{4}$)
$\displaystyle\varnothing=\\{t\mathbin{\scriptstyle\sqcup}A\\}\longrightarrow\mathit{false}$
($=_{5}$) If ($R\equiv X$ and $S\equiv X$) or
($R\equiv\\{c:\textbf{{X}}\mid\phi\mathbin{\bullet}u\\}$ and $S\equiv X$) or
($R\equiv\\{c:\textbf{{X}}\mid\phi\mathbin{\bullet}u\\}$ and
$S\equiv\\{d:X\mid\gamma\mathbin{\bullet}v\\}$) with $c\equiv u$ and $d\equiv
v$:
$\displaystyle\begin{split}\\{t_{0},&\dots,t_{m}\mathbin{\scriptstyle\sqcup}R\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S\\}\longrightarrow\\\
&t_{0}=s_{j}\\\
&\quad{}\land\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{1}\\}=R\land t_{0}\notin
N_{1}\land\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{2}\\}=S\land t_{0}\notin
N_{2}\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N_{1}\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N_{2}\\}\\\
&{}\lor t_{0}=s_{j}\\\ &\quad{}\land t_{0}\notin R\land t_{0}\notin S\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}R\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S\\}\\\
&{}\lor t_{0}=s_{j}\\\
&\quad{}\land\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}=R\land t_{0}\notin
N\land t_{0}\notin S\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S\\}\\\
&{}\lor t_{0}=s_{j}\\\ &\quad{}\land t_{0}\notin
R\land\\{s_{j}\mathbin{\scriptstyle\sqcup}N\\}=S\land s_{j}\notin N\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}R\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N\\}\\\
&{}\lor
t_{0}=s_{j}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}R\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S\\}\\\
&{}\lor
t_{0}=s_{j}\land\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}R\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S\\}\\\
&{}\lor X=\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}\\\
&{}\quad{}\land\text{{if} $S\equiv X$ {then} $\mathit{true}$ {else}
$\gamma(t_{0})$}\\\
&{}\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}R[X\mapsto
N]\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S[X\mapsto
N]\\}\end{split}$ ($=_{6}$) If $R\equiv X$ and
$S\equiv\\{d:X\mid\gamma\mathbin{\bullet}v\\}$ with $d\equiv v$:
$\displaystyle\begin{split}\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}R\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S\\}\longrightarrow\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S\\}=\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}R\\}\end{split}$
($=_{7}$)

$\displaystyle\text{If $R\equiv\\{c:\textbf{{X}}\mid\phi\mathbin{\bullet}u\\}$
and $S\equiv\\{d:X\mid\gamma\mathbin{\bullet}v\\}$ with $c\not\equiv u$ and
$d\not\equiv v$}:$
$\displaystyle\begin{split}\\{t_{0},&\dots,t_{m}\mathbin{\scriptstyle\sqcup}R\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S\\}\longrightarrow\\\
&t_{0}=s_{j}\\\
&\quad{}\land\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{1}\\}=R\land t_{0}\notin
N_{1}\land\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{2}\\}=S\land t_{0}\notin
N_{2}\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N_{1}\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N_{2}\\}\\\
&{}\lor t_{0}=s_{j}\\\ &\quad{}\land t_{0}\notin R\land t_{0}\notin S\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}R\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S\\}\\\
&{}\lor t_{0}=s_{j}\\\
&\quad{}\land\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}=R\land t_{0}\notin
N\land t_{0}\notin S\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S\\}\\\
&{}\lor t_{0}=s_{j}\\\ &\quad{}\land t_{0}\notin
R\land\\{s_{j}\mathbin{\scriptstyle\sqcup}N\\}=S\land s_{j}\notin N\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}R\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N\\}\\\
&{}\lor
t_{0}=s_{j}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}R\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S\\}\\\
&{}\lor
t_{0}=s_{j}\land\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}R\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S\\}\\\
&{}\lor X=\\{n\mathbin{\scriptstyle\sqcup}N\\}\land\gamma(n)\land
t_{0}=v(n)\\\ &\quad{}\land(\neg\phi(n)\lor(\phi(n)\land
u(n)\notin\\{s_{0},\dots,s_{k}\\}\land t_{0}=u(n)))\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}R[X\mapsto
N]\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S[X\mapsto N]\\}\\}\\\
&{}\lor X=\\{n\mathbin{\scriptstyle\sqcup}N\\}\land\gamma(n)\land
t_{0}=v(n)\land\phi(n)\land u(n)=s_{j}\\\
&\quad{}\land\\{u(n),t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}R[X\mapsto
N]\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}S[X\mapsto N]\\}\\}\\\
\end{split}$ ($=_{8}$)
$\displaystyle\begin{split}\\{t\mathbin{\scriptstyle\sqcup}&A\\}=\\{s\mathbin{\scriptstyle\sqcup}B\\}\longrightarrow\\\
&(t=s\land
A=\\{s\mathbin{\scriptstyle\sqcup}B\\})\lor(t=s\land\\{s\mathbin{\scriptstyle\sqcup}A\\}=B)\\\
&\lor(t=s\land
A=B)\lor(A=\\{s\mathbin{\scriptstyle\sqcup}N\\}\land\\{t\mathbin{\scriptstyle\sqcup}N\\}=B)\end{split}$
($=_{9}$) (rule (5) of Fig. 1)
$\displaystyle\\{\\{t\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}=\varnothing\longrightarrow\lnot\phi(t)\land\\{D\mid\phi\mathbin{\bullet}u\\}=\emptyset$
($=_{10}$) (rule (6) of Fig. 1)
$\displaystyle\begin{split}&\\{\\{t\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}=B\longrightarrow\\\
&(\phi(t)\land\\{u(t)\mathbin{\scriptstyle\sqcup}\\{D\mid\phi\mathbin{\bullet}u\\}\\}=B)\lor(\lnot\phi(t)\land\\{D\mid\phi\mathbin{\bullet}u\\}=B)\end{split}$
($=_{11}$) If $S\equiv X$ or
$S\equiv\\{c:\textbf{{X}}\mid\phi\mathbin{\bullet}u\\}$ with $c\equiv u$ and
$d\equiv v$:
$\displaystyle\begin{split}\\{d:&X\mid\gamma\mathbin{\bullet}v\\}=\\{t_{0},t_{1},\dots,t_{k}\mathbin{\scriptstyle\sqcup}S\\}\longrightarrow\\\
&X=\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}\land\gamma(t_{0})\land\\{d:N\mid\gamma\mathbin{\bullet}v\\}=\\{t_{1},\dots,t_{k}\mathbin{\scriptstyle\sqcup}S[X\mapsto
N]\\}\end{split}$ ($=_{12}$) If
$S\equiv\\{c:\textbf{{X}}\mid\phi\mathbin{\bullet}u\\}$ with $c\not\equiv u$
and $d\not\equiv v$:
$\displaystyle\begin{split}\\{d:&X\mid\gamma\mathbin{\bullet}v\\}=\\{t_{0},t_{1},\dots,t_{k}\mathbin{\scriptstyle\sqcup}S\\}\longrightarrow\\\
&X=\\{n\mathbin{\scriptstyle\sqcup}N\\}\land\gamma(n)\land
t_{0}=v(n)\land(\neg\phi(n)\lor t_{0}=u(n))\\\
&\land\\{d:N\mid\gamma\mathbin{\bullet}v\\}=\\{t_{1},\dots,t_{k}\mathbin{\scriptstyle\sqcup}S[X\mapsto
N]\\}\end{split}$ ($=_{13}$) (rule (7) of Fig. 1)
$\displaystyle\begin{split}&\\{\bar{D}\mid\phi\mathbin{\bullet}u\\}=\\{t\mathbin{\scriptstyle\sqcup}A\\}\longrightarrow\\\
&\bar{D}=\\{n\mathbin{\scriptstyle\sqcup}N\\}\land\phi(n)\land
t=u(n)\land\\{N\mid\phi\mathbin{\bullet}u\\}=A\end{split}$ ($=_{14}$)

There is a symmetric rule for each of the following: $\eqref{special2}$,
$\eqref{x=s}$, $\eqref{e=s}$, ($=_{10}$), ($=_{11}$), ($=_{12}$), ($=_{13}$)
and $\eqref{app.e:v=e}$. That is, these rules apply when the l.h.s. and the
r.h.s. are switched.

All other admissible $=$-constraints are in solved form; hence, they are dealt
with as irreducible constraints (see Section 4.2).

######  Remark A.1.

  * •

Rules ($=_{1}$) and ($=_{5}$) include rules (3) and (4) of Figure 1 as special
cases.

  * •

The condition $A\not\equiv\\{\\{d\sqcup D\\}\mid\phi\mathbin{\bullet}u\\}$ in
rule ($=_{4}$) is motivated by the fact that the case where
$A\equiv\\{\\{d\sqcup D\\}\mid\phi\mathbin{\bullet}u\\}$ is dealt with by rule
($=_{11}$).

  * •

The set part of an extensional set can be also a RIS term. All rules listed in
this section still continue to work also in these cases. In particular, rule
($=_{3}$) deals also with constraints of the form
$X=\\{t_{0},\dots,t_{n}\mathbin{\scriptstyle\sqcup}\\{X\mid\phi\mathbin{\bullet}u\\}\\}$
where the domain of the RIS is the same variable occurring in the left-hand
side of the equality. This constraint is rewritten to
$X=\\{t_{0},\dots,t_{n}\mathbin{\scriptstyle\sqcup}\\{N\mid\phi\mathbin{\bullet}u\\}\\}$
where $N$ is a fresh variable. For example, the equality
$X=\\{a,b\mathbin{\scriptstyle\sqcup}\\{x:X\mid\mathit{true}\mathbin{\bullet}x\\}\\}$
is rewritten to
$X=\\{a,b\mathbin{\scriptstyle\sqcup}\\{x:N\mid\mathit{true}\mathbin{\bullet}x\\}\\}$.
Note that, if $N=\emptyset$, then $X=\\{a,b\\}$, which is clearly a solution
of the given constraint.

  * •

Rules ($=_{12}$) and ($=_{13}$) (resp., ($=_{6}$), ($=_{7}$) and ($=_{8}$))
are motivated by the observation that rule ($=_{14}$) (resp., ($=_{9}$)) does
not work satisfactory (it loops forever) whenever the same variable $X$ occurs
in both sides of the equation. As an example, the rewriting of the simple
constraint $\\{x:D\mathbin{\bullet}x\\}=\\{1\mathbin{\scriptstyle\sqcup}D\\}$
does not terminate using rule ($=_{14}$), though it has the obvious solution
$D=\\{1\mathbin{\scriptstyle\sqcup}N\\}$, $N$ a fresh variable. Thus, rules
($=_{12}$) and ($=_{13}$) (resp., ($=_{6}$), ($=_{7}$) and ($=_{8}$)) are
introduced to deal with these special cases. Note that these rules are, in a
sense, the analogous of rule ($=_{3}$) which deals with equations of the form
$X=\\{t_{0},\dots,t_{n}\mathbin{\scriptstyle\sqcup}\textbf{{X}}\\}$ where the
same variable $X$ occurs in both sides of the equation. In turn, rule
($=_{3}$) is a generalization to RIS of rule (6) listed in Figure 3 of [Dovier
et al. (2000)]. ∎

### Inequality

$\displaystyle\varnothing\neq\varnothing\longrightarrow\mathit{false}$
($\neq_{1}$) $\displaystyle X\neq X\longrightarrow\mathit{false}$ ($\neq_{2}$)
If $A$ is neither a variable nor a RIS: $\displaystyle A\neq X\longrightarrow
X\neq A$ ($\neq_{3}$)
$\displaystyle\varnothing\neq\\{t\mathbin{\scriptstyle\sqcup}A\\}\longrightarrow\mathit{true}$
($\neq_{4}$) If $S\equiv X$ or $S\equiv\\{D\mid\phi\mathbin{\bullet}u\\}$:
$\displaystyle\begin{split}X\neq&\\{t_{0},\dots,t_{n}\mathbin{\scriptstyle\sqcup}S\\}\longrightarrow\\\
&(n\in X\land
n\notin\\{t_{0},\dots,t_{n}\mathbin{\scriptstyle\sqcup}S\\})\lor(n\notin
X\land n\in\\{t_{0},\dots,t_{n}\mathbin{\scriptstyle\sqcup}S\\})\end{split}$
($\neq_{5}$)
$\displaystyle\begin{split}\\{t\mathbin{\scriptstyle\sqcup}&A\\}\neq\\{s\mathbin{\scriptstyle\sqcup}B\\}\longrightarrow\\\
&(n\in\\{t\mathbin{\scriptstyle\sqcup}A\\}\land
n\notin\\{s\mathbin{\scriptstyle\sqcup}B\\})\lor(n\notin\\{t\mathbin{\scriptstyle\sqcup}A\\}\land
n\in\\{s\mathbin{\scriptstyle\sqcup}B\\})\end{split}$ ($\neq_{6}$) (rule (8)
of Fig. 1) $\displaystyle\begin{split}\\{D\mid&\phi\mathbin{\bullet}u\\}\neq
A\longrightarrow\\\ &(n\in\\{D\mid\phi\mathbin{\bullet}u\\}\land n\notin
A)\lor(n\notin\\{D\mid\phi\mathbin{\bullet}u\\}\land n\in A)\end{split}$
($\neq_{7}$)

There is a symmetric rule for each of the following: $\eqref{e_neq_s}$ and
$\eqref{app.e:neq}$. That is, these rules apply when the l.h.s. and the r.h.s.
are switched.

All other admissible $\neq$-constraints are in solved form (see Section 4.2).

######  Remark A.2.

The fact that $X\neq\\{D\mid\phi\mathbin{\bullet}u\\}$ (rule ($\neq_{7}$)) and
$X\neq\\{t_{0},\dots,t_{n}\mathbin{\scriptstyle\sqcup}\\{D\mid\phi\mathbin{\bullet}u\\}\\}$
(rule ($\neq_{5}$)) are not considered in solved form as it is $X\neq S$ when
$S$ is not a RIS term is motivated by the observation that, while determining
the satisfiability of $X\neq S$ is immediate, the satisfiability of of the
inequalities involving RIS depends on $D$, $\phi$ and $u$, and hence requires
further simplification of the constraint. ∎

### Set membership

$\displaystyle t\in\varnothing\longrightarrow\mathit{false}$ ($\in_{1}$)
$\displaystyle t\in\\{s\mathbin{\scriptstyle\sqcup}A\\}\longrightarrow t=s\lor
t\in A$ ($\in_{2}$) $\displaystyle t\in X\longrightarrow
X=\\{t\mathbin{\scriptstyle\sqcup}N\\}$ ($\in_{3}$) (rule (10) of Fig. 2)
$\displaystyle t\in\\{D\mid\phi\mathbin{\bullet}u\\}\longrightarrow n\in
D\land\phi(n)\land t=u(n)$ ($\in_{4}$)

No other admissible $\in$-constraint.

### Not set membership

$\displaystyle t\notin\varnothing\longrightarrow\mathit{true}$ ($\notin_{1}$)
$\displaystyle t\notin\\{s\mathbin{\scriptstyle\sqcup}A\\}\longrightarrow
t\neq s\land t\notin A$ ($\notin_{2}$) (rule (12) of Fig. 2)
$\displaystyle\begin{split}&t\notin\\{\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}\longrightarrow\\\
&(\phi(d)\land t\neq u(d)\land
t\notin\\{D\mid\phi\mathbin{\bullet}u\\})\lor(\lnot\phi(d)\land
t\notin\\{D\mid\phi\mathbin{\bullet}u\\})\end{split}$ ($\notin_{3}$)

All other admissible $\notin$-constraints are in solved form (see Section
4.2).

######  Remark A.3 (Membership/not membership).

Rules ($\in_{1}$) and ($\notin_{1}$) include rules (9) and (11) of Figure 2 as
special cases. ∎

### Sort constraints

$\displaystyle\mathit{set}(\emptyset)\longrightarrow\mathit{true}$
($\mathit{set}_{1}$)
$\displaystyle\mathit{set}(\\{t\mathbin{\scriptstyle\sqcup}A\\})\longrightarrow\mathit{set}(A)$
($\mathit{set}_{2}$)
$\displaystyle\mathit{set}(\\{D\mid\phi\mathbin{\bullet}u\\})\longrightarrow\mathit{true}$
($\mathit{set}_{3}$)
$\displaystyle\mathit{set}(t)\longrightarrow\mathit{false}$
($\mathit{set}_{4}$)

$\displaystyle\mathit{isX}(\emptyset)\longrightarrow\mathit{false}$
($\mathit{isX}_{1}$)
$\displaystyle\mathit{isX}(t\mathbin{\scriptstyle\sqcup}A\\}\longrightarrow\mathit{false}$
($\mathit{isX}_{2}$)
$\displaystyle\mathit{isX}(\\{D\mid\phi\mathbin{\bullet}u\\})\longrightarrow\mathit{false}$
($\mathit{isX}_{3}$)
$\displaystyle\mathit{isX}(t)\longrightarrow\mathit{true}$
($\mathit{isX}_{4}$)

######  Remark A.4.

In Algorithm 1 (see Section 3), $\mathit{SAT}_{\mathcal{RIS}}$ calls
$\mathit{SAT}_{\mathcal{X}}$ only once, at the end of the computation.
$\mathit{SAT}_{\mathcal{X}}$ is called by passing it the whole collection of
$\mathcal{X}$ literals previously accumulated in the current formula $\Phi$ by
the repeated applications of the rewrite rules within STEP. Alternatively, and
more efficiently, $\mathit{SAT}_{\mathcal{X}}$ could be called repeatedly in
the inner loop of the solver, just after the STEP procedure has been called.
This would allow possible inconsistencies to be detected as soon as possible
instead of being deferred to the last step of the decision procedure. For
example, if $\Phi$ contains the equation $\\{1\\}=\\{2\\}$, which is rewritten
by STEP as $1=_{\mathcal{X}}2$, calling $\mathit{SAT}_{\mathcal{X}}$ just
after STEP ends allows the solver to immediately detect that $\Phi$ is
unsatisfiable. Similarly, variable substitutions entailed by equalities
possibly returned by $\mathit{SAT}_{\mathcal{X}}$ are propagated to the whole
formula $\Phi$ as soon as possible. ∎

###  A.1 Nested RIS domains

According to the syntax of $\mathcal{L}_{\mathcal{RIS}}$ (see Section 2), RIS
domains can be a nested chain of RIS, ending in a variable or an extensional
set. On the other hand, the rewrite rules presented in Section 3.2 and
Appendix A apply only to RIS whose domain is not another RIS. We do so because
the rewrite rules for the most general case are more complex, thus they would
hinder understanding of the decision procedure.

These more general rules, however, can be easily generated from the rules for
the simpler case. In this section we show how this generalization can be done
by showing how one of the rules presented in Section 3.2, namely rule (6), is
adapted to deal with the more general case. All other rewrite rules can be
generalized in the same way.

Consider a non-variable RIS whose domain is a nested chain of RIS where the
innermost domain is an extensional set. The generalization of rule (6) to a
RIS of this form is a follows:

$\displaystyle\\{\\{\dots\\{\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi_{1}\mathbin{\bullet}u_{1}\\}\dots\mid\phi_{m-1}\mathbin{\bullet}u_{m-1}\\}\mid\phi_{m}\mathbin{\bullet}u_{m}\\}=B\longrightarrow$
$\displaystyle\begin{split}&\\{\dots\\{\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi_{1}\mathbin{\bullet}u_{1}\\}\dots\mid\phi_{m-1}\mathbin{\bullet}u_{m-1}\\}=\\{n\mathbin{\scriptstyle\sqcup}N\\}\\\
&\land(\phi(n)\land\\{u_{m}(n)\mathbin{\scriptstyle\sqcup}\\{N\mid\phi_{m}\mathbin{\bullet}u_{m}\\}\\}=B\\\
&\quad\lor\lnot\phi(n)\land\\{N\mid\phi_{m}\mathbin{\bullet}u_{m}\\}=B)\end{split}$

where $n$ and $N$ are two new variables. Note that the first element $n$ of
the domain of the outermost RIS is obtained by the recursive application of
the same rules for equality, over the domain itself (possibly another RIS) and
the extensional set $\\{n\mathbin{\scriptstyle\sqcup}N\\}$. Note also that
when $m=1$ this rule boils down to rule (6) of Figure 1.

###  A.2 Control Terms

As with nested RIS domains, we preferred not to show the rewrite rules when
the control term is not a variable, as these rules are somewhat more complex
than the others.

According to Definition 2.3, when the control term is not a variable then it
is an ordered pair of the form $(x,y)$ where both components are variables.
Consider the following RIS:

$\\{(x,y):\\{(1,2),55\\}\mid\phi\mathbin{\bullet}u\\}$

The problem with this RIS is that $(x,y)$ does not unify with $55$, for all
$x$ and $y$. The semantics of RIS stipulates that $55$ must not be considered
as a possible value on which evaluate $\phi$ and $u$.

As this example shows, it is necessary to consider one more case (i.e., one
more non-deterministic choice) in each rewriting rule. For example, if in rule
(6) we consider a general control term $c$, and not just a variable, the rule
is split into two rules:

$\displaystyle\begin{split}&\text{If $c\in\mathcal{V}$ or $d\in\mathcal{V}$ or
}\text{$(c\equiv f(x_{1},\dots,x_{n})$ and $d\equiv f(t_{1},\dots,t_{n}))$:
}\\\
&\\{c:\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}=B\longrightarrow\\\
&c=d\land\phi(d)\land\\{u(d)\mathbin{\scriptstyle\sqcup}\\{c:D\mid\phi\mathbin{\bullet}u\\}\\}=B\\\
&\lor
c=d\land\lnot\phi(d)\land\\{c:D\mid\phi\mathbin{\bullet}u\\}=B\end{split}$
$\displaystyle\begin{split}&\text{If $c\equiv f(x_{1},\dots,x_{n})$ and
$d\equiv g(t_{1},\dots,t_{m})$ and $(f\not\equiv g$ or $n\not\equiv m)$: }\\\
&\\{c:\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}=B\longrightarrow\\{c:D\mid\phi\mathbin{\bullet}u\\}=B\end{split}$

Note how the second rule simply skips $d$.

##  Appendix B Source code of the Bell-LaPadula case study

    :- int_solver(clpq).

    dominates([L1,C1],[L2,C2]) :-
      subset(C1,C2) & L1 =< L2.

    openRead(ScF,ScP,Proctbl,P,F,Proctbl_) :-
      [P,F] nin Proctbl &
      apply(ScF,F,[Lf,Cf]) &
      apply(ScP,P,[Lp,Cp]) &
      dominates([Lf,Cf],[Lp,Cp]) &
      Proctbl_ = {[P,F]/Proctbl}.

    seccond(ScF,ScP,Proctbl) :-
      foreach([Pi,Fi] in Proctbl,
              [Lf1,Cf1,Lp1,Cp1],
              subset(Cf1,Cp1) & Lf1 =< Lp1,
              apply(ScF,Fi,[Lf1,Cf1]) & apply(ScP,Pi,[Lp1,Cp1])
             ).

    openReadPreservesSeccond(ScF,ScP,Proctbl) :-
      seccond(ScF,ScP,Proctbl) &
      openRead(ScF,ScP,Proctbl,P,F,Proctbl_) &
      nforeach([Pi,Fi] in Proctbl_,
               [Lf1,Cf1,Lp1,Cp1],
               subset(Cf1,Cp1) & Lf1 =< Lp1,
               apply(ScF,Fi,[Lf1,Cf1]) & apply(ScP,Pi,[Lp1,Cp1])
              ).

##  Appendix C Detailed Proofs

This section contains detailed proofs of the theorems stated in the main text,
along with some results that justify some of our claims. We start with the
justification that RIS can be used to encode restricted universal quantifiers.

######  Proposition C.1.

$\displaystyle D\subseteq\\{x:D\mid F\\}\Leftrightarrow\forall x(x\in
D\implies F)$

######  Proof C.2.

$\Longrightarrow$)

$\displaystyle x\in D$ $\displaystyle\implies x\in\\{x:D\mid F\\}$ [by H]
$\displaystyle\implies x\in D\land F(x)$ [by RIS def.] $\displaystyle\implies
F(x)$

$\Longleftarrow$)

$\displaystyle x\in D$ $\displaystyle\implies F(x)$ [by H]
$\displaystyle\implies x\in D\land F(x)$ $\displaystyle\implies x\in\\{x:D\mid
F\\}$ [by RIS def.]

The following proposition supports the claim that to force a RIS to be empty
it is enough to consider its filter.

######  Proposition C.3.

If $D$ is a non-empty set, then:

$\displaystyle\\{x:D\mid\phi\mathbin{\bullet}u\\}=\emptyset\Leftrightarrow\forall
x(x\in D\implies\lnot\phi(x))$

######  Proof C.4.

$\displaystyle\\{x:D\mid\phi\mathbin{\bullet}u\\}=\emptyset$
$\displaystyle\Leftrightarrow\\{y:\exists d(x\in D\land\phi\land
y=u)\\}=\emptyset$ $\displaystyle\Leftrightarrow\forall y(\lnot\exists d(d\in
D\land\phi\land y=u))$ $\displaystyle\Leftrightarrow\forall y(\forall
d(d\notin D\lor\lnot\phi(d)\lor y\neq u(d)))$
$\displaystyle\Leftrightarrow\forall d(d\in D\implies\lnot\phi(d))$

The following proposition supports the claim that many RIS parameters can be
avoided by a convenient control term.

######  Proof C.5 (of Proposition 6.1).

$\Longrightarrow$)

$\displaystyle a\in S$ $\displaystyle\Leftrightarrow\exists x,\vec{p}(x\in
D\land\vec{p}\in D_{2}\land F(x,\vec{v},\vec{p})\land P(x,\vec{v},\vec{p})=a)$
[by H; RIS def.] $\displaystyle\Leftrightarrow\exists x,\vec{p}((x,\vec{p})\in
D\times D_{2}\land F(x,\vec{v},\vec{p})\land P(x,\vec{v},\vec{p})=a)$ [by
$\times$ def.] $\displaystyle\Leftrightarrow a\in\\{(x,\vec{p}):D_{1}\times
D_{2}\mid F((x,\vec{p}),\vec{v})\mathbin{\bullet}P((x,\vec{p}),\vec{v})\\}$
[by RIS def.]

$\Longleftarrow$) Similar to the previous case.

Now we prove Proposition 6.8 which gives the conditions to eliminate
existential quantifiers appearing in RIS filters in relation to functional
predicates.

######  Proof C.6 (of Proposition 6.8).

Note that:

$\displaystyle\forall
y(\lnot(p(x_{1},\dots,x_{n-1},y)\land\phi_{r}(\vec{x}_{r},y)))$
$\displaystyle\Leftrightarrow\forall y(\lnot
p(x_{1},\dots,x_{n-1},y)\lor\lnot\phi_{r}(\vec{x}_{r},y))$ (1)

Now we divide the proof into two implications.

$\Longrightarrow$) If $\phi_{q}(\vec{x}_{q})$ does not hold the conclusion is
proved. Now assume $\phi_{q}(\vec{x}_{q})$ holds. Then
$p(x_{1},\dots,x_{n-1},z)$ holds for some $z$ due to the hypothesis and
Definition 6.7. Hence for (1) to be true, $\phi_{r}(\vec{x}_{r},z)$ must be
false (because otherwise the disjunction would be true for $z$). So in this
case we have $\phi_{q}(\vec{x}_{q})\land
p(x_{1},\dots,x_{n-1},z)\land\lnot\phi_{r}(\vec{x}_{r},z)$, which proves the
conclusion.

$\Longleftarrow$) If $\phi_{q}(\vec{x}_{q})$ does not hold then
$p(x_{1},\dots,x_{n-1},y)$ does not hold for all $y$ due to the hypothesis and
Definition 6.7. Hence the conclusion.

Now assume $z$ is such that $\phi_{q}(\vec{x}_{q})\land
p(x_{1},\dots,x_{n-1},z)\land\lnot\phi_{r}(\vec{x}_{r},z)$ is true. Then the
conclusion is true for $z$ because $\phi_{r}(\vec{x}_{r},z)$ is false. Now
consider any $y\neq z$. Given that $p$ is a functional predicate symbol
(hypothesis), then we have $\lnot p(x_{1},\dots,x_{n-1},y)$ because $p$ can
hold for at most one value of its last parameter (and we know it holds for
$z$). So the conclusion.

The next subsections provide the proofs of the theorems stated in the main
text. All these proofs concern the base $\mathcal{L}_{\mathcal{RIS}}$
language, not the possible extensions discussed in Section 6 nor those
presented in Appendixes A.1 and A.2.

###  C.1 Satisfiability of the solved form (Theorem 4.10)

Basically, the proof of this theorem uses the fact that, given a pure
$\mathcal{RIS}$-formula $\Phi$ verifying the conditions of the theorem, it is
possible to guarantee the existence of a successful assignment of values to
all variables of $\Phi$ using pure sets only, with the only exception of the
variables $X$ occurring in terms of the form $X=u$—which are obviously already
assigned. In particular, the solved forms involving variable RIS verify the
following ($X_{i}$ are variables; $R_{i}$ are variables or variable-RIS whose
domain is variable $X_{i}$):

  * •

$t\notin\\{X_{1}\mid\phi\mathbin{\bullet}u\\}$

  * •

$\\{X_{1}\mid\phi\mathbin{\bullet}u\\}=\varnothing$

  * •

$\\{X_{1}\mid\phi_{1}\mathbin{\bullet}u_{1}\\}=\\{X_{2}\mid\phi_{2}\mathbin{\bullet}u_{2}\\}$

  * •

$\mathit{un}(R_{3},R_{4},R_{5})$

  * •

$R_{3}\parallel R_{4}$

are solved with $X_{i}=\emptyset$ and $R_{i}=\emptyset$ for those $R_{i}$ that
are variables.

In the proof we use the auxiliary function $\mathit{find}$:

$\mathit{find}(x,t)=\begin{cases}\emptyset&\text{if
}t=\emptyset,x\neq\emptyset\\\ \\{0\\}&\text{if $t=x$}\\\
\\{1+n:n\in\mathit{find}(x,y)\\}&\text{if
}t=\\{y\mathbin{\scriptstyle\sqcup}\emptyset\\}\\\
\\{1+n:n\in\mathit{find}(x,y)\\}\cup\mathit{find}(x,s)&\text{if
}t=\\{y\mathbin{\scriptstyle\sqcup}s\\},s\neq\emptyset\end{cases}$

which returns the set of ‘depths’ at which a given element $x$ occurs in the
set $t$.

######  Proof C.7.

Consider a pure $\mathcal{RIS}$-formula $\Phi$ in solved form. The proof is
basically the construction of a mapping for the variables of $\Phi$ of sort
$\mathsf{Set}$ into the interpretation domain $D_{\mathsf{Set}}$ (see Section
C.2 to see how variables of sort $\mathcal{X}$ are managed). The construction
is divided into two parts by dividing $\Phi$ as $\Phi_{=}\land\Phi_{r}$, where
$\Phi_{=}$ is a conjunction of equalities whose l.h.s is a variable, and
$\Phi_{r}$ is the rest of $\Phi$. In the first part $\Phi_{=}$ is not
considered. A solution for $\Phi_{r}$ is computed by looking for
valuations777A _valuation_ $\sigma$ of a $\Sigma$-formula $\varphi$ is an
assignment of values from the interpretation domain $D_{\mathsf{X}}$ to the
free variables of $\varphi$ which respects the sorts of the variables. of the
form:

$X_{i}\mapsto\underbrace{\\{\cdots\\{}_{n_{i}}\emptyset\\}\cdots\\}\vspace*{-2ex}$
(2)

fulfilling all $\neq$ and $\notin$ constraints. We will briefly refer to the
r.h.s. of (2) as $\\{\emptyset\\}^{n_{i}}$. In particular, RIS domains are
mapped onto $\emptyset$ ($n_{i}=0$) and the numbers $n_{i}$ for the other
variables are computed choosing one possible solution of a system of integer
equations and disequations, that trivially admits solutions. Such system is
obtained by analyzing the ‘depth’ of the occurrences of the variables in the
terms. Then, all the variables occurring in $\Phi$ only in r.h.s. of equations
of $\Phi_{=}$ are bound to $\emptyset$ and the mappings for the variables of
the l.h.s. are bound to the uniquely induced valuation.

In detail, let $X_{1},\dots,X_{m}$ be all the variables occurring in $\Phi$,
save those occurring in the l.h.s. of equalities, and let $X_{1},\dots,X_{h}$,
$h\leq m$, be those variables occurring as domains of RIS terms. Let
$n_{1},\dots,n_{m}$ be auxiliary variables ranging over $\mathbb{N}$. We build
the system Syst as follows:

  * •

For all $i\leq h$, add the equation $n_{i}=0$.

  * •

For all $h<i\leq m$, add the following disequations:

$\begin{array}[]{ll}n_{i}\neq n_{j}+c&\forall X_{i}\neq t\text{ in }\Phi\text{
and }c\in\mathit{find}(X_{j},t)\\\ n_{i}\neq c&\forall X_{i}\neq t\text{ in
}\Phi\text{ and }t\equiv\\{\emptyset\\}^{c}\\\ n_{i}\neq n_{j}+c+1&\forall
t\notin X_{i}\text{ in }\Phi\text{ and }c\in\mathit{find}(X_{j},t)\\\
n_{i}\neq c+1&\forall t\notin X_{i}\text{ in }\Phi\text{ and
}t\equiv\\{\emptyset\\}^{c}\end{array}$

If $m=h$, then $n_{i}=0$ for all $i=1,\dots,m$ is the unique solution of Syst.
Otherwise, it is easy to observe that Syst admits infinitely many solutions.
Let:

  * •

$\\{n_{1}=0,\dots,n_{h}=0,n_{h+1}=\bar{n}_{h+1},\dots,n_{m}=\bar{n}_{m}\\}$ be
one arbitrarily chosen solution of Syst.

  * •

$\theta$ be the valuation such that $\theta(X_{i})=\\{\emptyset\\}^{n_{i}}$
for all $i\leq m$.

  * •

$Y_{1},\dots,Y_{k}$ be all the variables of $\Phi$ which appear only in the
l.h.s. of equalities of the form $Y_{i}=t_{i}$.

  * •

$\sigma$ be the valuation such that $\sigma(Y_{i})=\theta(t_{i})$.

We prove that $\mathcal{R}\models\Phi[\theta\sigma]$ by case analysis on the
form of the atoms in $\Phi$:

  * •

$Y_{i}=t_{i}$ It is satisfied, since $\sigma(Y_{i})$ has been defined as a
ground term and equal to $\theta(t_{i})$.

  * •

$X_{i}\neq t$ If $t$ is a ground term, then we have two cases: if $t$ is not
of the form $\\{\emptyset\\}^{c}$, then it is immediate that
$\theta(X_{i})\neq t$; if $t$ is of the form $\\{\emptyset\\}^{c}$, for some
$c$, then we have $n_{i}\neq c$, by construction, and hence $\theta(X_{i})\neq
t$.

If $t$ is not ground, then if $\theta(X_{i})=\theta(t)$, then there exists a
variable $X_{j}$ in $t$ such that $\bar{n}_{i}=\bar{n}_{j}+c$ for some
$c\in\mathit{find}(X_{j},t)$; this cannot be the case since we started from a
solution of $Syst$.

  * •

$t\not\in X_{i}$ Similar to the case above.

  * •

$\\{X_{i}\mid\phi\mathbin{\bullet}u\\}=\varnothing$ This means that
$\bar{n}_{i}=0$ and $\theta(X_{i})=\theta(X_{j})=\theta(X_{k})=\emptyset$.

  * •

$\\{X_{i}\mid\phi_{1}\mathbin{\bullet}u_{1}\\}=\\{X_{j}\mid\phi_{2}\mathbin{\bullet}u_{2}\\}$
This means that $\bar{n}_{i}=\bar{n}_{j}=0$ and
$\theta(X_{i})=\theta(X_{j})=\emptyset$.

  * •

$\mathit{un}(R_{i},R_{j},R_{k})$ Recall that $R_{i},R_{j},R_{k}$ can be either
variables or variable-RIS whose domain are variables $X_{i},X_{j},X_{k}$,
respectively. Now, those $R$ that are variables are replaced by a
corresponding $X$ and for those that are not the valuation is computed for the
domains (which are variables, by construction). For example, if $R_{i}$ and
$R_{k}$ are variable-RIS and $R_{j}$ is a variable, we have
$\mathit{un}(R_{i},X_{j},R_{k})$, $X_{i}$ is the domain of $R_{i}$, $X_{k}$ is
the domain of $R_{k}$ and the valuation is computed for $X_{i}$, $X_{j}$ and
$X_{k}$. Also recall that from item 5 of Definition 4.8, there are no $\neq$
constraints involving any of the $X$ participating of the $\mathit{un}$
constraint. Then, this means that $\bar{n}_{i}=\bar{n}_{j}=\bar{n}_{k}=0$ and
$\theta(X_{i})=\theta(X_{j})=\theta(X_{k})=\emptyset$.

  * •

$R_{i}\parallel R_{j}$ Similar considerations for $R_{i}$ and $R_{j}$ to the
previous case apply. Then:

    * –

If $i,j\leq h$, then $\theta(X_{i})=\theta(X_{j})=\emptyset$

    * –

If $i>h$ (the same if $j>h$), then $\bar{n}_{i}\neq\bar{n}_{j}$ and so
$\theta(X_{i})=\\{\emptyset\\}^{n_{i}}$ is disjoint from
$\theta(X_{j})=\\{\emptyset\\}^{n_{j}}$.

###  C.2 Satisfiability of $\Phi_{\mathcal{S}}\land\Phi_{\mathcal{X}}$
(Theorem 4.12)

The satisfiability of $\Phi_{\mathcal{X}}$ is determined by
$\mathit{SAT}_{\mathcal{X}}$. Since $\mathit{SAT}_{\mathcal{X}}$ is a decision
procedure for $\mathcal{X}$-formulas, if $\Phi_{\mathcal{X}}$ is
unsatisfiable, then $\mathit{SAT}_{\mathcal{X}}$ returns $\mathit{false}$;
hence, $\Phi$ is unsatisfiable. If $\Phi_{\mathcal{X}}$ is satisfiable, then
$\mathit{SAT}_{\mathcal{X}}$ rewrites $\Phi_{\mathcal{X}}$ into an
$\mathcal{X}$-formula in a simplified form which is guaranteed to be
satisfiable w.r.t. the interpretation structure of
$\mathcal{L}_{\mathcal{X}}$. This rewriting, however, may cause non-set
variables in $\Phi_{\mathcal{X}}$, i.e., variables of sort $\mathsf{X}$, to
get values for which the formula is satisfied. These variables can occur in
both $\Phi_{\mathcal{X}}$ and $\Phi_{\mathcal{S}}$. Given that, at this point,
$\Phi_{\mathcal{S}}$ is in solved form, variables of sort $\mathsf{X}$ can
only appear in constraints that are in solved form. Specifically, if $x$ is a
variable of sort $\mathsf{X}$, the following are all solved form constraints
that may contain $x$:

  1. 1.

$X=S(x)$ or $X=\\{Y\mid\phi(x)\mathbin{\bullet}u(x)\\}$ (i.e., $x$ is a free
variable in the RIS)

  2. 2.

$\\{X\mid\phi(x)\mathbin{\bullet}u(x)\\}=\varnothing$ or
$\varnothing=\\{X\mid\phi(x)\mathbin{\bullet}u(x)\\}$

  3. 3.

$\\{X\mid\phi_{1}(x)\mathbin{\bullet}u_{1}(x)\\}=\\{Y\mid\phi_{2}(x)\mathbin{\bullet}u_{2}(x)\\}$.

  4. 4.

$X\neq S(x)$

  5. 5.

$t(x)\notin\bar{D}$

  6. 6.

$\mathit{un}(\bar{C},\bar{D},\bar{E})$ and $\bar{C}$ or $\bar{D}$ or $\bar{E}$
are of the form $\\{X\mid\phi(x)\mathbin{\bullet}u(x)\\}$

  7. 7.

$\bar{C}\parallel\bar{D}$, and $\bar{C}$ or $\bar{D}$ are of the form
$\\{X\mid\phi(x)\mathbin{\bullet}u(x)\\}$

All these constraints remains in solved form regardless of the value bound to
$x$. Hence, $\Phi$ is satisfiable.

###  C.3 Termination of $\mathit{SAT}_{\mathcal{RIS}}$ (Theorem 4.16)

In order to prove termination of $\mathit{SAT}_{\mathcal{RIS}}$ we use the
rules give in Appendix A for equality, inequality, set membership, and not set
membership, and those for union and disjointness given in Figures 3 and 4 in
the main text.

First of all, it is worth noting that the requirement that the set of
variables ranging on $\mathcal{RIS}$-terms (i.e., variables of sort
$\mathsf{Set}$) and the set of variables ranging on $\mathcal{X}$-terms (i.e.,
variables of sort $\mathsf{X}$) are disjoint sets prevents us from creating
recursively defined RIS, which could compromise the finiteness property of the
sets we are dealing with. In fact, a formula such as $X=\\{D\mid
F(X)\mathbin{\bullet}P\\}$, where $F$ contains the variable $X$, is not an
admissible $\mathcal{RIS}$-constraint, since the outer $X$ should be of sort
$\mathsf{Set}$ whereas the inner $X$ should be of sort $\mathsf{X}$ (recall
that the filter is a $\mathcal{X}$-formula). Note that, on the contrary, a
formula such as $X=\\{D(X)\mid F\mathbin{\bullet}P\\}$ is an admissible
formula, which, in many cases, is suitably handled by our decision procedure.

Let a _rewriting procedure for $\pi$_ be the repeated application of the
rewrite rules for a specific $\mathcal{RIS}$-constraint $\pi$ until either the
initial formula becomes $\mathit{false}$ or no rules for $\pi$ apply.
Following [Dovier et al. (2000)], we begin by proving that each individual
rewriting procedure, applied to an admissible formula, is _locally
terminating_ , that is each call to such procedures will stop in a finite
number of steps. For all the rules inherited from CLP($\mathcal{SET}$) we
assume the results in [Dovier et al. (2000)]. Then we prove local termination
only for the new rules dealing with RIS.

The following are non-recursive rules thus they terminate trivially:
($=_{1}$), ($=_{2}$), ($=_{3}$), ($=_{4}$), ($=_{5}$), ($=_{7}$),
($\neq_{1}$), ($\neq_{2}$), ($\neq_{3}$), ($\neq_{4}$), ($\neq_{5}$),
($\neq_{6}$), ($\neq_{7}$), ($\in_{1}$), ($\in_{3}$), ($\in_{4}$),
($\notin_{1}$), (13), (14), (15), (16), (21), (22) and (23).

Now we consider rules which contain direct recursive calls or calls to other
rules of the same rewriting procedure and involve at least one RIS. Figures
8-10 show what rewrite rule calls other rewrite rules of the same rewriting
procedure, for $=$, $\mathit{un}$ and $\parallel$, respectively. We only
depict these because the other rewriting procedures are simpler. We will pay
special attention to the possible loops that can be seen in all three graphs.

($=_{9}$)($=_{3}$)($=_{12}$) ($=_{13}$)($=_{11}$)($=_{14}$)($=_{6}$)($=_{8}$)
Figure 8: Calls relation between rules of the $=$-rewriting procedure
(19)(17)(18)(20)($\mathit{un}$-a) Figure 9: Calls relation between rules of
the $\mathit{un}$-rewriting procedure (24)(25)(26)(27) Figure 10: Calls
relation between rules of the $\parallel$-rewriting procedure

Rule ($=_{6}$)

In all branches, the recursive call is made with at least one argument whose
size is strictly smaller than the one of the input formula. In particular, in
the last branch the size of $X$ will not affect the size of the arguments of
the recursive call because $X$ is a variable so it cannot add elements to $N$,
$N$ is a variable itself and $X$ is removed from the recursive call.

Rule ($=_{8}$)

In the first seven branches, the recursive call is made with at least one
argument whose size is strictly smaller than the one of the input formula. In
the last branch, the recursive call is made with arguments whose size is equal
to those of the input formula. Indeed, we remove $t_{0}$ from the l.h.s. set
but we add $u(n)$ while variable $X$ is substituted by the new variable $N$.
However, we now know that $u(n)=s_{j}$ for some $j\in[0,k]$. Hence, the
recursive call will be processed by one of the first seven branches which we
know reduce the size of at least one of their arguments.

Rule ($=_{9}$)

We will prove termination of this rule by describing a particular abstract
implementation.

  1. 1.

If the set parts of $A$ and $B$ are not RIS, then the results of [Dovier et
al. (2000)] apply.

  2. 2.

If the set part of either $A$ or $B$ are RIS, then:

    1. (a)

‘Empty’ their domains. This means that if one of the RIS is of the form:

$\\{\\{d_{1},\dots,d_{k}\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}$

then rewrite this set into:

$\\{u(d_{1})\mathbin{\scriptstyle\sqcup}\\{\\{d_{2},\dots,d_{k}\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}\\}$

or

$\\{\\{d_{2},\dots,d_{k}\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}$

depending on whether $\phi(d_{1})$ holds or not. Continue with this rewriting
until all the $d_{i}$ have been processed. This process will transform the
initial RIS into a number of sets of the form:

$\\{u(d_{i_{1}}),\dots,u(d_{i_{m}})\mathbin{\scriptstyle\sqcup}\\{D\mid\phi\mathbin{\bullet}u\\}\\}$
(3)

with $\\{d_{i_{1}},\dots,d_{i_{m}}\\}\subseteq\\{d_{1},\dots,d_{k}\\}$ and $D$
variable or the empty set.

Hence, at the end of this process the domains of the RIS so generated are
either the empty set or a variable.

    2. (b)

If the domain of one of the RIS obtained in the previous step is the empty set
then substitute the RIS by the empty set. Then RIS of the form (3) become
$\\{u(d_{i_{1}}),\dots,u(d_{i_{m}})\mathbin{\scriptstyle\sqcup}\emptyset\\}$
which is equal to $\\{u(d_{i_{1}}),\dots,u(d_{i_{m}})\\}$.

Hence, at the end of this process the domains of the RIS so generated are
variables.

    3. (c)

Substitute the RIS by new variables. Formally (when at both sides there are
RIS):

$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{D\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{E\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle\longrightarrow$
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N_{1}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N_{2}\\}$
(a) $\displaystyle{}\land N_{1}=\\{D\mid\phi\mathbin{\bullet}u\\}\land
N_{2}=\\{E\mid\gamma\mathbin{\bullet}v\\}$

Note that might be no more RIS at this point, so there is nothing to
substitute.

  3. 3.

Now apply rule ($=_{9}$) only to the first conjunct of (a) as in [Dovier et
al. (2000)] until it terminates, delaying the processing of the remaining
conjuncts in (a). As no RIS are in the first conjunct of (a) the results of
[Dovier et al. (2000)] apply.

  4. 4.

Once rule ($=_{9}$) applied to the first conjunct terminates, variables
$N_{i}$ are substituted back by the corresponding RIS, thus obtaining
equalities of the following forms:

$\displaystyle\\{D\mid\phi\mathbin{\bullet}u\\}=\\{E\mid\gamma\mathbin{\bullet}v\\}$
$\displaystyle\\{D\mid\phi\mathbin{\bullet}u\\}=\\{\cdot\mathbin{\scriptstyle\sqcup}N\\}$
$\displaystyle\\{D\mid\phi\mathbin{\bullet}u\\}=\\{\cdot\mathbin{\scriptstyle\sqcup}\\{E\mid\gamma\mathbin{\bullet}v\\}\\}$

where $D$ and $E$ are variables (due to the process described in step 2).

Note that, without RIS, the final formulas returned by ($=_{9}$) would be in
solved form as their l.h.s. would be variables.

  5. 5.

As can be seen, by the form of the returned equalities and by Figure 8, these
equalities are processed by some of the rules added to deal with RIS.

So ($=_{9}$) either terminates as in [Dovier et al. (2000)], or calls other
rules for equality (which is an added behavior compared to [Dovier et al.
(2000)]).

Rule ($=_{10}$)

The recursive call is made with one argument whose size is strictly smaller
than in the initial formula, since $t$ is removed from the domain of the RIS.

Rule ($=_{11}$)

In the first branch there is no recursion on the same rule because the l.h.s.
of the equality constraint is no longer a RIS but an extensional set. In
particular, the size of the arguments are the same w.r.t. the initial ones.
However, the rules that can be fired in this case (see Figure 8 and the
analysis for the corresponding rules), all reduces the size of at least one of
its arguments. In particular, if rules ($=_{9}$) or ($=_{14}$) are called, if
they call this rule back, it will be done with strictly smaller arguments.
Then, this loop will run a finite number of times.

In the second branch the recursive call is made with one argument whose size
is strictly smaller than in the initial formula, since $t$ is removed from the
domain of the RIS.

Rule ($=_{12}$)

The size of the r.h.s. argument of the equality constraint is strictly smaller
than the one of the input formula because $t_{0}$ has been removed.
Furthermore, the size of $X$ will not affect the size of the arguments of the
recursive call because $X$ is a variable so it cannot add elements to $N$, $N$
is a variable itself and $X$ is removed from the recursive call.

Rule ($=_{13}$)

Same arguments of previous rule apply.

Rule ($=_{14}$)

The recursive call is made with one argument whose size is strictly smaller
than in the initial formula, since $t$ is removed from the r.h.s. The size of
$D$ can affect the size of the arguments of the recursive call only if $D$ is
the set part of $A$. However, this case is processed by one of the following
rules: ($=_{12}$) or ($=_{13}$).

Rule ($\in_{2}$)

The recursive call is made with a r.h.s. argument whose size is strictly
smaller than the initial one because $s$ is removed from the set.

Rule ($\notin_{2}$)

Same arguments of previous rule apply.

Rule ($\notin_{3}$)

In either branch the recursive call is made with a r.h.s. argument whose size
is strictly smaller than the initial one because $d$ is removed from the
domain of the RIS.

Rule (17)

In the first branch the recursive call is made with a first argument whose
size is strictly smaller than the initial one because $t$ is removed from it.
In the second branch, it is both arguments whose sizes are strictly smaller
than the initial ones because $t$ is effectively removed from $A$ given that
we know that $t\in A$.

Note that in Figure 9 this rule may call rule (20), which in turn may call
back this rule or rules (18) and (19), thus possibly generating an infinite
loop. However, this rule can call (20) only when the first or second argument
is a non-variable RIS. In that case, rule (20) removes one element of the
domain of the RIS but it does not necessarily reduces the size of the
arguments. This may fire the callback to this rule. But this rule reduces the
size of its arguments, so after a finite number of calls the loop finishes.
This shows how the arrow labeled ($\mathit{un}$-a) in Figure 9 can be
traversed only a finite number of times.

See below for an analysis of rule (20).

Rule (18)

Symmetric arguments to previous rule apply.

Rule (19)

In all branches the size of the third argument of the recursive call is
strictly smaller than the initial one because $t$ is removed from it.

Rule (20)

Consider the non-variable RIS arguments of this rule. The rule transforms
these RIS into either extensional sets or new RIS.

  1. 1.

If all such arguments are transformed into extensional sets, then the rule
does not recur on itself (but calls other rules of the $\mathit{un}$
constraint).

  2. 2.

If all such arguments are transformed into variable RIS, then the rule does
not recur on itself (but calls other rules of the $\mathit{un}$ constraint or,
possibly, is in solved form).

  3. 3.

If at least one of such arguments is still a non-variable RIS, then there is a
recursive call but the size of that argument is strictly smaller than the
initial one. In effect, this case occurs when the initial argument in question
is of the following form
$\\{x:\\{a,b\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}$
with $a\neq b$ and $\lnot\phi(a)$. That is, the initial argument is a non-
variable RIS with at least two elements in its domain but the “first” one does
not satisfy the filter. Then, $u(a)$ does not belong to the RIS and so it is
equal to
$\\{x:\\{b\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}$.
Precisely, this last RIS is used as the argument to the recursive call. Hence,
at least one argument of the recursive call is strictly smaller than the
initial one.

Nevertheless, if $\phi(a)$ holds, then $a$ is removed from the domain but the
RIS becomes the set part of an extensional set with $u(a)$ as its element
part. In this case, the size of this argument is equal to the initial one.
However, in this case, there is no recursive call but a call to one of rules
(17), (18) and (19), which effectively reduce the size of one of its.

Rule (24)

The recursive call is made with a r.h.s. argument whose size is strictly
smaller than the initial one because $t$ is removed from the set.

Rule (25)

Symmetric arguments of previous rule apply.

Rule (26)

In either branch the recursive call is made with a r.h.s. argument whose size
is strictly smaller than the initial one because $d$ is removed from the
domain of the RIS.

Rule (27)

Symmetric arguments of previous rule apply.

Therefore, the loops shown in Figure 10 end in a finite number of times since
rules (24)-(27) reduce the size of at least one of their arguments every time
they are called.

Local termination of each individual procedure, however, does not guarantee
global termination of $\mathit{SAT}_{\mathcal{RIS}}$, since the different
procedures may be dependent on each other. However, we observe that rewrite
rules not involving RIS in their left-hand sides do not construct any new RIS
term in their right-hand sides. They simply treat RIS terms as any other term.
Hence the presence of RIS terms do not affect their termination, which has
been proved in [Dovier et al. (2000)]. Hence, it is enough to consider only
the new rules involving RIS terms.

Rules involving RIS generate both $\mathcal{RIS}$\- and
$\mathcal{X}$-formulas. The $\mathit{SAT}_{\mathcal{X}}$ solver solves the
$\mathcal{X}$-formulas without producing $\mathcal{RIS}$-formulas. Then, for
each constraint $\pi$ and each recursive rewrite rule for it, we will analyze
what $\mathcal{RIS}$-constraints other than $\pi$ are generated. In this way
we will see if there are cycles between rewriting procedures. We proceed by
rule inspection.

  1. 1.

Rules ($\neq_{5}$), ($\neq_{6}$) and ($\neq_{7}$) generate $\in$\- and
$\notin$-constraints.

  2. 2.

Rule ($\in_{3}$) generates $=$-constraints.

  3. 3.

Rules (17), (18) and (19) generate $=$-constraints.

  4. 4.

Rules (24), (25), (26) and (27), generate $\notin$-constraints.

This is depicted in Figure 11. Hence, as can be seen, there are no loops
between the rewriting procedures.

$\neq$$\in$$=$$\parallel$$\notin$$\mathit{un}$ Figure 11: Calls relation
between rewriting procedures

###  C.4 Equisatisfiability (Theorem 4.14)

This section contains the detailed proofs on the equisatisfiability of the
rewrite rules involving RIS presented in Sect. 3.2 and Appendix A; the
equisatisfiability of the remaining rules has been proved elsewhere [Dovier et
al. (2000)]. Hence, these proofs use the rules considering that the control
expression is a variable and that the domain of RIS are not other RIS. These
proofs can be easily extended to the more general case.

In the following theorems and proofs, $\phi$, $\gamma$, $u$ and $v$ are
shorthands for $F(x)$, $P(x)$, $G(x)$ and $Q(x)$, respectively. Moreover, note
that a set of the form $\\{P(x):F(x)\\}$ (where pattern and filter are
separated by a colon ($:$), instead of a bar ($\mid$), and the pattern is
_before_ the colon) is a shorthand for $\\{y:\exists x(P(x)=y\land F(x))\\}$.
That is, the set is written in the classic notation for intensional sets used
in mathematics. Finally, $H$ denotes the current hypothesis.

$u$ and $v$ are assumed to be bijective patterns. Recall that all patterns
allowed in $\mathcal{L}_{\mathcal{RIS}}$ fulfill this condition. The condition
on the bijection of patterns is necessary to prove equisatisfiability for rule
(7).

The proof of Theorem 4.14 rests on a series of lemmas each of which shows that
the set of solutions of left and right-hand sides of each rewrite rule is the
same.

######  Lemma C.8 (Equivalence of rule ($=_{1}$)).

We consider only the following case; all the others covered by this rule are
either symmetric or trivial.

$\displaystyle\\{x:\emptyset\mid\phi\mathbin{\bullet}u\\}=\emptyset$

######  Proof C.9.

$\displaystyle\\{x:\emptyset\mid\phi\mathbin{\bullet}u\\}$
$\displaystyle=\\{u(x):x\in\emptyset\land\phi(x)\\}$
$\displaystyle=\\{u(x):\mathit{false}\land\phi(x)\\}$
$\displaystyle=\\{u(x):\mathit{false}\\}$ $\displaystyle=\emptyset$

######  Proposition C.10.

$\displaystyle\begin{split}\forall d,&D:\\\
&\\{x:\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}=\\{u(d)\mid\phi(d)\\}\cup\\{u(x)\mid
x\in D\land\phi(x)\\}\end{split}$

######  Proof C.11.

Taking any $d$ and $D$ we have:

$\displaystyle\\{x:\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}$
$\displaystyle=\\{u(x):x\in\\{d\mathbin{\scriptstyle\sqcup}D\\}\land\phi(x)\\}$
$\displaystyle=\\{u(x):(x=d\lor x\in D)\land\phi(x)\\}$
$\displaystyle=\\{u(x):(x=d\land\phi(x))\lor(x\in D\land\phi(x))\\}$
$\displaystyle=\\{u(x):x=d\land\phi(x)\\}\cup\\{u(x)\mid x\in
D\land\phi(x)\\}$ $\displaystyle=\\{u(d):\phi(d)\\}\cup\\{u(x)\mid x\in
D\land\phi(x)\\}$

######  Lemma C.12 (Equivalence of rule ($=_{3}$)).

We will consider only the case where
$S\equiv\\{c:\textbf{{X}}\mid\phi\mathbin{\bullet}u\\}$ with $c\equiv u$,
because the other one is proved in [Dovier et al. (2000)]:

$\displaystyle\begin{split}\forall X,&t_{0},\dots,t_{k}:\\\
&X=\\{t_{0},\dots,t_{k}\mathbin{\scriptstyle\sqcup}\\{c:\textbf{{X}}\mid\phi\mathbin{\bullet}u\\}\\}\\\
&\Leftrightarrow
X=\\{t_{0},\dots,t_{k}\mathbin{\scriptstyle\sqcup}\\{c:\textbf{{X}}[X/N]\mid\phi\mathbin{\bullet}u\\}\\}\end{split}$

where $N$ is a new variable.

######  Proof C.13.

Taking any $X,t_{0},\dots,t_{k}$ we have:

$\displaystyle
X=\\{t_{0},\dots,t_{k}\mathbin{\scriptstyle\sqcup}\\{c:\textbf{{X}}\mid\phi\mathbin{\bullet}u\\}\\}$
[by def. of X with $a\geq 0$] $\displaystyle\Leftrightarrow
X=\\{t_{0},\dots,t_{k}\\}\cup\\{c:\\{s_{1},\dots,s_{a}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}$
[by def. $\mathbin{\scriptstyle\sqcup}$] $\displaystyle\Leftrightarrow
X=\\{t_{0},\dots,t_{k}\\}\cup\\{c:\\{s_{1},\dots,s_{a}\\}\cup
X\mid\phi\mathbin{\bullet}u\\}$ [by prop. intensional sets]
$\displaystyle\Leftrightarrow
X=\\{t_{0},\dots,t_{k}\\}\cup\\{c:\\{s_{1},\dots,s_{a}\\}\mid\phi\mathbin{\bullet}u\\}\cup\\{c:X\mid\phi\mathbin{\bullet}u\\}$

Now note that if $c\equiv u$, then:

$\\{c:X\mid\phi\mathbin{\bullet}u\\}\subseteq X$

If $\\{c:X\mid\phi\mathbin{\bullet}u\\}=X$, then:

$\displaystyle
X=\\{t_{0},\dots,t_{k}\\}\cup\\{c:\\{s_{1},\dots,s_{a}\\}\mid\phi\mathbin{\bullet}u\\}\cup\\{c:X\mid\phi\mathbin{\bullet}u\\}$
[by $A=B\cup A\Leftrightarrow B\subseteq A$]
$\displaystyle\Leftrightarrow\\{t_{0},\dots,t_{k}\\}\cup\\{c:\\{s_{1},\dots,s_{a}\\}\mid\phi\mathbin{\bullet}u\\}\subseteq\\{c:X\mid\phi\mathbin{\bullet}u\\}$
[by exists $N$ completing $\\{c:X\mid\phi\mathbin{\bullet}u\\}$]
$\displaystyle\Leftrightarrow\\{t_{0},\dots,t_{k}\\}\cup\\{c:\\{s_{1},\dots,s_{a}\\}\mid\phi\mathbin{\bullet}u\\}\cup\\{c:N\mid\phi\mathbin{\bullet}u\\}=\\{c:X\mid\phi\mathbin{\bullet}u\\}$
$\displaystyle\Leftrightarrow\\{t_{0},\dots,t_{k}\\}\cup\\{c:\\{s_{1},\dots,s_{a}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}=\\{c:X\mid\phi\mathbin{\bullet}u\\}$
$\displaystyle\Leftrightarrow
X=\\{t_{0},\dots,t_{k}\\}\cup\\{c:\\{s_{1},\dots,s_{a}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}$
$\displaystyle\Leftrightarrow
X=\\{t_{0},\dots,t_{k}\\}\cup\\{c:\textbf{{X}}[N/X]\mid\phi\mathbin{\bullet}u\\}$

If $\\{c:X\mid\phi\mathbin{\bullet}u\\}\subset X$, then let $N$ be the
(proper) subset of $X$ such that
$\\{c:N\mid\phi\mathbin{\bullet}u\\}=\\{c:X\mid\phi\mathbin{\bullet}u\\}$.
Hence:

$\displaystyle
X=\\{t_{0},\dots,t_{k}\\}\cup\\{c:\\{s_{1},\dots,s_{a}\\}\mid\phi\mathbin{\bullet}u\\}\cup\\{c:X\mid\phi\mathbin{\bullet}u\\}$
$\displaystyle\Leftrightarrow
X=\\{t_{0},\dots,t_{k}\\}\cup\\{c:\\{s_{1},\dots,s_{a}\\}\mid\phi\mathbin{\bullet}u\\}\cup\\{c:N\mid\phi\mathbin{\bullet}u\\}$
$\displaystyle\Leftrightarrow
X=\\{t_{0},\dots,t_{k}\\}\cup\\{c:\\{s_{1},\dots,s_{a}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}$
$\displaystyle\Leftrightarrow
X=\\{t_{0},\dots,t_{k}\\}\cup\\{c:\textbf{{X}}[N/X]\mid\phi\mathbin{\bullet}u\\}$

In the following lemma, the case where $R\equiv X$ and $S\equiv X$ is covered
in [Dovier et al. (2000)]. Besides, given that the case where
$R\equiv\\{c:\textbf{{X}}\mid\phi\mathbin{\bullet}u\\}$ and $S\equiv X$ is
covered by the case where
$R\equiv\\{c:\textbf{{X}}\mid\phi\mathbin{\bullet}u\\}$ and
$S\equiv\\{d:X\mid\gamma\mathbin{\bullet}v\\}$, we will prove only the last
one. Indeed, given that $c\equiv u$, $d\equiv v$, we have
$\\{d:X\mid\gamma\mathbin{\bullet}v\\}\subseteq X$. Then, the last case covers
the second case when $\\{d:X\mid\gamma\mathbin{\bullet}v\\}=X$. In fact, in
this and the following lemma we will write
$\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}$ instead of X, where s
denotes zero or more elements; if s denotes zero elements then
$\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}$ is just $X$.

######  Lemma C.14 (Equivalence of rule ($=_{6}$)).

If $c\equiv u$ and $d\equiv v$:

$\displaystyle\begin{split}\forall X,&t_{0},\dots,t_{m},s_{0},\dots,s_{k}:\\\
&\begin{split}\\{t_{0},&\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}\\\
{}\Leftrightarrow{}&t_{0}=s_{j}\\\
&\quad{}\land\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{1}\\}=\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\land
t_{0}\notin N_{1}\\\
&\quad{}\land\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{2}\\}=\\{d:X\mid\gamma\mathbin{\bullet}v\\}\land
t_{0}\notin N_{2}\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N_{1}\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N_{2}\\}\\\
&{}\lor t_{0}=s_{j}\\\ &\quad{}\land
t_{0}\notin\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\land
t_{0}\notin\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}\\\
&{}\lor t_{0}=s_{j}\\\
&\quad{}\land\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}=\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\land
t_{0}\notin N\land t_{0}\notin\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}\\\
&{}\lor t_{0}=s_{j}\\\ &\quad{}\land
t_{0}\notin\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\land\\{s_{j}\mathbin{\scriptstyle\sqcup}N\\}=\\{d:X\mid\gamma\mathbin{\bullet}v\\}\land
s_{j}\notin N\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N\\}\\\
&{}\lor t_{0}=s_{j}\\\
&{}\quad\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}\\\
&{}\lor t_{0}=s_{j}\\\
&\quad{}\land\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}\\\
&{}\lor X=\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}\land\gamma(t_{0})\\\
&{}\quad\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\end{split}\end{split}$

######  Proof C.15.

$\implies)$
By H, $t_{0}$ must belong the the r.h.s. set. We will divide the proof in the
following cases each of which corresponds to one of the branches at the r.h.s.
Note that the disjunction of all the preconditions covers all possible cases.

  * •

$t_{0}\in\\{s_{0},\dots,s_{k}\\}$, then $t_{0}=s_{j}$, for some $j$

    * –

$t_{0}\notin\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\\}$

      * *

$s_{j}\notin\\{t_{1},\dots,t_{m}\\}$

        * ·

First branch:
$\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{1}\\}=\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\land\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{2}\\}=\\{d:X\mid\gamma\mathbin{\bullet}v\\}\land
t_{0}\notin N_{1}\land t_{0}\notin N_{2}$.

$\displaystyle\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N_{1}\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N_{2}\\}$
$\displaystyle\Leftrightarrow$ [by assumptions $t_{0}$ does not belong to
either set]
$\displaystyle\\{t_{0},t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N_{1}\\}=\\{s_{0},\dots,s_{j-1},t_{0},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N_{2}\\}$
$\displaystyle\Leftrightarrow$ [by absorption on the left, semantics of
$\mathbin{\scriptstyle\sqcup}$ and $s_{j}=t_{0}$]
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{1}\\}\\}=\\{s_{0},\dots,s_{j-1},s_{j},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{2}\\}\\}$
$\displaystyle\Leftrightarrow$ [by assumptions of this branch]
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

Since the last equality is H then the first equality holds.

        * ·

Second branch:
$t_{0}\notin\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\land
t_{0}\notin\\{d:X\mid\gamma\mathbin{\bullet}v\\}$

$\displaystyle\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle\Leftrightarrow$ [by assumptions $t_{0}$ does not belong to
either set]
$\displaystyle\\{t_{0},t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{j-1},t_{0},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle\Leftrightarrow$ [by $s_{j}=t_{0}$]
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{j-1},s_{j},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

Since the last equality is H then the first equality holds.

        * ·

Third branch:
$\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}=\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\land
t_{0}\notin\\{d:X\mid\gamma\mathbin{\bullet}v\\}\land t_{0}\notin N$.

$\displaystyle\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle\Leftrightarrow$ [by assumptions $t_{0}$ does not belong to
either set]
$\displaystyle\\{t_{0},t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N\\}=\\{s_{0},\dots,s_{j-1},t_{0},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle\Leftrightarrow$ [by absorption on the left, semantics of
$\mathbin{\scriptstyle\sqcup}$ and $s_{j}=t_{0}$]
$\displaystyle\\{t_{0},t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}\\}=\\{s_{0},\dots,s_{j-1},s_{j},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle\Leftrightarrow$ [by assumption of this branch]
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

Since the last equality is H then the first equality holds.

        * ·

Fourth branch:
$t_{0}\notin\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\land\\{s_{j}\mathbin{\scriptstyle\sqcup}N\\}=\\{d:X\mid\gamma\mathbin{\bullet}v\\}\land
s_{j}\notin N$.

$\displaystyle\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N\\}$
$\displaystyle\Leftrightarrow$ [by assumptions $t_{0}$ does not belong to
either set]
$\displaystyle\\{t_{0},t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{j-1},t_{0},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N\\}$
$\displaystyle\Leftrightarrow$ [by $s_{j}=t_{0}$]
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{j-1},s_{j},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N\\}\Leftrightarrow$
[by absorption on the left and semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{j-1},s_{j},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{s_{j}\mathbin{\scriptstyle\sqcup}N\\}\\}$
$\displaystyle\Leftrightarrow$ [by assumption of this branch]
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

Since the last equality is H then the first equality holds.

      * *

$s_{j}\in\\{t_{1},\dots,t_{m}\\}$

Now we consider the fifth branch.

Given that $s_{j}=t_{0}$ and that $s_{j}\in\\{t_{1},\dots,t_{m}\\}$, then
$t_{0}\in\\{t_{1},\dots,t_{m}\\}$.

$\displaystyle\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by $t_{0}\in\\{t_{1},\dots,t_{m}\\}$]
$\displaystyle=\\{t_{0},t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

    * –

$t_{0}\in\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\\}$

Now we consider the sixth branch.

Given that $s_{j}=t_{0}$ and that
$t_{0}\in\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\\}$, then
$s_{j}\in\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\\}$.

$\displaystyle\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by $s_{j}\in\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\\}$]
$\displaystyle=\\{s_{0},\dots
s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$ [by
H]
$\displaystyle=\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$

  * •

$t_{0}\notin\\{s_{0},\dots,s_{k}\\}$

Now we consider the last branch.

Given that $t_{0}\notin\\{s_{0},\dots,s_{k}\\}$, then necessarily
$t_{0}\in\\{d:X\mid\gamma\mathbin{\bullet}v\\}$, then $t_{0}\in X$ and
$\gamma(t_{0})$ holds. Now, the proof is divided in two cases.

    * –

$t_{0}\in\\{t_{1},\dots,t_{m}\\}\cup\\{\textbf{{s}}\\}\land\phi(t_{0})$

In this case we take $N=X$. Then
$\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}=\\{t_{0}\mathbin{\scriptstyle\sqcup}X\\}=X$,
where the last equality holds because $t_{0}\in X$. Now:

$\displaystyle\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{d:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by $t_{0}\in\\{t_{1},\dots,t_{m}\\}\cup\\{\textbf{{s}}\\}\land\phi(t_{0})$]
$\displaystyle=\\{t_{0},t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{d:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by $N=X$]
$\displaystyle=\\{t_{0},t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{d:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by $N=S$]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$

    * –

$t_{0}\notin\\{t_{1},\dots,t_{m}\\}\cup\\{\textbf{{s}}\\}\lor\lnot\phi(t_{0})$

In this case we take $N=X\setminus\\{t_{0}\\}$, then
$X=\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}$ because $t_{0}\in X$. Besides
$t_{0}\notin N$. Now we start from H.

$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle\Leftrightarrow$ [by
$X=\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}$]
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle\Leftrightarrow$ [by properties of
$\mathbin{\scriptstyle\sqcup}$ and intensional sets]
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}\cup\\{c:\\{t_{0}\\}\mid\phi\mathbin{\bullet}u\\}$
$\displaystyle\quad{}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\cup\\{d:\\{t_{0}\\}\mid\gamma\mathbin{\bullet}v\\}$
$\displaystyle\Leftrightarrow$ [by subtract $\\{t_{0}\\}$ on both sides]
$\displaystyle(\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}\cup\\{c:\\{t_{0}\\}\mid\phi\mathbin{\bullet}u\\})\setminus\\{t_{0}\\}$
$\displaystyle\quad{}=(\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\cup\\{d:\\{t_{0}\\}\mid\gamma\mathbin{\bullet}v\\})\setminus\\{t_{0}\\}$
$\displaystyle\Leftrightarrow$ [by $\setminus$ distributes over $\cup$]
$\displaystyle(\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}\setminus\\{t_{0}\\})\cup(\\{c:\\{t_{0}\\}\mid\phi\mathbin{\bullet}u\\}\setminus\\{t_{0}\\})$
$\displaystyle\quad{}=(\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\setminus\\{t_{0}\\})\cup(\\{d:\\{t_{0}\\}\mid\gamma\mathbin{\bullet}v\\}\setminus\\{t_{0}\\})$
$\displaystyle\Leftrightarrow$ [by
$t_{0}\notin\\{t_{1},\dots,t_{m}\\}\cup\\{\textbf{{s}}\\}$, $t_{0}\notin N$,
$t_{0}\notin\\{s_{0},\dots,s_{k}\\}$]
$\displaystyle\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$

$\Longleftarrow)$
We will consider each branch and will prove that the equality holds.

  * •

First branch.

$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{1}\\}\\}$
[by properties of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{t_{0},t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N_{1}\\}$
[by absorption on the left]
$\displaystyle=\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N_{1}\\}$
$\displaystyle=\\{t_{0}\\}\cup\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N_{1}\\}$
[by H]
$\displaystyle=\\{t_{0}\\}\cup\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N_{2}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{t_{0},s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N_{2}\\}$
[by absorption on the left]
$\displaystyle=\\{t_{0},s_{0},\dots,s_{j-1},t_{0},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N_{2}\\}$
[by H]
$\displaystyle=\\{s_{0},\dots,s_{j-1},s_{j},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{2}\\}\\}$
[by H]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

  * •

Second branch.

$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{t_{0}\\}\cup\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{t_{0}\\}\cup\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{s_{0},\dots,s_{j-1},t_{0},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by H]
$\displaystyle=\\{s_{0},\dots,s_{j-1},s_{j},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

  * •

Third branch.

$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}\\}$
[by properties of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{t_{0},t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N\\}$ [by
absorption on the left]
$\displaystyle=\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N\\}$
$\displaystyle=\\{t_{0}\\}\cup\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N\\}$
[by H]
$\displaystyle=\\{t_{0}\\}\cup\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{s_{0},\dots,s_{j-1},t_{0},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by H]
$\displaystyle=\\{s_{0},\dots,s_{j-1},s_{j},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by H]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

  * •

Fourth branch.

$\displaystyle\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by H]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{s_{j}\mathbin{\scriptstyle\sqcup}N\\}\\}$
[by properties of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{s_{j},s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N\\}$ [by
absorption on the left]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N\\}$ [by
semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{s_{j}\\}\cup\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N\\}$
[by H]
$\displaystyle=\\{s_{j}\\}\cup\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{s_{j},t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{t_{0},t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$

  * •

Fifth branch.

$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{t_{0}\\}\cup\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{t_{0}\\}\cup\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{t_{0},s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by H]
$\displaystyle=\\{s_{j},s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by absorption on the left]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

  * •

Sixth branch.

$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by absorption on the left]
$\displaystyle=\\{t_{0},t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{t_{0}\\}\cup\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{t_{0}\\}\cup\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{s_{0},\dots,s_{j-1},t_{0},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by H]
$\displaystyle=\\{s_{0},\dots,s_{j-1},s_{j},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

  * •

Seventh (last) branch.

$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$, property intensional sets]
$\displaystyle=\\{t_{0}\\}\cup\\{c:\\{t_{0}\\}\mid\phi\mathbin{\bullet}u\\}\cup\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{t_{0}\\}\cup\\{c:\\{t_{0}\\}\mid\phi\mathbin{\bullet}u\\}\cup\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by $\\{c:\\{t_{0}\\}\mid\phi\mathbin{\bullet}u\\}\subseteq\\{t_{0}\\}$]
$\displaystyle=\\{t_{0}\\}\cup\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{t_{0},s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{t_{0}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\\}$
[by H, semantics of $\mathbin{\scriptstyle\sqcup}$ and property of intensional
sets]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}\mid\gamma\mathbin{\bullet}v\\}\\}$
[by H]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

######  Lemma C.16 (Equivalence of rule ($=_{8}$)).

If $c\not\equiv u$ and $d\not\equiv v$:

$\displaystyle\begin{split}\forall X,&t_{0},\dots,t_{m},s_{0},\dots,s_{k}:\\\
&\begin{split}\\{t_{0},&\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}\\\
{}\Leftrightarrow{}&t_{0}=s_{j}\\\
&\quad{}\land\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{1}\\}=\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\land
t_{0}\notin N_{1}\\\
&\quad{}\land\\{t_{0}\mathbin{\scriptstyle\sqcup}N_{2}\\}=\\{d:X\mid\gamma\mathbin{\bullet}v\\}\land
t_{0}\notin N_{2}\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N_{1}\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N_{2}\\}\\\
&{}\lor t_{0}=s_{j}\\\ &\quad{}\land
t_{0}\notin\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\land
t_{0}\notin\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:X\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}\\\
&{}\lor t_{0}=s_{j}\\\
&\quad{}\land\\{t_{0}\mathbin{\scriptstyle\sqcup}N\\}=\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\land
t_{0}\notin N\land t_{0}\notin\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}N\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}\\\
&{}\lor t_{0}=s_{j}\\\ &\quad{}\land
t_{0}\notin\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\land\\{s_{j}\mathbin{\scriptstyle\sqcup}N\\}=\\{d:X\mid\gamma\mathbin{\bullet}v\\}\land
s_{j}\notin N\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}N\\}\\\
&{}\lor t_{0}=s_{j}\\\
&{}\quad\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}\\\
&{}\lor t_{0}=s_{j}\\\
&\quad{}\land\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{j-1},s_{j+1},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}\\\
&{}\lor X=\\{n\mathbin{\scriptstyle\sqcup}N\\}\land\gamma(n)\land
t_{0}=v(n)\land\phi(n)\land u(n)\notin\\{s_{0},\dots,s_{k}\\}\\\ &\quad{}\land
t_{0}=u(n)\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\\\
&{}\lor X=\\{n\mathbin{\scriptstyle\sqcup}N\\}\land\gamma(n)\land
t_{0}=v(n)\land\phi(n)\land u(n)=s_{j}\\\
&\quad{}\land\\{u(n),t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\\\
&{}\lor X=\\{n\mathbin{\scriptstyle\sqcup}N\\}\land\gamma(n)\land
t_{0}=v(n)\land\lnot\phi(n)\\\
&\quad{}\land\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\end{split}\end{split}$

######  Proof C.17.

The first six branches of this lemma are proved exactly as in the previous
lemma, in both directions, because those branches are equal in both lemmas.
Hence, we will prove only the last three branches, in both directions.
$\implies)$
In order to prove these branches we need to recall that $u$ and $v$ are
ordered pairs whose first component is the control variable and whose second
component is a $\mathcal{X}$-term. Then, from now on we will take
$u(x)=(x,f_{u}(x))$ for some term $f_{u}$ and $v(x)=(x,f_{v}(x))$, for some
term $f_{v}$.

Besides, all these branches are proved under the assumption as in the previous
lemma:

$t_{0}\notin\\{s_{0},\dots,s_{k}\\}$ (4)

The first step in the proof is that we can conclude that $t_{0}$ must belong
the the r.h.s. set, by H. Hence, due to (4), $t_{0}$ must belong to
$\\{d:X\mid\gamma\mathbin{\bullet}v\\}$, which means that there exists $n\in
X$, $\gamma(n)$ holds and $t_{0}=v(n)$. Observe that $t_{0}=v(n)$ means that
$t_{0}=(n,f_{v}(n))$.

Now, note that the following conditions of the branches under consideration:

$\displaystyle\phi(n)\land u(n)\notin\\{s_{0},\dots,s_{k}\\}$
$\displaystyle\phi(n)\land u(n)=s_{j}$ $\displaystyle\lnot\phi(n)$

are mutually exclusive. Since $n\in X$ then in the first two cases we have
$u(n)\in\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}$,
which implies that $u(n)$ belongs to the l.h.s. set. If $u(n)$ belongs to the
l.h.s. set of H, then it must belong to the r.h.s. of H. Then, in the first
case we assume $u(n)$ belongs to $\\{d:X\mid\gamma\mathbin{\bullet}v\\}$ while
in the second we assume is one of the $s_{i}$.

Hence, in order to prove each branch we will assume the corresponding
condition and we will prove the remaining predicates of the conclusion.

  * •

Assume $\phi(n)\land u(n)\notin\\{s_{0},\dots,s_{k}\\}$.

Will we prove that $t_{0}=u(n)$ by contradiction. We know that
$u(n)\in\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}$.
So:

$\displaystyle(n,f_{u}(n))\in\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\land
t_{0}\neq(n,f_{u}(n))$ [by assumption of this branch]
$\displaystyle\implies(n,f_{u}(n))\in\\{d:X\mid\gamma\mathbin{\bullet}v\\}\land
f_{v}(n)\neq f_{u}(n)$ [by semant. intensional sets, def. of $v$]
$\displaystyle\implies\gamma(n)\land(n,f_{u}(n))=(n,f_{v}(n))\land
f_{v}(n)\neq f_{u}(n)$ [by drop $\gamma(n)$ and equality of pairs]
$\displaystyle\implies f_{u}(n)=f_{v}(n)\land f_{v}(n)\neq f_{u}(n)$

which is clearly a contradiction. Hence, $t_{0}=u(n)$.

Now we will prove that
$\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:N\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$,
by dividing the proof in two cases.

    * –

$t_{0}\in\\{t_{1},\dots,t_{m}\\}\cup\\{c:\textbf{{s}}\mid\phi\mathbin{\bullet}u\\}$

In this case we take $N=X$. Then
$\\{n\mathbin{\scriptstyle\sqcup}N\\}=\\{n\mathbin{\scriptstyle\sqcup}X\\}=X$,
where the last equality holds because $n\in X$.

      * *

$t_{0}\in\\{t_{1},\dots,t_{m}\\}$

$\displaystyle\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by $N=X$]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by H]
$\displaystyle=\\{t_{0},t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by $t_{0}\in\\{t_{1},\dots,t_{m}\\}$, left absorption]
$\displaystyle=\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by $X=N$]
$\displaystyle=\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}$

      * *

$t_{0}\in\\{c:\\{\textbf{{s}}\\}\mid\phi\mathbin{\bullet}u\\}$. Note that in
this case
$\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}=\\{t_{0}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$.

$\displaystyle\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by $N=X$]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
[by H]
$\displaystyle=\\{t_{0},t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{t_{0}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}\\}$
[by $t_{0}\in\\{c:\\{\textbf{{s}}\\}\mid\phi\mathbin{\bullet}u\\}$]
$\displaystyle=\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by $X=N$]
$\displaystyle=\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}$

    * –

$t_{0}\notin\\{t_{1},\dots,t_{m}\\}\cup\\{c:\textbf{{s}}\mid\phi\mathbin{\bullet}u\\}$

In this case we take $N=X\setminus\\{n\\}$, then
$X=\\{n\mathbin{\scriptstyle\sqcup}N\\}$ because $n\in X$. Besides $n\notin
N$. Now we start from H.

$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle\Leftrightarrow$ [by $X=\\{n\mathbin{\scriptstyle\sqcup}N\\}$]
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}\\{n\mathbin{\scriptstyle\sqcup}N\\}\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:\\{n\mathbin{\scriptstyle\sqcup}N\\}\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle\Leftrightarrow$ [by properties of
$\mathbin{\scriptstyle\sqcup}$ and intensional sets]
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}\cup\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\}$
$\displaystyle\quad{}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\cup\\{d:\\{n\\}\mid\gamma\mathbin{\bullet}v\\}$
$\displaystyle\Leftrightarrow$ [by subtract $\\{t_{0}\\}$ at both sides]
$\displaystyle(\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}\cup\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\})\setminus\\{t_{0}\\}$
$\displaystyle\quad{}=(\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\cup\\{d:\\{n\\}\mid\gamma\mathbin{\bullet}v\\})\setminus\\{t_{0}\\}$
$\displaystyle\Leftrightarrow$ [by $\setminus$ distributes over $\cup$]
$\displaystyle(\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}\setminus\\{t_{0}\\})\cup(\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\}\setminus\\{t_{0}\\})$
$\displaystyle\quad{}=(\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\setminus\\{t_{0}\\})\cup(\\{d:\\{n\\}\mid\gamma\mathbin{\bullet}v\\}\setminus\\{t_{0}\\})$
$\displaystyle\Leftrightarrow$ [by $(\dagger)$]
$\displaystyle\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$

The justification of $(\dagger)$ is the following:

    1. 1.

Note that $\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\}=\\{u(n)\\}=\\{t_{0}\\}$
[by assumption of this branch and because in this branch $u(n)=t_{0}$], then
$\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\}\setminus\\{t_{0}\\}=\emptyset$.

    2. 2.

$\\{d:\\{n\\}\mid\gamma\mathbin{\bullet}v\\}=\\{t_{0}\\}$ [by $\gamma(n)\land
t_{0}=v(n)$], then
$\\{d:\\{n\\}\mid\gamma\mathbin{\bullet}v\\}\setminus\\{t_{0}\\}=\emptyset$.

    3. 3.

$t_{0}\notin\\{c:N\mid\phi\mathbin{\bullet}u\\}$ because if it does then there
exists $n^{\prime}\in N$ such that $\phi(n^{\prime})$ holds and
$t_{0}=u(n^{\prime})$. But, $t_{0}=u(n^{\prime})\Leftrightarrow
t_{0}=(n^{\prime},f_{u}(n^{\prime}))$. On the other hand $t_{0}=(n,f_{v}(n))$
and so $(n,f_{v}(n))=(n^{\prime},f_{u}(n^{\prime}))$ which implies that
$n=n^{\prime}$. But this is impossible because we have $n^{\prime}\in N$ and
$n\notin N$.

    4. 4.

$\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}\setminus\\{t_{0}\\}=\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by assumption:
$t_{0}\notin\\{t_{1},\dots,t_{m}\\}\cup\\{c:\textbf{{s}}\mid\phi\mathbin{\bullet}u\\}$;
and by $t_{0}\notin\\{c:N\mid\phi\mathbin{\bullet}u\\}$].

    5. 5.

$\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\setminus\\{t_{0}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by $t_{0}\notin\\{s_{0},\dots,s_{k}\\}$ and $n\notin N$].

  * •

Assume $\phi(n)\land u(n)=s_{j}$.

We have to prove that
$\\{u(n),t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$.
We proceed as with the previous branch. In fact, the first case is identical
(note that there we used assumptions that are also available in this branch).
In the second case, we take the same value for $N$ and start from H as in the
previous branch.

$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle\Leftrightarrow$ [by $X=\\{n\mathbin{\scriptstyle\sqcup}N\\}$]
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}},n\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:\\{n\mathbin{\scriptstyle\sqcup}N\\}\mid\gamma\mathbin{\bullet}v\\}\\}$
$\displaystyle\Leftrightarrow$ [by properties of
$\mathbin{\scriptstyle\sqcup}$ and intensional sets and $\phi(n)$ holds]
$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{u(n)\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}\\}$
$\displaystyle\quad{}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\cup\\{d:\\{n\\}\mid\gamma\mathbin{\bullet}v\\}$
$\displaystyle\Leftrightarrow$ [by semantics of
$\mathbin{\scriptstyle\sqcup}$]
$\displaystyle\\{u(n),t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\cup\\{d:\\{n\\}\mid\gamma\mathbin{\bullet}v\\}$
$\displaystyle\Leftrightarrow$ [by subtract $\\{t_{0}\\}$ at both sides]
$\displaystyle\\{u(n),t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}\setminus\\{t_{0}\\}$
$\displaystyle\quad{}=(\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\cup\\{d:\\{n\\}\mid\gamma\mathbin{\bullet}v\\})\setminus\\{t_{0}\\}$
$\displaystyle\Leftrightarrow$ [by $\setminus$ distributes over $\cup$]
$\displaystyle\\{u(n),t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}\setminus\\{t_{0}\\}$
$\displaystyle\quad{}=(\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\setminus\\{t_{0}\\})\cup(\\{d:\\{n\\}\mid\gamma\mathbin{\bullet}v\\}\setminus\\{t_{0}\\})$
$\displaystyle\Leftrightarrow$ [by $(\dagger)$]
$\displaystyle\\{u(n),t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$

The justification of $(\dagger)$ is the following:

    1. 1.

$\\{d:\\{n\\}\mid\gamma\mathbin{\bullet}v\\}=\\{t_{0}\\}$ [by $\gamma(n)\land
t_{0}=v(n)$], then
$\\{d:\\{n\\}\mid\gamma\mathbin{\bullet}v\\}\setminus\\{t_{0}\\}=\emptyset$.

    2. 2.

$t_{0}\neq u(n)$ because if not then $t_{0}=s_{j}$ which is in contraction
with (4).

    3. 3.

$t_{0}\notin\\{c:N\mid\phi\mathbin{\bullet}u\\}$ because if it belongs then
there exists $n^{\prime}\in N$ such that $\phi(n^{\prime})$ holds and
$t_{0}=u(n^{\prime})$. But, $t_{0}=u(n^{\prime})\Leftrightarrow
t_{0}=(n^{\prime},f_{u}(n^{\prime}))$. On the other hand $t_{0}=(n,f_{v}(n))$
and so $(n,f_{v}(n))=(n^{\prime},f_{u}(n^{\prime}))$ which implies that
$n=n^{\prime}$. But this is impossible because we have $n^{\prime}\in N$ and
$n\notin N$.

    4. 4.

$\\{u(n),t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}\setminus\\{t_{0}\\}=\\{u(n),t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by assumption:
$t_{0}\notin\\{t_{1},\dots,t_{m}\\}\cup\\{c:\textbf{{s}}\mid\phi\mathbin{\bullet}u\\}$;
by $t_{0}\neq u(n)$; and by $t_{0}\notin\\{c:N\mid\phi\mathbin{\bullet}u\\}$].

    5. 5.

$\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\setminus\\{t_{0}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by $t_{0}\notin\\{s_{0},\dots,s_{k}\\}$ and $n\notin N$].

  * •

Assume $\lnot\phi(n)$.

We have to prove that
$\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$.We
proceed as in the first branch considered in this lemma. In fact, the first
case is identical (note that there we used assumptions that are also available
in this branch). In the second case, we take the same value for $N$ and
proceed in the same way. The only difference is in the first item of the
justification of $(\dagger)$ because now we have
$\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\}=\emptyset$ because $\lnot\phi(n)$.

$\Longleftarrow)$
We will consider only the last three branches and will prove that the equality
holds.

Note that when $\phi(n)$ holds then
$\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\}=\\{u(n)\\}$; and when $\phi(n)$
does not hold then $\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\}=\emptyset$.

  * •

First branch.

$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}\\{n\mathbin{\scriptstyle\sqcup}N\\}\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$; property of intensional sets]
$\displaystyle=\\{t_{0}\\}\cup\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\}\cup\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{t_{0}\\}\cup\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\}\cup\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by $\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\}=\\{t_{0}\\}$]
$\displaystyle=\\{t_{0}\\}\cup\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{t_{0},s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{t_{0}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\\}$
[by H, semantics of $\mathbin{\scriptstyle\sqcup}$ and property of intensional
sets]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:\\{n\mathbin{\scriptstyle\sqcup}N\\}\mid\gamma\mathbin{\bullet}v\\}\\}$
[by H]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

  * •

Second branch.

$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$ and
$X=\\{n\mathbin{\scriptstyle\sqcup}N\\}$]
$\displaystyle=\\{t_{0}\\}\cup\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}},n\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by $\phi(n)$ holds, properties of intensional sets]
$\displaystyle=\\{t_{0}\\}\cup\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{u(n)\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{t_{0}\\}\cup\\{u(n),t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{t_{0}\\}\cup\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{t_{0},s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{t_{0}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\\}$
[by H, semantics of $\mathbin{\scriptstyle\sqcup}$ and property of intensional
sets]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:\\{n\mathbin{\scriptstyle\sqcup}N\\}\mid\gamma\mathbin{\bullet}v\\}\\}$
[by H]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

  * •

Third branch.

$\displaystyle\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}X\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{t_{0},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}\\{n\mathbin{\scriptstyle\sqcup}N\\}\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$; property of intensional sets]
$\displaystyle=\\{t_{0}\\}\cup\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\}\cup\\{t_{1},\dots,t_{m}\mathbin{\scriptstyle\sqcup}\\{c:\\{\textbf{{s}}\mathbin{\scriptstyle\sqcup}N\\}\mid\phi\mathbin{\bullet}u\\}\\}$
[by H]
$\displaystyle=\\{t_{0}\\}\cup\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\}\cup\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by $\\{c:\\{n\\}\mid\phi\mathbin{\bullet}u\\}=\emptyset$ by $\lnot\phi(n)$]
$\displaystyle=\\{t_{0}\\}\cup\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{t_{0},s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{t_{0}\mathbin{\scriptstyle\sqcup}\\{d:N\mid\gamma\mathbin{\bullet}v\\}\\}\\}$
[by H, semantics of $\mathbin{\scriptstyle\sqcup}$ and property of intensional
sets]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:\\{n\mathbin{\scriptstyle\sqcup}N\\}\mid\gamma\mathbin{\bullet}v\\}\\}$
[by H]
$\displaystyle=\\{s_{0},\dots,s_{k}\mathbin{\scriptstyle\sqcup}\\{d:X\mid\gamma\mathbin{\bullet}v\\}\\}$

The equivalence of rule ($=_{9}$) has been proved previously for any finite
set (extensional or intensional) [Dovier et al. (2000)].

######  Lemma C.18 (Equivalence of rule ($=_{10}$)).

We consider only the following case because the others covered by this rule
are similar.

$\displaystyle\begin{split}\forall d,&D:\\\
&\begin{split}&\\{x:\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}=\emptyset\\\
&\Leftrightarrow\lnot\phi(d)\land\\{x:D\mid\phi\mathbin{\bullet}u\\}=\emptyset\end{split}\end{split}$

######  Proof C.19.

Taking any $d$ and $D$ we have:

$\displaystyle\\{x:\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}=\emptyset$
[by Prop. C.10]
$\displaystyle\Leftrightarrow\\{u(d):\phi(d)\\}\cup\\{u(x):x\in
D\land\phi(x)\\}=\emptyset$
$\displaystyle\Leftrightarrow\\{u(d):\phi(d)\\}=\emptyset\land\\{u(x):x\in
D\land\phi(x)\\}=\emptyset$
$\displaystyle\Leftrightarrow\lnot\phi(d)\land\\{x:D\mid\phi\mathbin{\bullet}u\\}=\emptyset$

######  Lemma C.20 (Equivalence of rule ($=_{11}$)).

$\displaystyle\begin{split}\forall d,&D,B:\\\
&\begin{split}&\\{x:\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}=B\\\
&\begin{split}\Leftrightarrow&\phi(d)\land\\{u(d)\mathbin{\scriptstyle\sqcup}\\{x:D\mid\phi\mathbin{\bullet}u\\}\\}=B\\\
&\lor\lnot\phi(d)\land\\{x:D\mid\phi\mathbin{\bullet}u\\}=B\end{split}\end{split}\end{split}$

######  Proof C.21.

Taking any $d$, $D$ and $B$ we have:

$\displaystyle\\{x:\\{d\mathbin{\scriptstyle\sqcup}D\\}\mid\phi\mathbin{\bullet}u\\}=B$
[by Prop. C.10]
$\displaystyle\Leftrightarrow\\{u(d):\phi(d)\\}\cup\\{u(x):x\in
D\land\phi(x)\\}=B$
$\displaystyle\Leftrightarrow\\{u(d):\phi(d)\\}\cup\\{x:D\mid\phi\mathbin{\bullet}u\\}=B$

Now assume $\phi(d)$, then:

$\displaystyle\\{u(d):\phi(d)\\}\cup\\{x:D\mid\phi\mathbin{\bullet}u\\}=B$
$\displaystyle\Leftrightarrow\\{u(d)\\}\cup\\{x:D\mid\phi\mathbin{\bullet}u\\}=B$
[by semantics of $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle\Leftrightarrow\\{u(d)\mathbin{\scriptstyle\sqcup}\\{x:D\mid\phi\mathbin{\bullet}u\\}\\}=B$

Now assume $\lnot\phi(d)$, then:

$\displaystyle\\{u(d):\phi(d)\\}\cup\\{x:D\mid\phi\mathbin{\bullet}u\\}=B$
$\displaystyle\emptyset\cup\\{x:D\mid\phi\mathbin{\bullet}u\\}=B$
$\displaystyle\\{x:D\mid\phi\mathbin{\bullet}u\\}=B$

which finishes the proof.

######  Remark C.22.

Note that in Theorem C.20 when $B$ is:

  * •

An extensional set of the form $\\{y\mathbin{\scriptstyle\sqcup}A\\}$, then
the equality in the first disjunct becomes an equality between two extensional
sets:

$\\{u(d)\mathbin{\scriptstyle\sqcup}\\{x:D\mid\phi\mathbin{\bullet}u\\}\\}=\\{y\mathbin{\scriptstyle\sqcup}A\\}$

which is solved by the rules described in [Dovier et al. (2000)]. In turn, the
equality in the second disjunct becomes an equality between a RIS and an
extensional set:

$\\{x:D\mid\phi\mathbin{\bullet}u\\}=\\{y\mathbin{\scriptstyle\sqcup}A\\}$

This equality is managed by either rule ($=_{11}$) itself (if $D$ is not a
variable) or by rule ($=_{14}$) (if $D$ is a variable).

  * •

A non-variable RIS of the form
$\\{x:\\{e\mathbin{\scriptstyle\sqcup}E\\}\mid\gamma\mathbin{\bullet}v\\}$,
then the equality in the first disjunct becomes an equality between an
extensional set and a non-variable RIS:

$\\{u(d)\mathbin{\scriptstyle\sqcup}\\{x:D\mid\phi\mathbin{\bullet}u\\}\\}=\\{x:\\{e\mathbin{\scriptstyle\sqcup}E\\}\mid\gamma\mathbin{\bullet}v\\}$

which is managed again by rule ($=_{11}$). In turn, the equality in the second
disjunct becomes an equality between a RIS and a non-variable RIS: