{'fraction_non_alphanumeric': 0.050633944160697095, 'fraction_numerical': 0.008240458202111516, 'mean_word_length': 3.8186821827331343, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 4, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 45, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
The Extended Theory of Trees and Algebraic (Co)datatypes

The first-order theory of finite and infinite trees has been studied since the eighties, especially by the logic programming community. Following Djelloul, Dao and Fr\"uhwirth, we consider an extension of this theory with an additional predicate for finiteness of trees, which is useful for expressing properties about (not just datatypes but also) codatatypes. Based on their work, we present a simplification procedure that determines whether any given (not necessarily closed) formula is satisfiable, returning a simplified formula which enables one to read off all possible models. Our extension makes the algorithm usable for algebraic (co)datatypes, which was impossible in their original work due to restrictive assumptions. We also provide a prototype implementation of our simplification procedure and evaluate it on instances from the SMT-LIB.


Introduction
Trees play a fundamental role in computer science: syntactic terms can be regarded as finite trees, and operations like matching and unification, which are essential to functional and logic programming languages, can be viewed as solving certain first-order constraints in the structure of finite trees. Furthermore, trees are a model for program schemes, such as higher-order recursion schemes [11], and more generally as computation trees. The structures of finite and infinite trees are also central to the declarative semantics of logic (e.g. [7]) and functional languages (e.g. [15]). Furthermore, they play a role in the verification of programs [12] and in term rewriting systems [5]. The theory of finite and infinite trees was extensively studied by the logic programming community in the eighties. An axiomatization and a decision procedure for these structures was given by Maher in [8,9].
The structure of trees just consists of what one would normally think of as trees with labeled nodes, except that we allow them to be infinite. Examples of finite and infinite trees are depicted in Fig. 1. The labels for these trees are suggestively named after constructors for common algebraic datatypes because we want to specifically consider applications to the theory of (co)datatypes. In functional programming, two common data structures are natural numbers and linked lists: data nat = zero | succ(pred: nat) data list = nil | cons(head: nat, tail: list) Inhabitants of these types are naturally viewed as trees: the term cons(succ(zero), cons(zero, nil)) is shown as a tree in Fig. 1a. In some languages, such as Haskell, datatypes behave in fact more like codatatypes [14], i.e. they can be infinitely nested. For example, the term let t = cons(zero, cons(succ(zero), t)) in t corresponds to the infinite tree shown in Fig. 1b.
In this work, we consider the first-order theory of trees, extended with a predicate fin(t) for stating finiteness of t, and propose it as a tool for reasoning about algebraic datatypes and codatatypes. Why not use the theory of (co)datatypes as implemented in many SMT solvers? First, the theory of (co)datatypes is undecidable because selectors (head, tail) can be applied to the wrong constructor (nil) and the standard semantics from the SMT-LIB [2] does not specify the result of such an operation (cf. Section 3). Secondly, the theory of trees not only allows us to treat datatypes and codatatypes in a uniform way (both are represented by trees, datatypes just require a fin-predicate), but it is even more expressive: it can explicitly state non-finiteness (¬ fin(t)), as well as finiteness only for a proper subformula (cf. Section 3). Codatatypes are often used in mechanized proofs to represent infinite structures [14] and we believe that this increased flexibility can be useful there as well.
This extended theory of trees (with a fin-predicate) was first presented by Djelloul, Dao and Frhwirth in [4], where they also present a complete axiomatization and a decision procedure. However, one of their core assumptions is that there are infinitely many function symbols (i.e. constructors), which renders it unsuitable for algebraic (co)datatypes found in programming languages since those never have infinitely many constructors. In this work, we lift this restriction and allow sorts with finitely many generators. Note that we require at least two generators, however. Sorts with one generator are not hard to support in principle but require a lot of special casing, so we do not discuss them in this work.
Contributions Our first contribution is a formal description of the relationship between the theory of algebraic (co)datatypes and the extended theory of trees. We also present a decision procedure for first-order formulae (including quantifiers) in the latter, based on [4]. To the best of our knowledge, no decision procedure for this theory allowing finitely generated sorts was known before. Just like the algorithm in [4], it is not only a decision procedure that outputs "satisfiable" or "unsatisfiable" but instead, it simplifies the given input formula as much as possible, which makes it easy to read off all satisfying valuations of the free variables.
We propose this extended theory of trees as an interesting background theory for constrained Horn clauses. Recently, Ong and Wagner [10] proved that satisfiability of higher-order constrained Horn clauses (HoCHCs) is semi-decidable if the background theory is decidable. Since the extended theory of trees is decidable, it is potentially suitable as a background theory for HoCHCs. In addition, we hope that the existence of a simplification procedure instead of a mere decision procedure will also have useful applications to constrained Horn clauses.
Frhwirth [4]. However, they require that each sort have at least one constant generator and infinitely many non-constant generators. This assumption simplifies the treatment of the theory significantly but has the serious drawback that it makes their method unsuitable for algebraic (co)datatypes, which typically have only finitely many constructors (i.e. generators). Therefore, we first take a look at the relation between the two theories.

Relationship with (Co)Datatypes
The theory of algebraic (co)datatypes, also called (co)inductive datatypes, is similar to the theory of trees but there are a couple of important differences. For one thing, the set of sorts is partitioned into S = S dt ∪ S ct where S dt is the set of datatypes and S ct is the set of codatatypes. The function symbols are partitioned into the constructors F ctr and the selectors F sel , and there are no predicate symbols. Each (co)datatype δ is equipped with m ≥ 1 constructors F δ ctr = {C 1 , . . . , C m }. Each constructor C i ∈ F δ ctr has an arity δ 1 × · · · × δ n i → δ and is associated with n i selectors sel j C i : δ → δ j . Note that for a datatype (resp. codatatype) declaration, all constructor arguments must be datatypes (resp. codatatypes); no mixing is allowed. Such an assumption is common, for example in [14]. Another requirement is that datatypes be well-founded, i.e. one must be able to exhibit a ground term for each datatype. This excludes examples like a datatype infinite with a single constructor next : infinite → infinite. However, this is allowed as a codatatype. Semantics Both datatypes and codatatypes are interpreted as constructor trees, i.e. trees labeled only with constructors (not selectors). A structure D of (co)datatypes interprets a codatatype γ as the set γ D of constructor trees of sort γ and a datatype δ as the set δ D of finite constructor trees of sort δ . Each constructor C : s 1 × · · · × s n → s is interpreted as the function C D : s D 1 × · · · × s D n → s D constructing a new tree out of the given ones, with root C. Each selector sel i C : s → s i is interpreted as a function . . ,t n )) = t i but is not specified on inputs built with the wrong constructor. This semantics is very common and what the SMT-LIB standard specifies [2]. Note that other semantics are possible, however, such as returning a fixed default value if a selector is applied to the wrong constructor [3]. We call the latter the semantics with default values. The theory of (co)datatypes is the set of sentences that are true in any structure of (co)datatypes satisfying the above. Theorem 3.2. The first-order theory of (co)datatypes is undecidable.
Proof idea. The proof is based on the undecidability of formulae with quantifiers in the theory of uninterpreted functions (EUF). Uninterpreted functions f : s 1 × s 2 → s can be emulated using the following construct: data dummy = c(a 1 : s 1 , a 2 : s 2 ) | d(h : s) Then h(c(x, y)) acts like an unintepreted function f (x, y) because the selector h is applied to the wrong constructor c. For the full proof, refer to the appendix.
In the semantics with default values, selectors present much less of a problem: they can simply be eliminated. Theorem 3.3. In the theory of (co)datatypes with default values, a given formula can be effectively transformed into an equivalent one without selectors.
Proof idea. The idea is to introduce additional variables such that selectors only occur in equations of the form x = sel i C (t) where t does not contain selectors and then to rewrite such an equation as C is the default value for this selector. For the full proof, refer to the appendix.
But even in the standard semantics, quantifier-free formulae in the theory of (co)datatypes are decidable [14]. In fact, we can also eliminate selectors from such formulae.
Theorem 3.4. In the theory of (co)datatypes with standard semantics, a quantifier-free formula can be effectively transformed into an equisatisfiable one without selectors (but including quantifiers).
Proof idea. The first step is to introduce additional variables such that selectors only occur in equations of the form x = sel i C (t) where t does not contain selectors. For each such equation, we add the conjunct ∀z.t = C(z) → z i = x, which ensures that the selector correctly extracts the argument when applied to the right constructor. Furthermore, for each pair of such equations , we add the conjunct t = t ′ → x = x ′ , which ensures that selectors behave like functions, i.e. return the same result when applied to the same arguments. For the full proof, refer to the appendix.
Finally, we show that the theory of trees is enough for selector-free formulae.
Theorem 3.5. A selector-free formula in the theory of (co)datatypes can be effectively transformed into an equisatisfiable formula in the extended theory of trees.
Proof idea. Since in both theories, terms are interpreted as trees, we just have to ensure that datatypes are interpreted as finite trees. Hence, for a datatype d, existential quantification ∃x : d. φ is replaced by ∃x : d. fin(x) ∧ φ and universal quantification ∀x : d.φ is replaced by ∀x : d. fin(x) → φ . Finally, to ensure equisatisfiablity, free variables x : d require adding the conjunct fin(x) to the whole formula. For the full proof, refer to the appendix.
The last result raises the question of how the expressiveness of the extended theory of trees compares to selector-free (co)datatypes. The former is, in fact, more expressive because it allows specifying non-finiteness of individuals, such as ¬ fin(x). This is impossible in the theory of (co)datatypes since datatypes have only finite values and codatatypes can have finite and infinite values. Additionally, it facilitates specifying finiteness only in parts of the formula, such as in ( where t is finite in φ but infinite in ψ. This shows that the extended theory of trees is more powerful than the (selector-free) theory of (co)datatypes.

Analyzing Finitely Generated Sorts
Having shown how formulae involving (co)datatypes can often be reduced to formulae involving trees, we want to find a decision procedure for the latter based on the work by Djelloul, Dao and Frhwirth [4]. Their algorithm, however, makes the assumption that each sort contains infinitely many non-constant generators and one constant generator. As a consequence, each sort contains infinitely many finite and false : bool zero : nat nil : list infinitely many infinite trees. This simplifies solving logical formulae: the predicate fin(x) can always be made true or false for an appropriate valuation of x. However, their assumption is obviously not satisfied for sorts arising from (co)datatypes. Therefore, we consider the setting with finitely generated sorts, where the situation is more complicated. For instance, if x is of, say, a Boolean sort with only constant generators then the predicate fin(x) is always true. Due to these complications, we need to analyze the set of sorts and check for sorts with only finitely many finite or infinite trees.
In the following, we allow sorts with finitely many generators but assume that any sort has at least two generators. As mentioned before, this restriction is not hard to lift in principle but saves us a lot of technical details and space in this paper. Note that sorts with a single non-recursive generator can just be unfolded in the place that they are used.
For a sort s, denote by s fin , respectively s infin , the set of finite, respectively infinite, trees of sort s. Denote by S 0F , S FF , S 0I , S 1I , S FI ⊆ S the sets of sorts with no finite trees, finitely many finite trees, no infinite trees, exactly one infinite tree, and finitely many infinite trees, respectively. In the following, we present algorithms for computing these sets.
Algorithm 1 Algorithm computing the sets of sorts containing no finite (S 0F ⊆ S) or no infinite trees (S 0I ⊆ S), when given a signature (S, F, P) as input.
S 0I ← S 0I ∪ {s ∈ S | ∀(g : s 1 × · · · × s n → s) ∈ F s : ∀i ∈ {1, . . . , n} : s i ∈ S 0I } S 0F ← S 0F \ {s ∈ S | ∃(g : s 1 × · · · × s n → s) ∈ F s : ∀i ∈ {1, . . . , n} : s i / ∈ S 0F } until no changes in the last iteration Proof idea. A sort contains no infinite trees if every generator only takes arguments of sorts containing no infinite trees. A sort contains no finite trees unless some generator takes only arguments of sorts with finite trees. The sets S 0F and S 0I can thus be computed as fixed points, the former a least fixed point, the latter a greatest fixed point. For details, refer to the full proof in the appendix.  Fig. 2. How would Algorithm 1 act on this input? In the first iteration, it would add bool to S 0I because each generator is a constant. At the same time, bool, list, and nat are removed from S 0F because each one has a constant generator. In the next iteration, S 0I Algorithm 2 Algorithm computing the sets of sorts containing only finitely many finite (S FF ), respectively infinite (S FI ), trees; and their finite (s fin ), respectively infinite (s infin ), inhabitants.
Compute S 0I and S 0F as in Algorithm 1 . . , r n ) | (g : s 1 × · · · × s n → s) ∈ F infin s ; r j ∈ (s j ) fin ∪ (s j ) infin for j = 1, . . . , n such that ∃i ∈ {1, . . . , n} : r i / ∈ (s i ) fin } until no changes in the last iteration stays unchanged but d is removed from S 0F because it has the generator c1 whose parameter sort bool is not in S 0F anymore. For a similar reason, t is removed from S 0F . After this point, no more changes happen and we obtain S 0I = {bool} and S 0F = {inftree}.
Next, we consider the sets S FF , S 1I , S FI . Note that the sort nat from the above example has exactly one infinite tree, namely succ(succ(. . . )). For such sorts s ∈ S 1I , we introduce variables u s for their unique infinite tree. For instance, u nat = succ(u nat ) describes the unique infinite tree of nat. The sort t has two infinite trees g2(false, u nat ) and g2(true, u nat ). Hence to describe all infinite trees of sorts s ∈ S FI , we need the variables u s for s ∈ S 1I and their equations, like u nat = succ(u nat ). Algorithm 2 computes all this. Furthermore it computes the set s fin (the terms for the finite trees of sort s for s ∈ S FF ), and the set s infin (the terms for the infinite trees of sort s for s ∈ S FI ). The latter makes use of the variables u s (for s ∈ S 1I ), standing for the unique infinite tree of s. The equations that uniquely determine these u s are output in U s . Proof idea. Similarly to the previous algorithm, these sets are computed as fixed points. A sort s has only finitely many finite trees if there is a finite number of generators that only take sorts with finitely many finite trees as arguments (F s \ F infin s ), and the remaining generators (F infin s ) take at least one argument of a sort that contains no finite trees (because such a generator cannot create finite trees). Along the way, the algorithm builds up the set s fin from the generators of the former category.
Constructing the set S FI works similarly, except for the fact that we start the fixed point iteration with S 0I ∪ S 1I instead of the empty set. The reason is that for every sort with finitely many infinite trees, it can be shown (but is nontrivial) that the infinite parts of each such tree are built from the unique infinite trees of the sorts S 1I . These sorts with a unique infinite tree are also constructed by fixed point iteration. They can only have a single generator g that constructs infinite trees and it can only take one argument because otherwise we would have at least two infinite trees since each sort is assumed to have at least two generators.
A sort s only has finitely many infinite trees if the set of generators constructing infinite trees (F infin s ) is finite, and when picking an arbitrary argument i of it, this argument allows no infinite trees; or it allows finitely many infinite trees and all the other arguments allow only finitely many trees. This explains the fixed point iteration for S FI and s infin . For details, refer to the full proof in the appendix. In the first iteration, bool is added to S FF because all its generators are constants, and bool fin = {false, true}. Additionally, nat stays in S 1I because its generator succ satisfies nat ∈ S 1I and the other generator is constant. Therefore U nat = {u nat = succ(u nat )}. All the other sorts are removed from S 1I , either because they don't have a unary generator (bool, list) or there is another generator that allows infinite trees, destroying uniqueness (tree2 for inftree, c2 for d, and g2 for t). In the second iteration, d is added to S FF because c1 : bool → d only constructs finitely many finite trees since bool ∈ S FF and its other generator c2 constructs only infinite trees. Therefore, d fin is set to {c1(true), c1(false)}. After this points, no more changes happen.
At the start of the second loop, we have S FI = {bool, nat} and nat infin = {u nat }. In the loop iteration, t is added to S FI because we have F infin t = {g2}, which is finite, and its only generator g2 has the property that its first parameter is bool ∈ S 0I and its second parameter is nat ∈ S FI with the additional property that all remaining parameters, i.e. bool, are in S FF ∩ S FI . Therefore t infin is set to {g2(false, u nat ), g2(true, u nat )}. After this point, no more changes happen. The algorithm has computed S FF = {in f tree, bool, d} and S FI = {nat,t}.

