Automated Reasoning with Nested Datatypes

1. [1]

   Preiner, H.-J

   M. Preiner, H.-J. Schurr, C. Barrett, P. Fontaine, A. Niemetz, C. Tinelli, SMT-LIB release 2025 (non-incremental benchmarks), Zenodo, 2025. URL: https://zenodo.org/records/15493090. doi:10. 5281/zenodo.15493090, version 2025.05.22

   work page arXiv 2025

2. [2]

   Barbosa, C

   H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, A. Ozdemir, M. Preiner, A. Reynolds, Y . Sheng, C. Tinelli, Y . Zohar, cvc5: A versatile and industrial-strength SMT solver, in: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer, 2022

   2022

3. [3]

   J. E. Zhong, K. Cheang, S. Qadeer, W. Grieskamp, S. Blackshear, J. Park, Y . Zohar, C. W. Barrett, D. L. Dill, The Move Prover, in: CA V , 2020

   2020

4. [4]

   L. M. de Moura, N. S. Bjørner, Z3: an efficient SMT solver, in: C. R. Ramakrishnan, J. Rehof (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedi...

   work page doi:10.1007/978-3-540-78800-3_ 2008

5. [5]

   doi:10.1007/978-3-540-78800-3\_24

   work page doi:10.1007/978-3-540-78800-3

6. [6]

   Barrett, P

   C. Barrett, P. Fontaine, C. Tinelli, The SMT-LIB Standard: Version 2.6, Technical Report, Depart- ment of Computer Science, The University of Iowa, 2017. Available atwww.SMT-LIB.org

   2017

7. [7]

   C. W. Barrett, I. Shikanian, C. Tinelli, An abstract decision procedure for a theory of inductive data types, Journal on Satisfiability, Boolean Modeling and Computation 3 (2007) 21–46

   2007

8. [8]

   D. C. Oppen, Reasoning about recursively defined data structures, J. ACM 27 (1980) 403–411. URL: http://doi.acm.org/10.1145/322203.322204. doi:10.1145/322203.322204

   work page doi:10.1145/322203.322204 1980

9. [9]

   A. Shah, F. Mora, S. A. Seshia, An eager satisfiability modulo theories solver for algebraic datatypes, in: M. J. Wooldridge, J. G. Dy, S. Natarajan (Eds.), Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advan...

   work page doi:10.1609/aaai.v38i8.28649 2024

10. [10]

    H. B. Enderton, A mathematical introduction to logic, Academic Press, 2001

    2001

11. [11]

    Tinelli, C

    C. Tinelli, C. G. Zarba, Combining decision procedures for sorted theories, in: J. J. Alferes, J. A. Leite (Eds.), Logics in Artificial Intelligence, 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27-30, 2004, Proceedings, volume 3229 ofLecture Notes in Computer Science, Springer, 2004, pp. 641–653

    2004

12. [12]

    A. R. Bradley, Z. Manna, The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007

    2007

13. [13]

    Sheng, Y

    Y . Sheng, Y . Zohar, C. Ringeissen, J. Lange, P. Fontaine, C. W. Barrett, Polite combination of algebraic datatypes, J. Autom. Reason. 66 (2022) 331–355

    2022

14. [14]

    Meinke, J

    K. Meinke, J. V . Tucker, Universal algebra (1992)

    1992

15. [15]

    Nelson, D

    G. Nelson, D. C. Oppen, Simplification by cooperating decision procedures, ACM Trans. Pro- gram. Lang. Syst. 1 (1979) 245–257. URL: https://doi.org/10.1145/357073.357079. doi:10.1145/ 357073.357079

    work page doi:10.1145/357073.357079 1979

16. [16]

    Blackshear, N

    S. Blackshear, N. Vasilakis, et al., Move: A language with programmable resources, in: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2019

    2019

17. [17]

    Barnett, B

    M. Barnett, B. E. Chang, R. DeLine, B. Jacobs, K. R. M. Leino, Boogie: A modular reusable verifier for object-oriented programs, in: Formal Methods for Components and Objects (FMCO), volume 4111 ofLecture Notes in Computer Science, Springer, 2006, pp. 364–387

    2006

18. [18]

    Commit ac0b70a656bfb63eb7e569444b7a3a5ed318d6de

    Libra / Diem Team, Libra move prover, https://github.com/libra/libra, accessed 2026. Commit ac0b70a656bfb63eb7e569444b7a3a5ed318d6de

    2026

19. [19]

    Commit 044e533713346840b55e53c33082911fd077d299

    Boogie Team, Boogie verifier, https://github.com/boogie-org/boogie, accessed 2026. Commit 044e533713346840b55e53c33082911fd077d299. 14

    2026

20. [20]

    Jovanovi´c, C

    D. Jovanovi´c, C. Barrett, Polite Theories Revisited, Technical Report TR2010-922, New York University, 2010

    2010

21. [21]

    Jovanovic, C

    D. Jovanovic, C. W. Barrett, Polite theories revisited, in: C. G. Fermüller, A. V oronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, volume 6397 ofLecture Notes in Computer Science, Springer, 2010, pp. 402–416. Extended technical r...

    2010

22. [22]

    Tinelli, C

    C. Tinelli, C. G. Zarba, Combining decision procedures for sorted theories, in: Logics in Artificial Intelligence, 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27-30, 2004, Proceedings, volume 3229 ofLecture Notes in Computer Science, Springer, 2004, pp. 641–653. 15 𝜓 𝑥=select(𝑎, 𝑗)∧𝑦=c(𝑘, 𝑎) trF ormula(𝜓) 𝑥* =select(𝑎 ′, 𝑗*)∧𝑦 * =c *(...

    2004

23. [23]

    identifier

    If 𝜎=𝐴 𝑖∘ for some 𝑖∈[1, 𝑛] then 𝜎 is interpreted in ℬ exactly in the same way 𝐴𝑖 is interpreted in𝒜. Intuitively, this means that the “identifier" of each array is itself

24. [24]

    If 𝜏 is neither in StructΣ𝑛+1 nor in ArrayΣ, then 𝜏 * /∈StructΣ𝜑 𝑛+1 and we interpret 𝜏 * in ℬ in the same way 𝜏 is interpreted in 𝒜

    If 𝜎=𝜏 * for some sort 𝜏, there are two sub-cases. If 𝜏 is neither in StructΣ𝑛+1 nor in ArrayΣ, then 𝜏 * /∈StructΣ𝜑 𝑛+1 and we interpret 𝜏 * in ℬ in the same way 𝜏 is interpreted in 𝒜. Otherwise, 𝜏 is in ArrayΣ, or in StructΣ𝑛+1, and thus 𝜏 * ∈Struct Σ𝜑 𝑛+1 , and we interpret 𝜏 * in ℬ as the set of trees defined in Definition 5

25. [25]

    Example 38

    If𝜎=𝐴 ′ 𝑖 for some𝑖∈[1, 𝑛], we interpret𝐴 ′ 𝑖 inℬas the set of functions from𝐼 * 𝑖 ℬ to𝐸 * 𝑖 ℬ. Example 38. Consider the formula 𝜓 and its satisfying interpretation 𝒜0 from Example 36. The sorts of Σ𝜓 ndt are interpreted inℬ 0 as described in Table 15. A.2. Interpretation of the Variables In order to define the interpretation of the variables, we define t...

26. [26]

    , 𝑠𝑚) and 𝑡2 = ^𝑐(𝑟1,

    If𝜎∈Struct Σ𝑛+1, then there are two options: (a) If 𝑡1 =𝑐(𝑠 1, . . . , 𝑠𝑚) and 𝑡2 = ^𝑐(𝑟1, . . . , 𝑟𝑘) with 𝑐̸= ^𝑐, then according to Remark 44, we have ΓDT(𝑡1) =𝑐 *(. . .)̸= ^𝑐 *(. . .) = Γ DT(𝑡2), since distinct constructors yield disjoint images. (b) Otherwise both use the same constructor 𝑐, say 𝑡1 =𝑐(𝑠 1, . . . , 𝑠𝑚) and 𝑡2 =𝑐(𝑟 1, . . . , 𝑟𝑚), but 𝑡...

27. [27]

    intended

    If𝜎=𝐴 𝑗 ∈Array Σ, then ΓDT(𝑡1) =𝑐 𝑗 (︀ 𝑡1, . . . )︀ ̸=𝑐 𝑗 (︀ 𝑡2, . . . )︀ = ΓDT(𝑡2) □ We can now define the function ΓArr that will be used to define the interpretation of some of the variables intrF ormula(𝜑). A.2.2. DefiningΓ Arr We define a function ΓArr : ⋃︀𝑛 𝑖=1 𝐴𝒜 𝑖 → ⋃︀𝑛 𝑖=1 𝐴′ℬ 𝑖 as follows: for each 𝑡∈𝐴 𝒜 𝑗 (with 𝑗∈[1, 𝑛] ), ΓArr(𝑡)∈𝐴 ′ℬ 𝑗 =𝐼 * 𝑗...

28. [28]

    Theselect 𝐴′ 𝑖 andstore 𝐴′ 𝑖 functions are interpreted in the usual way for every𝑖∈[1, 𝑛]. Proof: W.l.o.g., we can assume that the domains in ℬ of all the sorts in 𝒮Σ𝜑 ∖(Struct Σ𝜑 𝑛+1 ∪Array Σ𝜑) are completely fresh and flat (i.e., they in particular do not contain any constructor symbols in them, or more specifically, we may assume that they are “copies"...

29. [29]

    We define the domains of the sorts in𝒞

30. [30]

    We define the interpretations of the symbols in𝒞

31. [31]

    We show that𝒞is a𝑇 𝜑 new-interpretation

32. [32]

    We show that every literal in𝜑is satisfied by𝒞

33. [33]

    Let there be 𝜎∈ 𝒮 Σ𝜑

    Defining the domains.The domains of the sorts in Σ𝜑 are defined in Table 20. Let there be 𝜎∈ 𝒮 Σ𝜑. We have three cases to consider:

34. [34]

    Otherwise, we add infinitely many fresh elements to it, denoted as{𝑒 𝐴𝑖∘ 𝑘 |𝑘∈N}

    If 𝜎=𝐴 𝑖∘ for some 𝑖∈[1, 𝑛] then 𝜎 is interpreted in 𝒞 exactly in the same way it is interpreted in ℬ if its domain is already infinite. Otherwise, we add infinitely many fresh elements to it, denoted as{𝑒 𝐴𝑖∘ 𝑘 |𝑘∈N}

35. [35]

    a) If 𝜏 is neither in StructΣ𝑛+1 nor in ArrayΣ, then according to Table 5, 𝜏 * /∈StructΣ𝜑 𝑛+1

    If𝜎=𝜏 * for some sort𝜏, there are two sub-cases. a) If 𝜏 is neither in StructΣ𝑛+1 nor in ArrayΣ, then according to Table 5, 𝜏 * /∈StructΣ𝜑 𝑛+1 . We want to make sure that the cardinality of𝜏 *𝒞 is infinite, so if𝜏 *ℬ is finite, we add infinitely many fresh elements to it, denoted as {𝑒𝜏 * 𝑘 |𝑘∈N} . If 𝜏 *ℬ is already infinite, we simply set 𝜏 *𝒞 =𝜏 *ℬ. b)...

