pith. sign in

arxiv: 2105.03005 · v2 · submitted 2021-05-06 · 💻 cs.LO · cs.SE

A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals

Maximiliano Cristi\'a , Gianfranco Rossi This is my paper

Pith reviewed 2026-05-24 12:46 UTC · model grok-4.3

classification 💻 cs.LO cs.SE
keywords decision procedurefinite setscardinality constraintsinteger intervalsquantifier-free logicset minimum maximumautomated reasoninginvariance lemmas
0
0 comments X

The pith

A decision procedure extends to finite sets with integer intervals whose bounds can involve unbounded variables.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper extends a decision procedure for the Boolean algebra of finite sets with cardinality constraints to handle finite integer intervals. Interval limits are allowed to be integer linear terms that include unbounded variables. This change makes it possible to represent operators such as the minimum and maximum of a set inside quantifier-free formulas. The resulting procedure therefore decides a wider class of formulas than before. It is implemented inside the {log} tool and shown to discharge all invariance lemmas in an elevator algorithm case study.

Core claim

The authors extend the decision procedure for L_|.| to L_[ ] by adding support for set terms that denote finite integer intervals whose limits are integer linear terms possibly containing unbounded variables. The extension keeps the logic quantifier-free while allowing direct use of set minimum and maximum, and the procedure is shown to remain decidable and to succeed on the elevator invariance lemmas.

What carries the argument

The decision procedure for L_[ ] obtained by extending the base procedure for L_|.| to decide formulas containing finite integer interval terms with unbounded variable bounds.

If this is right

  • Quantifier-free formulas involving minimum and maximum of sets become decidable.
  • The {log} tool can automatically discharge invariance lemmas that mention intervals.
  • Set-based specifications that rely on bounded integer ranges can be verified without introducing quantifiers.
  • The same decision procedure applies when interval endpoints depend on free variables.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same extension technique might be reusable for other bounded numeric set operators beyond min and max.
  • Verification of algorithms that maintain ordered sets or ranges could be automated more readily.
  • The approach opens a route to combine the procedure with other SMT back-ends that already handle linear arithmetic.

Load-bearing premise

The extension of the base decision procedure to interval terms with unbounded variables preserves decidability and is correctly implemented.

What would settle it

A concrete formula using min or max of a set that the implemented procedure classifies as satisfiable but is in fact unsatisfiable, or vice versa.

Figures

Figures reproduced from arXiv: 2105.03005 by Gianfranco Rossi, Maximiliano Cristi\'a.