Simplification Procedure for the Theory of Trees
Having explained how to analyze finitely generated sorts, we can now describe how the simplification procedure from [4] is extended to finitely generated sorts. Before going into detail, we provide a brief outline of this algorithm. The procedure works on special formulae, called normal formulae. Any formula can be transformed into an equivalent normal formula, so this is not a restriction. Roughly speaking, the output of our algorithm is a disjunction of fully simplified formulae that is equivalent to the original formula. A fully simplified formula makes it easy to read off all its models. The simplification algorithm works similarly to [4], except for the fact that finitely generated sorts sometimes require case splits (also called instantiations) for certain variables (called instantiable). These case splits can be on the finitely many generators of a sort, or on the finitely many (finite or infinite) inhabitants of a sort if it is in S FF or S FI . In this section, we focus on these instantiable variables and case splits because it is the novel part of our extension of [4]. The full algorithm is described in the appendix. Before we can start with the concept of normal formulae, we first need to define basic formulae.
whereū,v are variables and each t i is a variable or a term of the form f(z) for a function symbol f and variablesz. Such a formula will be abbreviated by v = t ∧ fin(u). Given a total order on its free variables, it is called solved if (1) the variablesū,v are distinct and for each equation x = y, we have x > y, and (2) if fin(v) occurs then the sort of v contains both finite and infinite trees. A variable x n is reachable from a variable x 0 if the basic formula contains The variable ordering is important when we consider basic subformulae of larger formulae. Then this ordering ensures that in solved basic formulae, variables bound more deeply inside the whole formula occur on the left-hand side of equations, which is important for the correctness proof. In order to offer some intuition for reachability: if y is reachable from x, this means that y is a subtree of x. Djelloul, Dao and Frhwirth describe an algorithm to solve a basic formula (rules 1-10 in [4]). In our extended setting, two things have to be changed: if fin(u) occurs in the basic formula where u : s with s ∈ S 0I , or s ∈ S 0F , then fin(u) is always satisfied and can be removed, or is never satisfied and the basic formula is unsolvable, respectively. This is summarized by the following theorem.