36. [36]

    By Lemma 55 we have∀𝜎∈ 𝒮 Σ.𝜎*ℬ ⊆𝜎 *𝒞

    If𝜎=𝐴 ′ 𝑖 for some𝑖∈[1, 𝑛], we interpret𝐴 ′ 𝑖 in𝒞as the set of functions from𝐼 * 𝑖 𝒞 to𝐸 * 𝑖 𝒞. By Lemma 55 we have∀𝜎∈ 𝒮 Σ.𝜎*ℬ ⊆𝜎 *𝒞

37. [37]

    We also create for every 𝑖∈[1, 𝑛] a mapping Ψ𝑖 :𝐴 ′ℬ 𝑖 →𝐴 ′𝒞 𝑖

    Defining the interpretation of the variables.For every 𝜎∈ 𝒮 Σ𝜑, we choose an arbitrary elementd 𝜎 ∈𝜎 𝒞. We also create for every 𝑖∈[1, 𝑛] a mapping Ψ𝑖 :𝐴 ′ℬ 𝑖 →𝐴 ′𝒞 𝑖 . Let there be 𝑥∈𝐴 ′ℬ 𝑖 . Note that 𝐴′𝒞 𝑖 is the set of functions from𝐼 * 𝑖 𝒞 to𝐸 * 𝑖 𝒞, and thus we can defineΨ 𝑖(𝑥) :𝐼 * 𝑖 𝒞 →𝐸 * 𝑖 𝒞 in the following way: ∀𝑗∈𝐼 * 𝑖 𝒞.Ψ𝑖(𝑥)(𝑗) = {︃ selectℬ...

38. [38]

    For every array variable𝑎of sort𝐴 ′ 𝑖, we set𝑎 𝒞 = Ψ𝑖(𝑎ℬ)

39. [39]

    This is well defined since we have shown that∀𝜎∈ 𝒮 Σ.𝜎*ℬ ⊆𝜎 *𝒞

    For every variable of any other sort (𝒮Σ𝜑 ∖Array Σ𝜑) , we set 𝑥𝒞 =𝑥 ℬ. This is well defined since we have shown that∀𝜎∈ 𝒮 Σ.𝜎*ℬ ⊆𝜎 *𝒞

40. [40]

    Defining the interpretation of the functions and predicates.The function symbols in 𝒞 are interpreted as follows:

41. [41]

    For every𝑖∈[1, 𝑛], theselect 𝐴′ 𝑖 function symbol is interpreted as select𝒞 𝐴′ 𝑖 (𝑎, 𝑗) =𝑎(𝑗)

42. [42]

    For every𝑖∈[1, 𝑛], thestore 𝐴′ 𝑖 function symbol is interpreted as store𝒞 𝐴′ 𝑖 (𝑎, 𝑗, 𝑣)(𝑘) = {︃ 𝑣if𝑘=𝑗 𝑎(𝑘)otherwise

43. [43]

    The constructor symbols are interpreted according to the datatype theory

44. [44]

    , 𝑡𝑛) 𝑠ℬ (𝑐,𝑖)(𝑥)otherwise, if𝑥∈𝜎 *ℬ d𝜏 * otherwise Note that this function is well defined since𝜏 *ℬ ⊆𝜏 *𝒞 and thus𝑠 ℬ (𝑐,𝑖)(𝑥)∈𝜏 *𝒞 when𝑥∈𝜎 *ℬ

    The selector symbols are interpreted as follows (𝑠 (𝑐,𝑖) :𝜎 * →𝜏 * when𝜎, 𝜏∈ 𝒮 Σ): 𝑠𝒞 (𝑐,𝑖)(𝑥) = ⎧ ⎪⎨ ⎪⎩ 𝑡𝑖 if𝑥=𝑐(𝑡 1, . . . , 𝑡𝑛) 𝑠ℬ (𝑐,𝑖)(𝑥)otherwise, if𝑥∈𝜎 *ℬ d𝜏 * otherwise Note that this function is well defined since𝜏 *ℬ ⊆𝜏 *𝒞 and thus𝑠 ℬ (𝑐,𝑖)(𝑥)∈𝜏 *𝒞 when𝑥∈𝜎 *ℬ

45. [45]

    Thus, we have thatΨ 𝑖(𝑓 ℬ 𝐴𝑖(𝑥))∈𝐴 ′𝒞 𝑖 for every𝑥∈𝐴 * 𝑖 ℬ

    For every function symbol𝑓 𝐴𝑖 of arity𝐴 * 𝑖 →𝐴 ′ 𝑖, we define: 𝑓 𝒞 𝐴𝑖(𝑥) = {︃ Ψ𝑖(𝑓 ℬ 𝐴𝑖(𝑥))if𝑥∈𝐴 * 𝑖 ℬ d𝐴′ 𝑖 otherwise Note that this function is well defined since 𝑓 ℬ 𝐴𝑖 :𝐴 * 𝑖 ℬ →𝐴 ′ℬ 𝑖 and Ψ𝑖 :𝐴 ′ℬ 𝑖 →𝐴 ′𝒞 𝑖 . Thus, we have thatΨ 𝑖(𝑓 ℬ 𝐴𝑖(𝑥))∈𝐴 ′𝒞 𝑖 for every𝑥∈𝐴 * 𝑖 ℬ

46. [46]

    Note that this function is well defined

    For every function symbol𝑔 𝐴𝑖 of arity𝐴 ′ 𝑖 →𝐴 * 𝑖 , we set 𝑔𝒞 𝐴𝑖(𝑥) = {︃ 𝑔ℬ 𝐴𝑖(Ψ−1 𝑖 (𝑥))ifΨ −1 𝑖 (𝑥)̸=∅ d𝐴* 𝑖 otherwise . Note that this function is well defined. First, we have already shown that Ψ𝑖 is injective, so Ψ−1 𝑖 (𝑥) contains a single element, if any. Second, sinceΨ𝑖 :𝐴 ′ℬ 𝑖 →𝐴 ′𝒞 𝑖 , we know that the restricted inverse Ψ−1 𝑖 ↾{𝑦∈𝐴′𝒞 𝑖 |Ψ−1 𝑖 ...

47. [47]

    ) 𝑓 𝑎𝑙𝑠𝑒otherwise By the way 𝒞 interprets the select𝐴′ 𝑗 and store𝐴′ 𝑗 for every 𝑗∈[1, 𝑛] , we get that 𝒞Σ* 𝑗 is an array Σ* 𝑗-structure

    The tester symbols are interpreted in the standard way for datatype structors: ∀𝑐∈ 𝒞𝒪 Σ𝜑.is 𝒞 𝑐 (𝑥) = {︃ 𝑡𝑟𝑢𝑒if𝑥=𝑐(. . .) 𝑓 𝑎𝑙𝑠𝑒otherwise By the way 𝒞 interprets the select𝐴′ 𝑗 and store𝐴′ 𝑗 for every 𝑗∈[1, 𝑛] , we get that 𝒞Σ* 𝑗 is an array Σ* 𝑗-structure. Likewise,𝒞 Σ𝜑 is a datatypeΣ 𝜑-structure. 29

48. [48]

    For each 𝑗∈[1, 𝑛] , the reduct 𝒞Σ* 𝑗 interprets select𝐴′ 𝑗 and store𝐴′ 𝑗 in the standard way for an arrays structure

    Showing that 𝒞 is a 𝑇 𝜑 new-interpretation.Recall that 𝑇 𝜑 new = (︁⨄︀𝑛 𝑗=1 𝑇 * 𝑗 )︁ ⊎𝑇 𝜑 𝑛+1 ⊎𝑇 𝑛+2 . For each 𝑗∈[1, 𝑛] , the reduct 𝒞Σ* 𝑗 interprets select𝐴′ 𝑗 and store𝐴′ 𝑗 in the standard way for an arrays structure. On Σ𝜑 𝑛+1, 𝒞 uses the usual tree-based interpretation of constructors, selectors and testers (see Definition 6). By construction, each se...

49. [49]

    Suppose ℬ satisfies ℓ

    Showing that 𝒞 satisfies every literal in 𝜑.Let ℓ be a literal in 𝜑. Suppose ℬ satisfies ℓ. We prove𝒞satisfies it, by considering all of its possible shapes

50. [50]

    b) If the sort of𝑥and𝑦is not𝐴 ′ 𝑖, then we have that 𝑥𝒞 =𝑥 ℬ =𝑦 ℬ =𝑦 𝒞

    For a literal of the form𝑥=𝑦, there are two cases: a) If the sort of𝑥and𝑦is𝐴 ′ 𝑖, then: 𝑥𝒞 = Ψ𝑖(𝑥ℬ) = Ψ𝑖(𝑦ℬ) =𝑦 𝒞. b) If the sort of𝑥and𝑦is not𝐴 ′ 𝑖, then we have that 𝑥𝒞 =𝑥 ℬ =𝑦 ℬ =𝑦 𝒞

51. [51]

    b) If the sort of𝑥and𝑦is not𝐴 ′ 𝑖, then we have that 𝑥𝒞 =𝑥 ℬ ̸=𝑦 ℬ =𝑦 𝒞

    For a literal of the form𝑥̸=𝑦, there are two cases: a) If the sort of𝑥and𝑦is𝐴 ′ 𝑖, the injectivity ofΨ 𝑖 ensures that: 𝑥𝒞 = Ψ𝑖(𝑥ℬ)̸= Ψ 𝑖(𝑦ℬ) =𝑦 𝒞. b) If the sort of𝑥and𝑦is not𝐴 ′ 𝑖, then we have that 𝑥𝒞 =𝑥 ℬ ̸=𝑦 ℬ =𝑦 𝒞