Figure 1
Figure 1. Figure 1: Some key rewrite rules inherited from CLP( [PITH_FULL_IMAGE:figures/full_fig_p013_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Rewrite rules for =-constraints involving interv [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Rewrite rules for ∈-constraints involving intervals [k, m] k ∅ −→ true (18) If A is a set variable or an extensional set: (19) [k, m] k A −→ m < k ∨ (k ≤ m ∧ N˙ ⊆ [k, m] ∧ size(N˙ , m − k + 1) ∧ N˙ k A) [k, m] k [i, j] −→ m < k ∨ j < i ∨ (k ≤ m ∧ i ≤ j ∧ (m < i ∨ j < k)) (20) [k, m] 6k A −→ n˙ ∈ [k, m] ∧ n˙ ∈ A (21) [PITH_FULL_IMAGE:figures/full_fig_p015_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Rewrite rules for k-constraints involving intervals 4.4. Rules for ∈-constraints The rewrite rules for ∈-constraints are listed in [PITH_FULL_IMAGE:figures/full_fig_p015_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Rewrite rules for un-constraints involving intervals size([k, m], p) −→ (m < k ∧ p = 0) ∨ (k ≤ m ∧ p = m − k + 1) (28) nsize([k, m], p) −→ (m < k ∧ p 6= 0) ∨ (k ≤ m ∧ p 6= m − k + 1) (29) [PITH_FULL_IMAGE:figures/full_fig_p017_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Rewrite rules for size-constraints involving intervals 17 [PITH_FULL_IMAGE:figures/full_fig_p017_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Rule scheme for 6=-constraint elimination rules Example 4 (Unsatisfiable formula returned by STEPS[ ]). The [ ]-formula: un(A, B, C) ∧ un(A, B, D) ∧ C 6= D (30) cannot be further rewritten by any of the rewrite rules of STEPS[ ]. Nevertheless, it is clearly unsatisfiable. In order to guarantee that SAT [ ] returns either false or satisfiable formulas (see Theorem 3), we still need to remove all inequalitie… view at source ↗
Figure 8
Figure 8. Figure 8: A rewrite rule for diff -constraints involving intervals Example 12. When the last alternative of rule (26) is applied to the following formula: un(int(K,M),int(I,J),A) & un(int(I,J),int(K,M),B) & A neq B the result is a formula such as: un(W,X,A) & un(Y,Z,B) & A neq B & K =< M & I =< J & subset(W,int(K,M)) & size(W,P1) & P1 is M - K + 1 & subset(X,int(I,J)) & size(X,P2) & P2 is J - I + 1 & subset(Y,int(I,… view at source ↗
Figure 9
Figure 9. Figure 9: A typical state invariant 8.3. Automated proofs Being able to run simulations on the code is good to have a first idea on how the system works, but this cannot guarantee the program is correct. If we need stronger evidence on the correctness of the program we should try to prove some properties true of it. In this section we show that we can use the same representation of the control software and the same … view at source ↗
Figure 10
Figure 10. Figure 10: A typical invariance lemma passFloor(MinF,MaxF,Lift,Lift_) & Lift_ = [F_,Nf_,D_,C_,Di_,R_] & Di_ = up & C_ = moving & F_ >= Nf_. In this case {log} returns a counterexample stating that: F_ = Nf, Nf_ = Nf, Nf is F + 1 That is, initially, F < Nf but passFloor increments F in one and ‘assigns’ this value to F_ while leaving Nf unchanged. Then, after passFloor has executed the current floor can be equal to t… view at source ↗
read the original abstract

In this paper we extend a decision procedure for the Boolean algebra of finite sets with cardinality constraints ($\mathcal{L}_{\lvert\cdot\rvert}$) to a decision procedure for $\mathcal{L}_{\lvert\cdot\rvert}$ extended with set terms denoting finite integer intervals ($\mathcal{L}_{[\,]}$). In $\mathcal{L}_{[\,]}$ interval limits can be integer linear terms including \emph{unbounded variables}. These intervals are a useful extension because they allow to express non-trivial set operators such as the minimum and maximum of a set, still in a quantifier-free logic. Hence, by providing a decision procedure for $\mathcal{L}_{[\,]}$ it is possible to automatically reason about a new class of quantifier-free formulas. The decision procedure is implemented as part of the $\{log\}$ tool. The paper includes a case study based on the elevator algorithm showing that $\{log\}$ can automatically discharge all its invariance lemmas some of which involve intervals.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper extends an existing decision procedure for the theory of finite sets with cardinality constraints (denoted L_|.|) to a new theory L_[ ] that incorporates finite integer interval terms. In L_[ ], the interval bounds may be integer linear expressions over unbounded variables. This allows quantifier-free expression of operators such as set minimum and maximum. The extended procedure is implemented in the {log} tool and is shown, via a case study on the elevator algorithm, to discharge all invariance lemmas, some of which involve intervals.

Significance. If the extension preserves decidability and soundness, the work enlarges the class of quantifier-free set formulas that can be decided automatically, directly supporting verification tasks that require extremal values or interval reasoning. The concrete elevator case study supplies a falsifiable demonstration of utility, and the {log} implementation supplies a reproducible artifact.

minor comments (2)
  1. [Abstract] Abstract: the claim that the procedure 'remains decidable' would be strengthened by a one-sentence pointer to the key reduction or termination argument used in the extension.
  2. The case-study section would benefit from an explicit statement of which formulas involve unbounded interval bounds and how many such formulas were discharged.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, significance assessment, and recommendation of minor revision. No major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper presents an extension of a previously published decision procedure for L_|.| to the new theory L_[ ] that incorporates finite integer interval terms whose bounds may involve unbounded integer variables. The base procedure is treated as an external, independently developed component; the extension is described as preserving decidability through explicit algorithmic modifications, with correctness supported by implementation in {log} and empirical validation on the elevator invariance lemmas. No step reduces a claimed prediction or uniqueness result to a fitted parameter, self-citation chain, or definitional renaming; the central claim remains an independent algorithmic construction whose soundness is not forced by the inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the correctness of the base L_|.| decision procedure together with standard properties of sets and integer arithmetic; no new free parameters or invented entities are introduced.

axioms (2)
  • domain assumption Decidability and correctness of the base theory L_|.|
    The extension presupposes that the prior procedure is sound.
  • standard math Standard axioms of Boolean algebra, finite sets, and linear integer arithmetic
    Invoked throughout the construction of the new decision procedure.

pith-pipeline@v0.9.0 · 5694 in / 1229 out tokens · 72779 ms · 2026-05-24T12:46:32.904077+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

49 extracted references · 49 canonical work pages

  1. [1]

    Abrial, The B-book: Assigning Programs to Meanings, Cambr idge University Press, New York, NY, USA, 1996

    J.-R. Abrial, The B-book: Assigning Programs to Meanings, Cambr idge University Press, New York, NY, USA, 1996

    work page 1996

  2. [2]

    Leuschel, M

    M. Leuschel, M. Butler, ProB: A model checker for B, in: A. Keijir o, S. Gnesi, D. Mandrioli (Eds.), FME, Vol. 2805 of Lecture Notes in Com - puter Science, Springer-Verlag, 2003, pp. 855–874

    work page 2003

  3. [3]

    URL http://www.atelierb.eu/

    Clearsy, Aterlier B home page. URL http://www.atelierb.eu/

    work page

  4. [4]

    C. G. Zarba, Combining sets with integers, in: A. Armando (Ed.), F ron- tiers of Combining Systems, 4th International Workshop, FroCoS 2002, Santa Margherita Ligure, Italy, April 8-10, 2002, Proceedings, V ol. 2309 of Lecture Notes in Computer Science, Springer, 2002, pp. 103–1 16. doi:10.1007/3-540-45988-X 9. URL https://doi.org/10.1007/3-540-45988-X\_9

    work page doi:10.1007/3-540-45988-x 2002

  5. [5]

    Kuncak, H

    V. Kuncak, H. H. Nguyen, M. C. Rinard, Deciding Boolean algebra with Presburger arithmetic, J. Autom. Reason. 36 (3) (2006) 213 –239. doi:10.1007/s10817-006-9042-1

    work page doi:10.1007/s10817-006-9042-1 2006

  6. [6]

    Bansal, C

    K. Bansal, C. W. Barrett, A. Reynolds, C. Tinelli, Reasoning with fin ite sets and cardinality constraints in SMT, Log. Methods Comput. Sci. 14 (4). doi:10.23638/LMCS-14(4:12)2018. 36

    work page doi:10.23638/lmcs-14(4:12)2018 2018

  7. [7]

    Cristi´ a, G

    M. Cristi´ a, G. Rossi, Integrating cardinality constraints into co nstraint logic programming with sets, CoRR abs/2102.05422, under consider ation in Theory Pract. Log. Program. arXiv:2102.05422. URL https://arxiv.org/abs/2102.05422

    work page arXiv

  8. [8]

    A. R. Bradley, Z. Manna, H. B. Sipma, What’s decidable about ar- rays?, in: E. A. Emerson, K. S. Namjoshi (Eds.), Verification, Mod el Checking, and Abstract Interpretation, 7th International Con ference, VM- CAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceeding s, Vol. 3855 of Lecture Notes in Computer Science, Springer, 2006, pp. 4 27–442. doi:10...

    work page doi:10.1007/11609773 2006

  9. [9]

    Z. Su, D. A. Wagner, A class of polynomially solvable range constra ints for interval analysis without widenings, Theor. Comput. Sci. 345 (1) (2 005) 122–138. doi:10.1016/j.tcs.2005.07.035. URL https://doi.org/10.1016/j.tcs.2005.07.035

    work page doi:10.1016/j.tcs.2005.07.035 2005

  10. [10]

    Dovier, C

    A. Dovier, C. Piazza, E. Pontelli, G. Rossi, Sets and constraint lo gic pro- gramming, ACM Trans. Program. Lang. Syst. 22 (5) (2000) 861–9 31

    work page 2000

  11. [11]

    Cristi´ a, G

    M. Cristi´ a, G. Rossi, Solving quantifier-free first-order cons traints over fi- nite sets and binary relations, J. Autom. Reasoning 64 (2) (2020) 2 95–330. doi:10.1007/s10817-019-09520-4. URL https://doi.org/10.1007/s10817-019-09520-4

    work page doi:10.1007/s10817-019-09520-4 2020

  12. [12]

    Cristi´ a, G

    M. Cristi´ a, G. Rossi, A decision procedure for restricted inten sional sets, in: L. de Moura (Ed.), Automated Deduction - CADE 26 - 26th Intern a- tional Conference on Automated Deduction, Gothenburg, Swede n, August 6-11, 2017, Proceedings, Vol. 10395 of Lecture Notes in Compute r Science, Springer, 2017, pp. 185–201. doi:10.1007/978-3-319-63046-5 12. ...

    work page doi:10.1007/978-3-319-63046-5 2017

  13. [13]

    Cristi´ a, G

    M. Cristi´ a, G. Rossi, Automated reasoning with restricted inte nsional sets, Journal of Automated Reasoningdoi:10.1007/s10817-021-09589 -w. URL https://doi.org/10.1007/s10817-021-09589-w

    work page doi:10.1007/s10817-021-09589

  14. [14]

    Dovier, E

    A. Dovier, E. G. Omodeo, E. Pontelli, G. Rossi, A language for pro - gramming in logic with finite sets, J. Log. Program. 28 (1) (1996) 1–4 4. doi:10.1016/0743-1066(95)00147-6. URL http://dx.doi.org/10.1016/0743-1066(95)00147-6

    work page doi:10.1016/0743-1066(95)00147-6 1996

  15. [15]

    Rossi, {log}, http://people.dmi.unipr.it/gianfranco.rossi/ setlog.Home.html (2021)

    G. Rossi, {log}, http://people.dmi.unipr.it/gianfranco.rossi/ setlog.Home.html (2021). URL \url{http://people.dmi.unipr.it/gianfranco.rossi/setlog. Home.html}

    work page 2021

  16. [16]

    Cristi´ a, G

    M. Cristi´ a, G. Rossi, Automated proof of Bell-LaPadula security properties, J. Autom. Reason. 65 (4) (2021) 463–478. doi:10.1007/s10817-0 20-09577-6. URL https://doi.org/10.1007/s10817-020-09577-6 37

    work page doi:10.1007/s10817-0 2021

  17. [17]

    Cristi´ a, G

    M. Cristi´ a, G. Rossi, An automatically verified prototype of the Tokeneer ID station specification, CoRR abs/2009.00999. arXiv:2009.00999. URL https://arxiv.org/abs/2009.00999

    work page arXiv 2009

  18. [18]

    Dovier, E

    A. Dovier, E. Pontelli, G. Rossi, Set unification, Theory Pract. L og. Pro- gram. 6 (6) (2006) 645–701. doi:10.1017/S1471068406002730

    work page doi:10.1017/s1471068406002730 2006

  19. [19]

    Eriksson, M

    J. Eriksson, M. Parsa, A DSL for integer range reasoning: Par tition, in- terval and mapping diagrams, in: E. Komendantskaya, Y. A. Liu (Ed s.), Practical Aspects of Declarative Languages - 22nd Internationa l Sympo- sium, PADL 2020, New Orleans, LA, USA, January 20-21, 2020, Pro ceed- ings, Vol. 12007 of Lecture Notes in Computer Science, Springer, 2 020...

    work page doi:10.1007/978-3-030-39197-3 2020

  20. [20]

    Holzbaur, OF AI CLP(Q,R) manual, Tech

    C. Holzbaur, OF AI CLP(Q,R) manual, Tech. rep., edition 1.3.3. Tec hnical Report TR-95-09, Austrian Research Institute for Artificial Int elligence (1995). URL http://www.ofai.at/cgi-bin/tr-online?number+95-09

    work page 1995

  21. [21]

    J. M. Howe, A. King, A pearl on SAT and SMT solving in Prolog, Theo r. Comput. Sci. 435 (2012) 43–55. doi:10.1016/j.tcs.2012.02.024. URL https://doi.org/10.1016/j.tcs.2012.02.024

    work page doi:10.1016/j.tcs.2012.02.024 2012

  22. [22]

    Cristi´ a, G

    M. Cristi´ a, G. Rossi, Rewrite rules for a solver for sets, binary relations and partial functions, Tech. rep., http://people.dmi.unipr.it/gianfranco. rossi/SETLOG/calculus.pdf (2019)

    work page 2019

  23. [23]

    Cristi´ a, G

    M. Cristi´ a, G. Rossi, A set solver for finite set relation algebra, in: J. De- sharnais, W. Guttmann, S. Joosten (Eds.), Relational and Algebra ic Meth- ods in Computer Science - 17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29 - November 1, 2018, Pro ceedings, Vol. 11194 of Lecture Notes in Computer Science, Springer, 2...

    work page 2018

  24. [24]

    In: International Conference on Relational and Algebraic Methods in Computer Science, Springer, pp

    doi:10.1007/978-3-030-02149-8 20. URL https://doi.org/10.1007/978-3-030-02149-8\_20

    work page doi:10.1007/978-3-030-02149-8

  25. [25]

    Cristi´ a, G

    M. Cristi´ a, G. Rossi, C. S. Frydman, {log} as a test case generator for the Test Template Framework, in: R. M. Hierons, M. G. Merayo, M. Brav etti (Eds.), SEFM, Vol. 8137 of Lecture Notes in Computer Science, Spr inger, 2013, pp. 229–243

    work page 2013

  26. [26]

    J. F. Allen, Maintaining knowledge about temporal intervals, Com mun. ACM 26 (11) (1983) 832–843. doi:10.1145/182.358434. URL http://doi.acm.org/10.1145/182.358434

    work page doi:10.1145/182.358434 1983

  27. [27]

    Mentr´ e, C

    D. Mentr´ e, C. March´ e, J.-C. Filliˆ atre, M. Asuka, Dischargingproof obliga- tions from Atelier B using multiple automated provers, in: J. Derrick, J. A. Fitzgerald, S. Gnesi, S. Khurshid, M. Leuschel, S. Reeves, E. Ricco bene (Eds.), ABZ, Vol. 7316 of Lecture Notes in Computer Science, Sprin ger, 2012, pp. 238–251. 38

    work page 2012

  28. [28]

    Harvey, P

    W. Harvey, P. J. Stuckey, Improving linear constraint propag ation by changing constraint representation, Constraints An Int. J. 8 (2 ) (2003) 173–207. doi:10.1023/A:1022323717928. URL https://doi.org/10.1023/A:1022323717928

    work page doi:10.1023/a:1022323717928 2003

  29. [29]

    K. R. Apt, P. Zoeteweij, An analysis of arithmetic constraints o n integer intervals, Constraints An Int. J. 12 (4) (2007) 429–468. doi:10.10 07/s10601- 007-9017-9. URL https://doi.org/10.1007/s10601-007-9017-9

    work page doi:10.1007/s10601-007-9017-9 2007

  30. [30]

    Bozzelli, A

    L. Bozzelli, A. Molinari, A. Montanari, A. Peron, Model checking in terval temporal logics with regular expressions, Inf. Comput. 272 (2020 ) 104498. doi:10.1016/j.ic.2019.104498. URL https://doi.org/10.1016/j.ic.2019.104498

    work page doi:10.1016/j.ic.2019.104498 2020

  31. [31]

    A. A. Krokhin, P. Jeavons, P. Jonsson, Reasoning about temp oral relations: The tractable subalgebras of allen’s interval algebra, J. ACM 50 (5) (2003) 591–640. doi:10.1145/876638.876639. URL https://doi.org/10.1145/876638.876639

    work page doi:10.1145/876638.876639 2003

  32. [32]

    P. B. Ladkin, The completeness of a natural system for reaso ning with time intervals, in: J. P. McDermott (Ed.), Proceedings of the 10th Inte rnational Joint Conference on Artificial Intelligence. Milan, Italy, August 23- 28, 1987, Morgan Kaufmann, 1987, pp. 462–465. URL http://ijcai.org/Proceedings/87-1/Papers/091.pdf

    work page 1987

  33. [33]

    Janhunen, M

    T. Janhunen, M. Sioutis, Allen’s interval algebra makes the differ ence, in: P. Hofstedt, S. Abreu, U. John, H. Kuchen, D. Seipel (Eds.), Dec lara- tive Programming and Knowledge Management - Conference on Decla ra- tive Programming, DECLARE 2019, Unifying INAP, WLP, and WFLP, Cottbus, Germany, September 9-12, 2019, Revised Selected Pap ers, Vol. 12057 of ...

    work page doi:10.1007/978-3-030-46714-2 2019

  34. [34]

    All the y i p are of sort Int

    work page

  35. [35]

    All the y i p are such that k i≤ y i p≤ m i

    work page

  36. [36]

    Therefore, if (B.2) is unsatisfiable when (B.3) is satisfiable it must be b ecause Φ1∧ Φ2 implies at least one of the following:

    There are at least vi integer numbers in [ k i , m i ]—because all the y i p are different from each other. Therefore, if (B.2) is unsatisfiable when (B.3) is satisfiable it must be b ecause Φ1∧ Φ2 implies at least one of the following:

    work page

  37. [37]

    x∈ ˙Ai∧ ninteger(x )

    work page

  38. [38]

    x∈ ˙Ai∧ (x < k i∨ m i < x )

    work page

  39. [39]

    size( ˙Ai , q)∧ m i− k i + 1 < q m i− k i + 1 < q, size( ˙Ai , q)∧ ˙Ai⊆ [k i , m i ] is trivially unsatisfiable

    work page

  40. [40]

    (b) size( ˙Ai , m i− k i + 1− p) ∧ ˙Ai ⊆ [k i , m i ] implies that there are m i− k i + 1− p elements in [ k i , m i ]

    0 ≤ p∧ (⋀p+1 j =1 xp /∈ ˙Ai∧ k i≤ xp≤ m i )∧ size( ˙Ai , m i− k i + 1− p) (a) ⋀p+1 j =1 k i≤ xp≤ m i implies that there are p + 1 elements in [ k i , m i ]. (b) size( ˙Ai , m i− k i + 1− p) ∧ ˙Ai ⊆ [k i , m i ] implies that there are m i− k i + 1− p elements in [ k i , m i ]. (c) ⋀p+1 j =1 xp /∈ ˙Ai implies that the p + 1 elements of 4a are disjoint from ...

    work page

  41. [41]

    Then, if one of the new rewrite rules genera tes a constraint dealt by the old rewrite rules, the latter will not call the f ormer

    Rewrite rules of SAT |·|do not call the new rewrite rules as L|·|does not admit integer intervals. Then, if one of the new rewrite rules genera tes a constraint dealt by the old rewrite rules, the latter will not call the f ormer. Then, termination is proved in what concerns the interaction betwe en new and old rewrite rules

    work page

  42. [42]

    All these constraints are processed by CLP(Q) which only generates integer constraints

    Rules (10), (12), (13), (15), (16), (17), (18), (20), (22), (27), (28) and (29), produce only integer constraints or true. All these constraints are processed by CLP(Q) which only generates integer constraints. T hen, termination is proved

    work page

  43. [43]

    This is important because o ther rules in Figures 2-5 produce constraints of the form ·∈ [·,·] or· /∈ [·,·]

    Rules (16) and (17) trivially terminate. This is important because o ther rules in Figures 2-5 produce constraints of the form ·∈ [·,·] or· /∈ [·,·]. So when that happens, termination is proved

    work page

  44. [44]

    This is important because these a re the rules called when the identity (3) is applied

    Rules (22)-(24) are either non-recursive or self recursive, bu t they never make a recursion on another rule. This is important because these a re the rules called when the identity (3) is applied. Then, when (22)-(24) ar e called, termination is proved

    work page

  45. [45]

    Then, termination is proved

    Rule (11) generates a size-constraint in which case 1 applies; and a con- straint of the form ·⊆ [·,·] in which case 4 applies. Then, termination is proved

    work page

  46. [46]

    Then, te rmi- nation is proved

    Rule (14) calls rules (16) and (17), in which case 3 applies. Then, te rmi- nation is proved

    work page

  47. [47]

    Then, termination is proved

    Rule (19) generates a size and a∥ constraints in which case 1 applies; and a constraint of the form·⊆ [·,·] in which case 4 applies. Then, termination is proved

    work page

  48. [48]

    Then, termination is proved

    Rule (21) generates a constraint of the form ·∈ [·,·] in which case 3 applies. Then, termination is proved

    work page

  49. [49]

    They also generate constraints of the form [ ·,·] =·in which case 5 applies; and constraints of the form ·⊆ [·,·] in which case 4 applies

    Rules (25) and (26) generate equality, size and un constraints in which case 1 applies. They also generate constraints of the form [ ·,·] =·in which case 5 applies; and constraints of the form ·⊆ [·,·] in which case 4 applies. Then, termination is proved. 45 Appendix C. Two Operators Definable as L[ ] F ormulas In this section we show two more operators de...

    work page