in the appendix) that correctly solves basic formulae α, i.e. it turns α into an equivalent solved formula (with respect to the given variable ordering) or returns false if none exists.
Basic formulae are insufficient for the general case but they are an important building block for the concept of normal formulae, which can express any first-order formula.
The simplest normal formula is ¬ true. As a normal formula allows expressing negation, conjunction, existential quantification and nesting, the following theorem is straightforward to prove [4][Property 4.3.3].
Theorem 5.4. There is an algorithm NORMALIZE(φ ) which turns any first-order formula φ into a normal one that is equivalent in the theory of trees.
Example 5.5. Consider the formula ∀x : nat.¬ fin(x) → x = succ(x). It can be rewritten as ¬(∃x : nat. ¬ fin(x) ∧ ¬(x = succ(x))), which is a normal formula of depth 2. Now we come to the main difference with the original algorithm from [4]: our more general setting necessitates case splits (or instantiations) for certain variables. For instance, consider the normal formula φ 1 ≡ ¬(∃x : list. ¬(x = nil) ∧ ¬(∃y, z. x = cons(y, z))). If list had infinitely many generators, it would always be possible to find a value for x that is neither nil nor cons. However, since list only has those two generators, no such x exists and the formula is true. Here our extended algorithm will do a case split on both constructors of list (described later in more detail) and realize that neither works.
As another example, consider . If t had infinitely many infinite trees, then this would be true because we could always choose a valuation for x that is different from the free variables y and z. Since t has only two infinite trees, our extended algorithm does a case split on all two infinite trees of t, instantiating x with g2(true, u nat ) and g2(false, u nat ) where u nat is the unique tree of sort nat, namely succ(succ(. . . )). A similar case occurs with a constraint fin(x) where x only has finitely many finite trees or, in general, if x has only finitely many trees. This leads us to the definition of an instantiable variable, i.e. a variable that requires a case split.
Note that every normal formula can be transformed into an equivalent one of depth at most 2 by repeatedly applying rule 16 (depth reduction) from [4, section 4.6]. Therefore we can limit our attention to such formulae in the following. Definition 5.6 (instantiable variable). Let ¬∃x. α ∧ i ¬(∃ȳ i . β i ) be a normal formula of depth at most 2 such that each α and β i are solved basic formulae. Let β * i be β i with all conjuncts also occurring in α removed. Then a variable v : s that is free in the formula or occurs inx is called instantiable if one of the following conditions is satisfied: 1. s has finitely many generators F s and some β * and α contains no equation v = t for any term t, or 3. s ∈ S FF , α contains fin(v), and some β * i contains v, or 4. s ∈ S FI and some β * j contains only fin()-constraints, among them fin(v).