52. [52]

    The first equality holds since 𝑥∈vars 𝐸𝑖(𝜓) and thus 𝑥𝒞 =𝑥 ℬ

    For a literal of the form𝑥=select 𝐴′ 𝑖 (𝑎, 𝑗), we have that 𝑥𝒞 =𝑥 ℬ =select ℬ 𝐴′ 𝑖 (𝑎ℬ, 𝑗ℬ) =𝑎 𝒞(𝑗𝒞) =select 𝒞 𝐴′ 𝑖 (𝑎𝒞, 𝑗𝒞). The first equality holds since 𝑥∈vars 𝐸𝑖(𝜓) and thus 𝑥𝒞 =𝑥 ℬ. The second equality holds because ℬ satisfies the literal𝑥=select 𝐴′ 𝑖 (𝑎, 𝑗). The third equality holds by the definition of array variables in𝒞. The fourth equality hol...

53. [53]

    Thus: a)select ℬ 𝐴′ 𝑖 (𝑏ℬ, 𝑖ℬ) =𝑣 ℬ

    For a literal of the form𝑏=store 𝐴′ 𝑖 (𝑎, 𝑖, 𝑣), we already know that 𝑏ℬ =store ℬ 𝐴′ 𝑖 (𝑎ℬ, 𝑖ℬ, 𝑣ℬ). Thus: a)select ℬ 𝐴′ 𝑖 (𝑏ℬ, 𝑖ℬ) =𝑣 ℬ. b)∀𝑘∈𝐼 * 𝑖 ℬ ∖ {𝑖ℬ}.selectℬ 𝐴′ 𝑖 (𝑏ℬ, 𝑘) =select ℬ 𝐴′ 𝑖 (𝑎ℬ, 𝑘). Let there be 𝑘∈𝐼 * 𝑖 𝒞. Since, 𝐼𝑖 ∈ 𝒮 Σ ∖(Struct∪Array) , we have that 𝐼 * 𝑖 ℬ ⊆𝐼 * 𝑖 𝒞. Hence, 𝐼 * 𝑖 𝒞 ={𝑖 𝒞} ∪(𝐼 * 𝑖 ℬ ∖ {𝑖𝒞})∪(𝐼 * 𝑖 𝒞 ∖𝐼 * 𝑖 ℬ)and sin...

54. [54]

    , 𝑥𝑛), we have that 𝑦𝒞 =𝑦 ℬ =𝑐 ℬ(𝑥ℬ 1 ,

    For a literal of the form𝑦=𝑐(𝑥 1, . . . , 𝑥𝑛), we have that 𝑦𝒞 =𝑦 ℬ =𝑐 ℬ(𝑥ℬ 1 , . . . , 𝑥ℬ 𝑛) =𝑐 𝒞(𝑥𝒞 1 , . . . , 𝑥𝒞 𝑛)

55. [55]

    For a literal of the form𝑥=𝑠 (𝑐,𝑖)(𝑦), we have that 𝑥𝒞 =𝑥 ℬ =𝑠 ℬ (𝑐,𝑖)(𝑦ℬ) =𝑠 𝒞 (𝑐,𝑖)(𝑦𝒞)

56. [56]

    For a literal of the form is𝑐(𝑦) or ¬is𝑐(𝑦), we have that 𝑦𝒞 is an application of a constructor 𝑐 if and only if𝑦 ℬ is an application of a constructor𝑐

57. [57]

    For a literal of the form𝑎=𝑓 𝐴𝑖(𝑥), we have that 𝑎𝒞 = Ψ𝑖(𝑎ℬ) = Ψ𝑖(𝑓 ℬ 𝐴(𝑥ℬ)) =𝑓 𝒞 𝐴(𝑥𝒞)

58. [58]

    □ Example 57

    For a literal of the form𝑥=𝑔 𝐴𝑖(𝑎), we have that 𝑥𝒞 =𝑥 ℬ =𝑔 ℬ 𝐴(𝑎ℬ) =𝑔 ℬ 𝐴(Ψ−1 𝑖 (Ψ𝑖(𝑎ℬ))) =𝑔 𝒞 𝐴(𝑎𝒞). □ Example 57. Consider ^ℬ from Table 18, which satisfies the formulatrF ormula(𝜓)(Table 12). Accord- ing to Lemma 56, we can construct a Σ𝜓 ndt-interpretation ℬ1 that satisfies the same formula, and the three conditions specified in Lemma 56. This new in...

59. [59]

    If 𝜎 /∈StructΣ𝑛+1 ∪Array Σ, then by definition 𝜎𝑖 =𝜎 *ℬ =𝜎 𝑖+1, so the inclusion is immediate

60. [60]

    If𝜎∈Struct Σ𝑛+1, then𝜎 𝑖+1 =𝜎 𝑖 ∪𝑇 𝜎 (︀ Σ|𝒞𝒪,𝐵𝑖)︀ ,and hence𝜎 𝑖 ⊆𝜎 𝑖+1

61. [61]

    base:if𝑖= 0, then𝐴 0 𝑘 =∅, inductive step:If𝑖≥1, then since𝐸 𝑖−1 𝑘 ⊆𝐸 𝑖 𝑘 and𝐼 𝑖−1 𝑘 =𝐼 𝑖 𝑘, we have 𝐴𝑖 𝑘 =AC(𝐼 𝑖−1 𝑘 , 𝐸𝑖−1 𝑘 ) =AC(𝐼 𝑖 𝑘, 𝐸𝑖−1 𝑘 )⊆AC(𝐼 𝑖 𝑘, 𝐸𝑖 𝑘) =𝐴 𝑖+1 𝑘

    For all𝑘∈[1, 𝑛], we use induction over𝑖∈Nto show that𝐴 𝑖 𝑘 ⊆𝐴 𝑖+1 𝑘 . base:if𝑖= 0, then𝐴 0 𝑘 =∅, inductive step:If𝑖≥1, then since𝐸 𝑖−1 𝑘 ⊆𝐸 𝑖 𝑘 and𝐼 𝑖−1 𝑘 =𝐼 𝑖 𝑘, we have 𝐴𝑖 𝑘 =AC(𝐼 𝑖−1 𝑘 , 𝐸𝑖−1 𝑘 ) =AC(𝐼 𝑖 𝑘, 𝐸𝑖−1 𝑘 )⊆AC(𝐼 𝑖 𝑘, 𝐸𝑖 𝑘) =𝐴 𝑖+1 𝑘 . The inclusion holds since enlarging the codomain 𝑌 in AC(𝑋, 𝑌) preserves all almost constant functions. 32 □ No...

62. [62]

    If𝜎∈𝐹 𝑘, then𝜎 𝑘 ̸=∅by IH, so according to Lemma 59,𝜎 𝑘+1 ⊇𝜎 𝑘 ̸=∅

63. [63]

    Hence {︀ 𝑐(𝑡1,

    If there exists a constructor 𝑐:𝜎 1 × · · · ×𝜎 𝑛 →𝜎 with each 𝜎𝑖 ∈𝐹 𝑘, then IH gives 𝜎𝑘 𝑖 ̸=∅ . Hence {︀ 𝑐(𝑡1, . . . , 𝑡𝑛)|𝑡 𝑖 ∈𝜎 𝑘 𝑖 }︀ ⊆𝑇 𝜎(Σ|𝒞𝒪,𝐵𝑘)⊆𝜎 𝑘+1,so𝜎 𝑘+1 ̸=∅

64. [64]

    Therefore: 𝐴𝑘+1 𝑖 =AC(𝐼 𝑘 𝑖 , 𝐸𝑘 𝑖 )̸=∅

    If 𝜎=𝐴 𝑖 is an array sort where 𝐸𝑖, 𝐼𝑖 ∈𝐹 𝑘, then IH gives 𝐼 𝑘 𝑖 ̸=∅ and 𝐸𝑘 𝑖 ̸=∅ . Therefore: 𝐴𝑘+1 𝑖 =AC(𝐼 𝑘 𝑖 , 𝐸𝑘 𝑖 )̸=∅. Hence for each𝜎there is some𝑘with𝜎 𝑘 ̸=∅, and so𝜎 𝒜 = ⋃︀ 𝑘∈N 𝜎𝑘 is nonempty.□ B.3. Properties of the Domains of the𝒯 N𝐷𝑇 Σ -interpretation In order to show that 𝒜 is a 𝒯 N𝐷𝑇 Σ -interpretation, we need to show that the relation ℛ𝒜 is...

65. [65]

    , 𝑢𝑗−1, 𝑥, 𝑢𝑗+1,

    In case (1), we fix for each𝑠∈[1, 𝑘]∖ {𝑗}some𝑢 𝑠 ∈𝜏 𝒜 𝑠 and define: 𝑓𝑖(𝑥) =𝑐(𝑢 1, . . . , 𝑢𝑗−1, 𝑥, 𝑢𝑗+1, . . . , 𝑢𝑘)

66. [66]

    34 □ Definition 66

    In case (2), we define 𝑓𝑖(𝑥) as the constant array from 𝐼 𝒜 𝑘 to 𝐸𝒜 𝑘 whose image is the singleton {𝑥}. 34 □ Definition 66. Let ΣDT be a datatype signature and 𝒞 be a ΣDT-interpretation. For every 𝑥∈𝜎 𝒞 for some𝜎∈ 𝒮 ΣDT, we define theminimum index of𝑥, denoted dtIdx(𝑥), as follows: dtIdx(𝑥) = min{𝑖∈N|𝑥∈𝑇 𝜎,𝑖(ΣDT|𝒞𝒪ΣDT , 𝐵)} where𝐵is theElem-sorted set wit...

67. [67]

    If 𝜎∈ 𝒮 Σ ∖(Array Σ ∪Struct Σ𝑛+1), step 0 suggests that every such sort has an infinite domain, contradicting the fact that every sort in𝑉 ′′ has a finite domain

68. [68]

    Hence𝜎∈Struct Σ𝑛+1 and thus𝑉 ′′ ⊆Struct Σ𝑛+1

    If 𝜎=𝐴 𝑘 for some 𝑘∈[1, 𝑛] , then its element sort 𝐸𝑘 would be reachable from 𝐴𝑘 inside 𝐺′′ Σ, contradicting the definition of𝐸 𝑖1. Hence𝜎∈Struct Σ𝑛+1 and thus𝑉 ′′ ⊆Struct Σ𝑛+1. Step 5. The sorts in 𝑉 ′′ must be interpreted as in 𝒜.For every 𝑇𝑛+1-interpretation 𝒞 and every 𝜎∈𝑉 ′′ we have𝜎 𝒞 =𝜎 𝒜. In order to prove this claim, we first remember that accord...

69. [69]

    Then, let 𝜎∈𝑉 ′′: 𝑇𝜎,𝑘+1(Σ|𝒞𝒪,𝐵) = 𝑇𝜎,𝑘(Σ|𝒞𝒪,𝐵)∪ {︀ 𝑐(𝑡1,

    Step:Assume 𝑇𝜏,𝑘(Σ|𝒞𝒪,𝐵) =𝑇 𝜏,𝑘(Σ|𝒞𝒪, ̂︀𝐵) for every𝜏∈𝑉 ′′. Then, let 𝜎∈𝑉 ′′: 𝑇𝜎,𝑘+1(Σ|𝒞𝒪,𝐵) = 𝑇𝜎,𝑘(Σ|𝒞𝒪,𝐵)∪ {︀ 𝑐(𝑡1, . . . , 𝑡𝑚) ⃒⃒ 𝑐:𝜏 1 × · · · ×𝜏 𝑚 →𝜎∈ 𝒞𝒪 Σ𝑛+1, 𝑡 𝑖 ∈𝑇 𝜏𝑖,𝑘(Σ|𝒞𝒪,𝐵) }︀ . Since 𝜏1, . . . , 𝜏𝑚 ∈𝑉 ′′, by the IH we have 𝑇𝜏𝑖,𝑘(Σ|𝒞𝒪,𝐵) =𝑇 𝜏𝑖,𝑘(Σ|𝒞𝒪, ̂︀𝐵) for every 𝑖∈[1, 𝑚] . Thus,𝑇 𝜎,𝑘+1(Σ|𝒞𝒪,𝐵) =𝑇 𝜎,𝑘+1(Σ|𝒞𝒪, ̂︀𝐵). Thus,𝜎 𝒞 =𝑇 𝜎(Σ|𝒞𝒪, ̂︀𝐵) ...

70. [70]

    If 𝑠1 =𝑠 2, then (𝑠2, 𝑠1) = (𝑠1, 𝑠2)∈𝑅

    Symmetry:Assume (𝑠1, 𝑠2)∈𝑅 . If 𝑠1 =𝑠 2, then (𝑠2, 𝑠1) = (𝑠1, 𝑠2)∈𝑅 . Otherwise, 𝑠1, 𝑠2 ∈ SE𝜑(ℬ) and tl(𝑓 ℬ 𝐴𝑖(𝑠1)) =tl(𝑓 ℬ 𝐴𝑖(𝑠2)). By symmetry of equality, tl(𝑓 ℬ 𝐴𝑖(𝑠2)) =tl(𝑓 ℬ 𝐴𝑖(𝑠1)), hence(𝑠 2, 𝑠1)∈𝑅. 39

71. [71]

    If 𝑠1 =𝑠 2 or 𝑠2 =𝑠 3, then by substitution we obtain (𝑠1, 𝑠3)∈𝑅

    Transitivity:Assume (𝑠1, 𝑠2),(𝑠 2, 𝑠3)∈𝑅 . If 𝑠1 =𝑠 2 or 𝑠2 =𝑠 3, then by substitution we obtain (𝑠1, 𝑠3)∈𝑅 . Otherwise, 𝑠1, 𝑠2, 𝑠3 ∈SE 𝜑(ℬ) and tl(𝑓 ℬ 𝐴𝑖(𝑠1)) =tl(𝑓 ℬ 𝐴𝑖(𝑠2)) and tl(𝑓 ℬ 𝐴𝑖(𝑠2)) = tl(𝑓 ℬ 𝐴𝑖(𝑠3)). By transitivity of equality,tl(𝑓 ℬ 𝐴𝑖(𝑠1)) =tl(𝑓 ℬ 𝐴𝑖(𝑠3)), hence(𝑠 1, 𝑠3)∈𝑅. Thus 𝑅 partitions 𝑆∩𝐴 * 𝑖 ℬ into equivalence classes. Since this s...

72. [72]

    If 𝑥∈𝜎 ℬ for some 𝜎 /∈StructΣ𝜑 𝑛+1 and 𝑥∈ ∪{𝜎 𝒜 |𝜎∈ 𝒮 Σ} ∪ (︀⋃︀ 𝑖∈[1,𝑛] 𝐴𝑖∘ℬ)︀ , then Ψ(𝑥) =𝑥

73. [73]

    , 𝑡𝑘) for some 𝑐:𝜎 1 × · · · ×𝜎 𝑘 →𝜎∈ 𝒞𝒪 Σ𝑛+1, Ψ is defined for 𝑡1,

    If 𝑥=𝑐 *(𝑡1, . . . , 𝑡𝑘) for some 𝑐:𝜎 1 × · · · ×𝜎 𝑘 →𝜎∈ 𝒞𝒪 Σ𝑛+1, Ψ is defined for 𝑡1, . . . , 𝑡𝑘, and ∀𝑖∈[1, 𝑘].Ψ(𝑡 𝑖)∈𝜎 𝒜 𝑖 thenΨ(𝑥) =𝑐(Ψ(𝑡 1), . . . ,Ψ(𝑡𝑘))

74. [74]

    , 𝑡𝑘) for some 𝑖∈[1, 𝑛] , Ψ is defined over 𝑡1,

    If 𝑥=𝑐 𝑖(𝑡1, . . . , 𝑡𝑘) for some 𝑖∈[1, 𝑛] , Ψ is defined over 𝑡1, . . . , 𝑡𝑘 and ∀𝑗∈2, . . . , 𝑘.Ψ(𝑡 𝑗)∈ 𝐸𝒜 𝑖 , then we defineΨ(𝑥)as follows: ∀𝑗∈𝐼 𝒜 𝑖 .Ψ(𝑥)(𝑗) = {︃ Ψ(𝑡min{𝑜(𝑘)|𝑘∈AssocInd(𝑥,𝑖).𝑘 *ℬ=𝑗}+1)if∃𝑘∈AssocInd(𝑥, 𝑖).𝑘 *ℬ =𝑗 tail𝑖(𝑥)otherwise Example 82.Consider the formula𝜓and its translation in Table 12 andℬ 1 as defined in Table 21. The set𝑆is g...

75. [75]

    , 𝑡𝑚) and 𝑦=𝑐 *(𝑠1,

    If 𝑥=𝑐 *(𝑡1, . . . , 𝑡𝑚) and 𝑦=𝑐 *(𝑠1, . . . , 𝑠𝑚) for some 𝑐:𝜎 1 × · · · ×𝜎 𝑘 →𝜎∈ 𝒞𝒪 Σ𝑛+1, then by definition there exists some 𝑗∈[1, 𝑘] such that 𝑡𝑗 ̸=𝑠 𝑗. According to the IH, Ψ(𝑡𝑗)̸= Ψ(𝑠 𝑗), and thusΨ(𝑥) =𝑐(Ψ(𝑡 1), . . . ,Ψ(𝑡𝑚))̸=𝑐(Ψ(𝑠 1), . . . ,Ψ(𝑠𝑚)) = Ψ(𝑦)

76. [76]

    , 𝑡𝑚) and 𝑦= ˜𝑐 *(𝑠1,

    If 𝑥= ^𝑐 *(𝑡1, . . . , 𝑡𝑚) and 𝑦= ˜𝑐 *(𝑠1, . . . , 𝑠𝑙), then Ψ(𝑥) = ^𝑐(Ψ(𝑡 1), . . . ,Ψ(𝑡𝑚))̸= ˜𝑐(Ψ(𝑠1), . . . ,Ψ(𝑠𝑙)) = Ψ(𝑦),since^𝑐̸= ˜𝑐. • If 𝑥, 𝑦∈𝐴 * 𝑖 ℬ for some 𝑖∈[1, 𝑛] , then we can denote 𝑥=𝑐 𝑖(𝑡1, . . . , 𝑡𝑘) and 𝑦=𝑐 𝑖(𝑠1, . . . , 𝑠𝑙). There are 2 subcases:

77. [77]

    Hence, for every 𝑘∈𝐼 * 𝑖 ∖ {𝑙*ℬ |𝑙∈I (𝐴𝑖,𝜑)} we have that Ψ(𝑥)(𝑘) =tail 𝑖(𝑥)̸=tail 𝑖(𝑦) = Ψ(𝑦)

    If ¬ (︀ 𝑥, 𝑦∈SE 𝜑(ℬ)∧tl(𝑓 ℬ 𝐴𝑖(𝑥)) =tl(𝑓 ℬ 𝐴𝑖(𝑦)) )︀ according to Lemma 76,tail𝑖(𝑥)̸=tail 𝑖(𝑦). Hence, for every 𝑘∈𝐼 * 𝑖 ∖ {𝑙*ℬ |𝑙∈I (𝐴𝑖,𝜑)} we have that Ψ(𝑥)(𝑘) =tail 𝑖(𝑥)̸=tail 𝑖(𝑦) = Ψ(𝑦)

78. [78]

    Since𝑥, 𝑦∈SE 𝜑(ℬ)there are𝑎, 𝑏∈vars 𝐴𝑖(𝜑)with𝑎 *ℬ =𝑥and𝑏 *ℬ =𝑦

    Otherwise, we have that (︀ 𝑥, 𝑦∈SE 𝜑(ℬ)∧tl(𝑓 ℬ 𝐴𝑖(𝑥)) =tl(𝑓 ℬ 𝐴𝑖(𝑦)) )︀ . Since𝑥, 𝑦∈SE 𝜑(ℬ)there are𝑎, 𝑏∈vars 𝐴𝑖(𝜑)with𝑎 *ℬ =𝑥and𝑏 *ℬ =𝑦. ℬsatisfiesL 3(𝜑): –𝑎 * =𝑔 𝐴𝑖(𝑎′), –𝑏 * =𝑔 𝐴𝑖(𝑏′), –𝑎 ′ =𝑓 𝐴𝑖(𝑎*), –𝑏 ′ =𝑓 𝐴𝑖(𝑏*). Thus, we have𝑎 ′ℬ =𝑓 ℬ 𝐴𝑖(𝑥)and𝑏 ′ℬ =𝑓 ℬ 𝐴𝑖(𝑦). Suppose towards contradiction that𝑎 ′ℬ =𝑏 ′ℬ. Using the first 2 equalities, we have: 𝑥=𝑎 ...

79. [79]

    ,idx(𝑡𝑚)}

    If 𝑥𝑖+1ℛ𝒜𝑥𝑖 by the first case then 𝑘𝑖+1 ≤𝑘 𝑖:If 𝑥𝑖+1ℛ𝒜𝑥𝑖 by the first case, then by Lemma 86, we have that 𝑘𝑖 ≥max{idx(𝑡 1), . . . ,idx(𝑡𝑚)}. Since 𝑥𝑖+1 =𝑡 𝑗 for some 𝑗∈[1, 𝑚] , we have that 𝑘𝑖+1 =idx(𝑡 𝑗)≤𝑘 𝑖

80. [80]

    By Lemma 87, we have that𝑘 𝑖+1 =idx(select 𝒜 𝐴𝑚(𝑥𝑖, 𝑗))<idx(𝑥 𝑖) =𝑘 𝑖

    If 𝑥𝑖+1ℛ𝒜𝑥𝑖 by the second case then 𝑘𝑖+1 < 𝑘 𝑖:We can assume that 𝜎𝑖 =𝐴 𝑚 for some 𝑚∈[1, 𝑛]. By Lemma 87, we have that𝑘 𝑖+1 =idx(select 𝒜 𝐴𝑚(𝑥𝑖, 𝑗))<idx(𝑥 𝑖) =𝑘 𝑖

Showing first 80 references.