Algorithm 3 Algorithm for finding instantiable variables and their instantiations.
if s has finitely many generators, and u = f(z) occurs in some β * i , and u is not properly reachable from u in β i then if s ∈ S FF and u occurs in some β * i , and fin(u) in α then return {u = t | t ∈ s fin } if s ∈ S FI and fin(u) occurs in some β * j that contains only fin()-constraints then Algorithm 3 looks for an instantiable variable (if any) in a normal formula ¬(∃x. α ∧ i φ i ) with free variablesv by checking exactly the four conditions from above. If it finds an instantiable variable u, it returns a set I of formulae, called instantiations. Note that while we write "u = t", which is not a basic formula, in the return value for simplicity, we actually mean an equivalent formula ∃z. γ where γ is a basic formula. For instance, by u = c1(true), we mean ∃z. u = c1(z) ∧ z = true for a fresh variable z. We can use these instantiations to get rid of instantiable variables, as the following theorem explains.
Then φ is equivalent to the following conjunction of normal formulae, in which the variable u is no longer instantiable: Example 5.8. In the formula φ 1 ≡ ¬(∃x : list. ¬(x = nil) ∧ ¬(∃y, z. x = cons(y, z))) from above, x is instantiable because of condition 1. (Note that the reachability check in this condition is required to avoid infinite loops for recursive equations like x = cons(y, x).) Here FINDINSTANTIATION returns I = {x = nil; ∃y, z. x = cons(y, z)}. By the above theorem, φ 1 is equivalent to z)). Both existential subformulae obviously contain a contradiction, so the whole formula simplifies to ¬(false) ∧ ¬(false) and thus true.
which means x is either a finite tree or one of the two infinite trees g2(false, u nat ), g2(true, u nat ) where u nat is the unique tree with u nat = succ(u nat ). By the above theorem, φ 2 is equivalent to . The other parts of the simplification procedure (unchanged from [4]) simplify this to true ∧¬(∃u nat : t. u nat = succ(u nat ) ∧ ¬(y = g2(false, u nat )) ∧ ¬(z = g2(false, u nat )) ∧¬(∃u nat : t. u nat = succ(u nat ) ∧ ¬(y = g2(true, u nat )) ∧ ¬(z = g2(true, u nat )), where the variable x is removed because it is unreachable from the free variables. The resulting formula essentially expresses that y or z has to be equal to g2(false, u nat ); and that y or z has to be equal to g2(true, u nat ). In other words, they can only take on those two infinite values and have to be different. Note that the algorithm has not completed at this point yet because y and z are now instantiable by condition 1. We skip the following (less interesting) instantiations for space reasons.
At this point, we can introduce the notions of solved and fully simplified formulae, which make up the output of our extended simplification procedure. Definition 5.10. A normal formula φ ≡ ¬(∃x. α ∧ i ¬(∃ȳ i . β i )), of depth at most 2, is called solved if it satisfies the following properties.
1. Each β i and α are solved basic formulae with respect to a variable ordering u < v if the binding of v is more deeply nested than u, i.e. u is free where v is bound. 2. The equations of α are included in every β i . 3. Each β i contains at least one conjunct that does not occur in α. 4. There are no instantiable variables. 5. All the variablesx andȳ i are reachable from the variables that are free in the subformulae ∃x. α and ∃ȳ i . β i , respectively. A formula ψ is called fully simplified if ¬ψ is a solved normal formula. (This is an extension of the definition of "explicit solved form" in [4].) Example 5.11. The point of fully simplified formulae is that they're easy to interpret, i.e. it is easy to read of all possible models from them. For instance, consider the fully simplified formula ∃v. x = succ(v) ∧ v = y ∧ fin(y) ∧ ¬(∃w. y = succ(w) ∧ fin(w) ∧ fin(z)) Any model has to satisfy x = succ(y) and y has to be finite. To falsify the other part ∃w. y = succ(w) ∧ fin(w) ∧ fin(z), there are two options for the free variables y and z: (1) instantiate y with any finite tree with a root other than succ and z with any tree, or (2) instantiate y with any finite tree and z with any infinite tree. These are the only two classes of models for the above fully simplified formula. In general, the following holds about fully simplified formulae.
Theorem 5.12. Let φ be a fully simplified formula. If φ has no free variables then φ ≡ true. Otherwise both φ and ¬φ are satisfiable in the theory of trees.
The task of the main algorithm, is, given a formula φ , to return a disjunction of fully simplified formulae. Since each individual disjunct allows an easy description of its models, we can describe all possible models of φ . Theorem 5.13. There is an algorithm SOLVE(φ ) (Algorithm 5 in the appendix) that, given a formula φ , returns true, false, or a disjunction of fully simplified formulae that is equivalent to φ in the extended theory of trees. In particular, if φ is closed, it returns true or false.
Proof idea. The simplification procedure from [4] does not have to be changed a lot. We use the function SOLVEBASIC from Theorem 5.2 to solve basic formulae. Afterwards, the rules 11-14 and 16 from [4] ensure that the result is a disjunction of formulae satisfying conditions (1-3) of Definition 5.10. At this point, we make use of FINDINSTANTIATION and Theorem 5.7, to ensure that condition (4) is satisfied. After each such instantiation, the previous rules have to be applied again because conditions (1-3) may have been invalidated. These steps will not, however, invalidate condition (4). The nontrivial proof of the fact that these instantiations terminate can be found in the appendix. Avoiding infinite loops of instantiations is the reason for the complicated condition 1 in Definition 5.6. Finally, Rule 15 of the original algorithm [4] ensures that condition (5) is satisfied as well. The proof that this part is still correct in our more general setting is again nontrivial and can be found in the appendix.
Time complexity Regarding the performance of our extended algorithm, note that the original algorithm has non-elementary time complexity [4]. In fact, Vorobyov proved that deciding first-order formulae in the (ordinary) theory of trees already has non-elementary time complexity [16], so we cannot hope for an efficient algorithm for the extended theory of trees in the worst case.
Implementation In order to evaluate the performance in practice, we created a prototype implementation in Scala. Due to a lack of benchmarks involving formulae of trees, we took the tests set of the QF_DT (quantifier-free datatypes) suite of the SMT-LIB and transformed each instance to a formula in the extended theory of trees using the results from Section 3. Then we ran our extended simplification procedure on the transformed instances. Over 90% of them completed in less than 1 second and about 5% timed out after 10 seconds (more data in Table 1 in the appendix). While state-of-theart SMT solvers decide each QF_DT instance in a few milliseconds, our transformed instances are considerably harder because they contain quantifiers and can be significantly larger than the original ones. Furthermore, our prototype implementation obviously cannot compete with heavily optimized SMT solvers and leaves a lot of room for improvements: for instance, the normalization of formulae can be optimized, and heuristics for choosing which variable to instantiate (instead of picking the first one) could make a big difference. It nevertheless demonstrates that our algorithm has a reasonable performance on many practical instances. A web interface to our implementation can be found at http://mjolnir.cs.ox.ac.uk/trees-codata/.

Conclusion
We believe that the extended theory of trees is an interesting theory to study because of its decidability and connections with algebraic (co)datatypes. We have explained the complications arising from finitely generated sorts, which are necessary to apply it to (co)datatypes. The fact that we not only provide a decision procedure but a simplification procedure should make it easier to conduct further research on the theory of trees, such as investigating Craig interpolation.

A Omitted proofs from Section 3
Theorem (Theorem 3.2, repeated). The first-order theory of (co)datatypes is undecidable.
Proof of Theorem 3.2. The proof works by reduction from Post's correspondence problem. An instance of the problem is given by a finite set of pairs of bit strings {(x 1 , y 1 ), . . . , (x n , y n )}, i.e. each x i , y i ∈ {0, 1} * . A solution to such an instance is a nonempty finite sequence of indices i 1 , . . . , i k with each i j ∈ {1, . . . , n} such that The decision problem is to decide whether such a solution exists, and is famously undecidable [13]. Let {(x 1 , y 1 ), . . . , (x n , y n )} be an instance of the problem. In the following, we construct a signature and formula φ , which is satisfiable in the theory of datatypes if and only if the instance has a solution.
For the encoding, consider the following datatype declarations. data bool = true | false data bitstring = e | 0(tail 0 : bitstring) | 1(tail 1 : bitstring) data dummy = f(b 1 : bitstring, b 2 : bitstring) | g(h : bool) We have the usual definition of Booleans (true or false), bit strings are empty (e) or start with a 0 or with a 1, and the dummy datatype is just used to emulate uninterpreted functions: h(f(s, s ′ )) acts like an unspecified function on the bit strings s, s ′ because h is applied to the wrong constructor and the standard semantics leaves this case unspecified. In this proof, φ is constructed in such a way that h(f(s, s ′ )) = true holds if s, s ′ is a valid pair of bit strings that can be built out of the (x i , y i ).
First, for a bit string x, we write p x (t) for the bit string that prepends x to t. For example, if x = 101, p x (t) stands for 1(0(1(t))). Consider the following formulae.
First, φ 1 and φ 2 specify what pairs of bit strings can be constructed out of x i and y i , and finally φ 3 specifies that a solution to the instance exists. Hence we claim that φ :≡ φ 1 ∧ φ 2 → φ 3 is valid if and only if the given instance of Post's correspondence problem is solvable.
First, suppose φ is valid. Consider the model M where h is interpreted as follows: In this model, φ 1 and φ 2 are satisfied by construction, hence φ 3 is satisfied as well. This means there is an element u ∈ bitstring M such that h M (f M (u, u)) = true M . By the choice of M , this means that u = M (p x (e)) such that there are i 1 , . . . , i k with x = x i 1 . . . x i k and y = y i 1 . . . y i k , which means the given instance is solvable.
Conversely, suppose the instance of Post's correspondence problem has a solution i 1 , . . . , i k . Let M be a structure where φ 1 ∧ φ 2 is true. Let s j = x i 1 . . . x i j and t j = y i 1 . . . y i j . Then φ 1 ensures that h(f(p s 1 (e), p t 1 (e))) = true in M and φ 2 ensures that the induction step works and hence that h(f(p s j (e), p t j (e))) = true holds for all j, in particular for j = k. Set u = p s k (e). Since s k = t k is a solution to the instance, we have h(u, u) = true in M . Hence φ 3 also holds in M . Therefore φ is valid.
Since a formula is valid if and only if its negation is unsatisfiable, this proof also shows that the satisfiability problem of first-order formulae in the theory of datatypes is undecidable.
Note that in the proof, we never used the fact that a bitstring is finite, so the same proof works when replacing the above datatype declarations by codatatype declarations.
Theorem (Theorem 3.3, repeated). In the theory of (co)datatypes with default values, a given formula can be effectively transformed into an equivalent one without selectors.
Proof of Theorem 3.3. The transformation works in two steps. First, it ensures that selectors don't occur nested but instead only occur in equations of the form x = sel i C (t) for a variable x. Afterwards, it replaces such equations by an equivalent formula that doesn't contain selectors.
Step 1 The first step isolates selectors to simple equations. For every equation t = t ′ where one side contains a selector, do the following. If t = t ′ is of the form x = sel i C (s) for a variable x and a selectorfree term s then there is nothing to do. Otherwise, without loss of generality, assume that t contains a (nested) selector, so t can be written as r[sel i C (s)/x] for a term r where x is a fresh variable. Then rewrite , which is always equivalent in first-order logic. This process is repeated until no more changes can be made.
Step 2 Now the formula only contains selectors as part of equations of the form x = sel i C (s) where s is selector-free. Each such equation can be rewritten as wherev are fresh variables. This is equivalent because C is the default value for this selector. The first equivalence is simply a case split on ∃v. s = C(v), the second one just moves a quantifier outward and the last one uses the definition of selectors.

Theorem (Theorem 3.4, repeated). In the theory of (co)datatypes with standard semantics, a quantifierfree formula can be effectively transformed into an equisatisfiable one without selectors (but including quantifiers).
Proof of Theorem 3.4. The transformation works in two steps. The first step is similar to the previous proof and replaces every selector term by an existentially quantified fresh variable. The second step is different from before obviously, but is similar to Ackermann's reduction for uninterpreted functions [1] (see [6,Section 11.2.1] for an exposition).
Step 1 Let φ be the formula to transform. Let S be a set of equations, initially empty. As long as φ contains a selector term, pick one that doesn't contain any nested selector terms. Let that term be t ≡ sel i C (s). Replace t by a fresh variable v in φ and add the equation v = sel i C (s) to S. This is repeated until φ contains no more selector terms.
Step 2 Let φ be the formula after the first step and S = {v j = sel i j C j (s j ) | j ∈ {1, . . . , n}} the set of equations of selectors. For each j = 1, . . . , n define the following two formulae wherez are fresh variables for each j. The idea is that the ψ j 's specify that sel i C (C(z)) = z i and the χ j 's (which is also part of Ackermann's reduction) ensure functional consistency, i.e. that if the same selector is applied to equal terms then the results should be equal. The latter property is important if the selector sel i C is applied to a term that is not of the form C(. . . ) because then the result is unspecified but it still has to be consistent. Finally define ψ to be the following formula Let φ be the original formula and φ ′ be the result of step 1. We claim that ψ ∧ φ ′ , which does not contain selectors anymore, is equisatisfiable with φ .
First, suppose that φ is satisfiable. Let M be a model of φ . We modify it to M ′ satisfying Note that the first case is well-defined since there are no cyclic dependencies between the variablesv by the design of Step 1. Then M ′ satisfies each ψ j since the interpretation of sel i C in M (and hence M ′ ) has to satisfy the selector axioms. It also satisfies each χ j because M ′ (sel i C ) is a function that has to give the same result if applied to the same object.
Furthermore, it is not hard to see that M ′ satisfies φ ′ as well. First of all, M ′ satisfies φ because the variables v j don't occur in φ since they were assumed to be fresh and M ′ agrees with M on everything else. Also note that by construction of M ′ , every equation v j = sel Next, suppose that ψ ∧ φ ′ is satisfiable and let M be a model of it. We define a new model M ′ modifying the interpretation of the selectors such that it satisfies: by v j in φ ′ , the interpretations of φ and φ ′ are the same in M ′ . Hence φ is true of M ′ , and thus φ is satisfiable, which finishes the proof.

Theorem (Theorem 3.5, repeated). A selector-free formula in the theory of (co)datatypes can be effectively transformed into an equisatisfiable formula in the extended theory of trees.
Proof of Theorem 3.5. Without loss of generality, we can assume that the given formula φ contains only existential quantifiers, no universal ones, because ∀x.ψ can be replaced by ¬∃x. ¬ψ. Let φ ′ be the result of replacing each ∃v 1 , . . . , v n . ψ occurring in φ with ∃v 1 : s 1 , . . . , v n : s n .
Finally let u 1 : s 1 , . . . , u n : s n be the free variables of φ ′ . Set Then it is clear that each model of φ can be reduced to a model of φ ′′ by forgetting the interpretation of the selector functions because the interpretation of datatypes are finite trees, thus satisfying all the additional fin()-constraints. Conversely, each model of φ ′′ in the theory of trees can be extended to a model of φ by picking arbitrary selector functions. The fin()-constraints ensure that the interpretation of each datatype variable is a finite tree, so it is, in fact, a model of φ .

B Omitted proofs from Section 4
Note that we make the standard assumption that the first-order language of trees is well-founded, meaning that there is no infinite sequence s 0 , s 1 , . . . of sorts such that for all i ∈ N, there is a function symbol f i of arity f i : · · · × s i+1 × · · · → s i .
Proof of Theorem 4.1. The validity of the fixed point computations is implied by the following two lemmas.
Lemma B.1. The set S 0I of sorts without infinite trees is the least fixed point of the following function f : P(S) → P(S) where P(·) denotes the power set: Proof. It is clear that S 0I is a fixed point because for each generator g each parameter sort must only allow finite trees, i.e. be in S 0I , yielding f (S 0I ) = S 0I . We claim that any sort s containing only finite trees of depth ≤ d is included in the set f d+1 ( / 0). This is proved inductively. For d = 0, this means s contains only constant symbols. Then the condition ∀g : s 1 × · · · × s n → s ∈ F s : ∀i ∈ {1, . . . , n} : s i ∈ / 0 is vacuously true and s ∈ f ( / 0). For d ≥ 1, this means that the argument of each generator has depth at most d − 1. Hence by the induction hypothesis, all generator arguments have sorts in f d ( / 0). By the definition of f , this means that then s ∈ f ( f d ( / 0)), proving the claim. Hence S 0I = ∪ d∈ω f d+1 ( / 0), in other words, S 0I is the least fixed point of f . Note that the least fixed point is guaranteed to exist by the Knaster-Tarski theorem.

Lemma B.2. The set S 0F of sorts without finite trees is the greatest fixed point of the following function f : P(S) → P(S):
f (X ) := X \ {s ∈ S | ∃(g : s 1 × · · · × s n → s) ∈ F s : ∀i ∈ {1, . . . , n} : s i / ∈ X } Proof. It is clear that S 0F is a fixed point because a sort with a generator g where all parameter sorts of g allow finite trees cannot contain only infinite trees. Hence all such sorts must be excluded, which is what f does. Therefore S 0F = f (S 0F ). Note again that f is monotonic, so the greatest fixed point is guaranteed to exist by the Knaster-Tarski theorem. Similarly to the proof of Lemma B.1, it is easy to see by induction that any sort s containing a finite tree of depth d is excluded from the set f d+1 (S). Hence S 0F = ∩ d∈ω f d+1 (S), in other words, S 0F is the greatest fixed point of f . Proof. Why is S FF a fixed point? First, F infin s are generators that can only construct infinite trees. So any other generator (in F s \ F infin s ) can construct at least one finite tree. For there to be only finitely many finite trees in s, there have to be finitely many of the latter generators and for each such generator, each parameter sort s i must have only finitely many finite trees. This explains the definition of the function f . Note that f is monotonic, so the least fixed point is guaranteed to exist by the Knaster-Tarski theorem.
In fact, similarly to the proof of Lemma B.1, it is easy to see inductively that if a sort s has finitely many finite trees of depth at most d then s ∈ f d+1 ( / 0). Hence S FF = d∈ω f d+1 ( / 0), in other words, S FF is in fact the least fixed point of f . Lemma B.4. Let S 1I ⊆ S be the set of sorts such that each s ∈ S 1I has exactly one infinite tree. Then S 1I is the greatest fixed point of the following function f : P(S \ S 0I ) → P(S \ S 0I ): f (X ) := {s ∈ X | ∃(g : s 1 → s) ∈ F s : s 1 ∈ X ∧ (∀(g ′ : s ′ 1 × · · · × s ′ n → s) ∈ F s \ {g} : ∀i : s ′ i ∈ S 0I )} Furthermore, the equations U s that uniquely determine the unique infinite inhabitant u s of s ∈ S 1I are given by the least fixed point of f ′ (X s ) = X s ∪ {u s = g(u s 1 )} ∪ X s 1 where f ′ maps sets of terms to sets of terms, both indexed by s ∈ S 1I , and g : s 1 → s is the unique generator with s 1 ∈ S 1I . Proof. Why is S 1I a fixed point? If s has a unique infinite tree then it must start with some generator g ∈ F s . If g had more than one parameter then the choice of the other parameter would create at least two infinite inhabitants, contradiction. So g has only one parameter. Furthermore every other generator g ′ can only create finite trees because otherwise we would lose uniqueness of the infinite tree. The function f removes all sorts from X that do not satisfy these criteria. Hence S 1I is a fixed point.
Conversely, a sort s in the fixed point must have two distinct infinite trees and they have to differ at some finite depth d. Then s / ∈ f d+1 (S \ S 0I ) because f removes sorts that have more than one infinite inhabitant and if those two inhabitants differ at depth d this is detected after at most d + 1 applications of f . This can be proved by induction, similarly to the proof of Lemma B.1. Hence S 1I = d∈ω f d+1 (S \ S 0I ), in other words, S 1I is the greatest fixed point of f .
Why is U s a fixed point of f ′ ? The equation u s = g(u s 1 ) must be true by the above arguments. In order to describe u s 1 uniquely, we need the equations U s 1 as well. Thus the U s are a fixed point of f ′ . They are, in fact, the least fixed point because we are interested in the smallest set of equations describing the u s . Then without loss of generality, assume that b 1 is an infinite subtree. Since s 2 has at least two generators, the number of infinite inhabitants of s 1 is at most #s infin /2 < #s infin . By induction hypothesis, b 1 has the desired form. The same argument works for other infinite subtrees of a. For each finite subtree, there is a ground term describing it. Hence a has the desired form.
Next, suppose f has only one parameter, a = f(a 1 ). If s has another infinite tree a ′ = f ′ (a ′ 1 ) starting with a different function symbol f ′ then the sort of a 1 has less than #s infin infinite trees, and the induction hypothesis gives us the desired form for a 1 and thus for a. Otherwise, all infinite trees of s start with the same function symbol f. We can apply the same argument to a 1 and see that all the infinite trees of the sort of a 1 must have the form a 1 = f 1 (a 2 ). So there are two cases. Case 1: there is an a n such that a = f( f 1 (. . . f n−1 (a n ) . . . )) and either a n has more than one parameter or the sort of a n has two infinite trees starting with different generators. Then the induction hypothesis can be applied to a n as before, yielding the desired form also for a. Case 2: there is no such a n , meaning that the tree a is uniquely determined, as an infinite path of unary function symbols. But then s only contains one infinite tree, contradiction. So this case cannot occur.
Lemma B.6. Let S FI ⊆ S be the set of sorts such that each s ∈ S FI has only finitely many infinite trees. Let F infin s = {(g : s 1 × · · · × s n → s) | ∃i ∈ {1, . . . , n} : s i / ∈ S 0I } be the set of generators that can construct infinite trees. Then S FI is the least fixed point of the following function f : P(S) → P(S): where S 0I is the set of sorts with only finite trees and S 1I is the set of sorts with a unique infinite tree.
Proof. Why is S FI a fixed point? First of all, it is clear that S 0I ∪ S 1I ⊆ S FI . Furthermore, for the sort s to have finitely many infinite trees, there have to be finitely many generators F infin s that can construct infinite trees. Additionally, for each such generator g : s 1 × · · · × s n → s ∈ F infin s , there have to be finitely many infinite trees starting with g.
It is easier to describe the negation of this: If a generator g starts infinitely many infinite trees, there must be a parameter i such that s i contains infinite trees and one of the following: (1) s i containing infinitely many infinite trees or (2) one of the other s j containing infinitely many trees. In either case, this leads to infinitely many infinite trees starting with g. As a formula: ∃i ∈ {1, . . . , n} : The negation is what is written in the above function definition. This explains why S FI is a fixed point of f .
Next, we show that S FI is the least fixed point. Let s be a sort with finitely many infinite trees and a such a tree. By Lemma B.5, there is a term t a describing a, containing only variables u i : s i representing the unique infinite tree of s i . We always choose t a to be of minimal depth among those terms. By definition of f , each s i ∈ f ( / 0). Let a be the infinite tree in S FI such that its corresponding t a has maximal depth d. Then one can see inductively, as in the proof of Lemma B.1, that s ∈ f d+1 ( / 0). Hence S FI = d∈ω f d+1 ( / 0), in other words, S FI is in fact the least fixed point of f .

C Supplementary material for Section 5
In this section, when talking about reachability in a formula, we mean reachablility from the free variables of the formula. We are also going to need the Unique Solution Axiom (axiom 3 in [4]), which states that for any sequence of distinct variablesz and non-variable terms t i containing only the variablesx and z, we have ∀x. ∃!z.
Algorithm 4 Algorithm for solving a basic formula α with free variables v 0 < · · · < v n . The rules 1-10 are taken from [4]. The two rules in blue at the end are new. Throughout, u, v, x, y, z denote variables, f, g function symbols and t terms.
if α is fin(u) ∧ α ′ and u is properly reachable from u then return false ⊲ Rule 9 if α is fin(u) ∧ α ′ and u : s with s ∈ S 0F then return false ⊲ (*) until no changes in the last iteration return α Theorem (Theorem 5.2, repeated). The function SOLVEBASIC (v = v 0 < · · · < v n , α) from Algorithm 4 correctly solves basic formulae α, i.e. it turns α into an equivalent solved formula (with respect to the given variable ordering) or returns false if none exists.
Proof of Theorem 5.2. Most parts of the algorithm (the numbered rules) are taken from [4] and property (1) of solved basic formulae is proven correct there. The two additional rules (*) involve variables u : s where s is a sort without infinite, respectively finite, trees. Obviously, fin(u) is then always, respectively never, satisfied. Therefore property (2) of solved basic formulae holds as well.
Proof of Theorem 5.7. We first show that in each case, the result I of the call to FINDINSTANTIATION satisfies α → ψ∈I ψ.
For the first return statement in FINDINSTANTIATION, this is clear because if there are finitely many generators of s then one of them has to be used to construct a tree of sort s. For the second return statement, it is clear because u can have only finitely many values, so if I contains formulae describing each possible value then the disjunction over all of them must be true. For the third return statement, note that fin(u) occurs in α, so u has to be finite. Hence I only contains formulae describing each finite value of s, and we have fin(u) → ψ∈I ψ. Finally, consider the fourth return statement. The variable u has to represent either a finite tree, meaning fin(u) or one of the finitely many infinite trees in s. Again, we find that ψ∈I ψ holds.
Since α → ψ∈I ψ holds in each case, φ is equivalent to: By the construction of I, the instantiable variable u found in the algorithm is no longer instantiable in this transformed formula.
Theorem (Theorem 5.12, repeated). Let φ be a fully simplified formula. If φ has no free variables then φ ≡ true. Otherwise both φ and ¬φ are satisfiable in the theory of trees.
Proof of Theorem 5.12. The formula φ has the form First consider the case of no free variables. Then no variable can be reachable in ∃x. α, hence by condition (5) of Definition 5.10,x is empty. This implies that α is just true because it cannot mention any variables. The same argument applied to each ∃y i . β i means thatȳ i is empty and β i ≡ true. Since φ is fully simplified, each β i must include a conjunct not occurring in α. Hence I = / 0. Altogether, we have φ ≡ true If φ contains free variables, it is enough to find a valuation for the free variables such that φ is true in the theory of trees and another one such that φ is false in the theory of trees.
To find a valuation that makes φ false, consider the following: If α contains a free variable z, it can be made false like this.
• If α contains z = w, then z > w according to the variable ordering since α is solved. Hence w is also a free variable and α can be made false by instantiating z and w to different trees. • If z = f(w) occurs in α, it is enough to instantiate z to a tree not starting with f to make α false, which is always possible because each sort has at least two generators. • If w = t with t containing z occurs in α, this equation must be reachable in ∃x. α by condition (5) of Definition 5.10. This means that there is an equation of the form z ′ = . . . in α, with z ′ free and w reachable from z ′ . This situation was already handled in one of the previous two cases. • If fin(z) occurs in α, simply instantiate z to an infinite tree (which is possible by the modified definition of solved basic formula) to make α false. Otherwise, α contains no free variables, sox is empty and α is true by the same argument as before. Since φ contains a free variable, there must be a β i that contains a free variable, so is nonempty. Since β i is a solved basic formula, it is satisfiable by Lemma C.1. Hence there is a valuation of free variables that makes ¬∃ȳ i . β i false. Then the same valuation makes φ false.
Next, we want to find a valuation making φ true. Let β * i be β i with all conjuncts occurring in α removed. Our goal is to find a valuation of the free variables andx that makes α true and every ∃ȳ i . β * i false (since we cannot make the parts of β i that also occur in α false). Letx lhs me the variables from x that occur on the left-hand side of an equation in α. The valuation for these variables will be picked last because it is uniquely determined by the Unique Solutions Axiom, once the valuation for the other variables is chosen. So the equations of α are taken care of.
If fin(v) occurs in α then any equation v = f(w) occurring in any β i is automatically false because v has to be properly reachable from itself (otherwise v would be instantiable), but then v cannot be finite. So the only constraints on v on the left-hand side that we care about in β i are v = w i for other variables w i . In this case, each w i is also a free variable because v > w i by the variable ordering, and the sort of v has infinitely many finite trees because otherwise v would be instantiable. Thus it is always possible to find a valuation that contradicts all these finitely many equations of the form v = w i by picking a value for v that is different from the values picked for all the w i . This proves that we can always make α true.
Next, we do a case analysis on the β * i that have not been made false yet. By reachability, each β * i has to contain fin(v) or v = t for a free variable v. Then v / ∈x lhs by Definition 5.10 and we can assume that fin(v) does not occur in α because this case was already discussed above. For each such free variable v, we do the following case analysis: • Suppose there is a β * i that contains fin(v). If β * i also contains an equation, then the following cases apply and suffice to make it false. So suppose β * i only contains fin-constraints. Then the sort of v has infinitely many infinite trees because otherwise v would be instantiable. This makes the following cases work, by restricting the set of possible values for v to the set of infinite trees. Using such a value also makes fin(v), and thus β * i , false as desired.
• Suppose v = f(w) occurs in some β * i . Then v must be properly reachable from itself in β i because otherwise, it would be instantiable. If the sort of v had only finitely many trees then v would be instantiable, contradiction. Hence the sort of v has infinitely many trees. Since the previous cases are already handled, we can assume that the only constraints on v in all the β * j 's are of the form v = f(w) with v properly reachable from itself in β * j or v = w. Since the sort of v has infinitely many trees, it is possible to contradict all these constraints.
• Suppose v = w occurs in some β i . Since the previous cases are already handled, we can assume that the only constraints on v from the β * i 's are of the form v = w i for variables w i . Then each w i is also a free variable because v > w i by the variable ordering, and the sort of v has infinitely many trees because otherwise v would be instantiable. Thus it is always possible to find a valuation that contradicts all these finitely many equations of the form v = w i by picking a value for v that is different from the values picked for all the w i . This case analysis shows that we can make all the β * i false. Thus it is always possible to find a valuation that makes φ true, as desired.
Lemma C.1. Any solved basic formula is satisfiable.
Proof. Let the basic formula be given by v = t ∧ fin(u). By the condition (2) of solved basic formulae (Definition 5.1), eachū can be given the value of some finite tree. Since the variablesv andū are disjoint, the Unique Solution Axiom tells us that ∃v. v = t is satisfiable for this valuation ofū.
Theorem (Theorem 5.13, repeated). Given a formula φ , the function SOLVE(φ ) from Algorithm 5 returns true, false, or a disjunction of fully simplified formulae that is equivalent to φ in the extended theory of trees. In particular, if φ is closed, it returns true or false.
Proof of Theorem 5.13. The proof of this is quite involved and will take up the rest of this section. The function SOLVE(φ ) first normalizes ¬φ and then solves its basic formula. If the latter contains a contradiction, φ is unsatisfiable. Otherwise, the function SOLVENESTED recursively solves ¬φ : it returns a set of solved normal formulae {ψ 1 , . . . , ψ n } such that ¬φ is equivalent to n i=1 ψ i . It works very similarly to the original algorithm in [4]. The only change is the instantiation step, highlighted in Algorithm 5.
The following lemmas prove the correctness of this change. Lemma C.3 establishes the termination of repeated instantiation steps. The termination of the unchanged parts of the original algorithm is shown in [4]. The fact that the instantiation step is correct was proven in Theorem 5.7 already. Next, Lemma C.4 proves that the properties (1) to (4) of a solved formula (Definition 5.10) are satisfied when REMOVEUNREACHABLEPARTS is called. Lemma C.5 proves that the return value of REMOVEUN-REACHABLEPARTS is correct. By construction, it satisfies property (5) as well, thus it is solved.
Since the return value of SOLVENESTED is a set of solved normal formulae {ψ 1 , . . . , ψ n } such that ¬φ is equivalent to n i=1 ψ i , φ is equivalent to n i=1 ¬ψ i . In particular, if n = 0 then φ is always false. Conversely, if each ψ i is ¬ true then φ is always true. In all other cases, we remove subformulae that were duplicated by Rule 12 in SOLVENESTED and return the whole disjunction.
To prove the termination of repeated instantiations, we need the following concept. Definition C.2 (depth). Let α be a solved basic formula. The depth of a variable v in α, denoted by depth α (v), is defined as follows. If v is properly reachable from itself or doesn't occur on the lefthand side of an equation in α, its depth is 0. Else if v = f(w) occurs in α, its depth is depth α (v) := 1 + max i (depth α (w i )). Else if v = w occurs in α, its depth is depth α (v) := depth α (w).

24
The Extended Theory of Trees and Algebraic (Co)datatypes Algorithm 5 Extension of Djelloul, Dao, and Frhwirth's algorithm [4] for transforming a normal formula into an equivalent conjunction of solved formulae. The added part is in blue.