{'fraction_non_alphanumeric': 0.04898650938919395, 'fraction_numerical': 0.007335095925699952, 'mean_word_length': 4.0486686289273734, 'pattern_counts': {'":': 0, '<': 8, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 78, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Automated Induction for Complex Data Structures

We propose a procedure for automated implicit inductive theorem proving for equational specifications made of rewrite rules with conditions and constraints. The constraints are interpreted over constructor terms (representing data values), and may express syntactic equality, disequality, ordering and also membership in a fixed tree language. Constrained equational axioms between constructor terms are supported and can be used in order to specify complex data structures like sets, sorted lists, trees, powerlists... Our procedure is based on tree grammars with constraints, a formalism which can describe exactly the initial model of the given specification (when it is sufficiently complete and terminating). They are used in the inductive proofs first as an induction scheme for the generation of subgoals at induction steps, second for checking validity and redundancy criteria by reduction to an emptiness problem, and third for defining and solving membership constraints. We show that the procedure is sound and refutationally complete. It generalizes former test set induction techniques and yields natural proofs for several non-trivial examples presented in the paper, these examples are difficult to specify and carry on automatically with related induction procedures.


Introduction
Given a specification R of a program or system S made of equational Horn clauses, proving a property P for S generally amounts to show the validity of P in the minimal Herbrand model of R, also called initial model of R (inductive validity). In this perspective, it is important to have automated induction theorem proving procedures supporting a specification language expressive enough to axiomatize complex data structures like sets, sorted lists, powerlists, complete binary trees, etc. Moreover, it is also important to be able to automatically generate induction schemas used for inductive proofs in order to minimize user interaction. However, theories of complex data structures generate complex induction schemes, and the automation of inductive proofs is therefore difficult for such theories.
It is common to assume that R is built with constructor function symbols (to construct terms representing data) and defined symbols (representing the operations defined on constructor terms). Assuming in addition the sufficient completeness of R (every ground (variable-free) term is reducible, using the axioms of R, to a constructor term) and the termination of R, a set of representants for the initial model of R (the model in which we want to proof the validity of conjectures) is the set of ground constructor terms not reducible by R C (the subset of equations of R between terms made of constructor symbols), called constructor normal forms.
In the case where the constructors are free (R C = ∅), the set of constructor normal forms is simply the set of ground terms built with constructors and it is very easy in this case to define an induction schema. This situation is therefore convenient for inductive reasoning, and many inductive theorem provers require free constructors, termination and sufficient completeness. However, it is not expressive enough to define complex data structures. With rewrite rules between constructors, the definition of induction schema is more complex, and requires a finite description of the set of constructor normal-forms. Some progress has been done e.g. in [5] and [6] in the direction of handling specification with non-free constructors, with severe restrictions (see related work below).
Tree automata (TA) with constraints, or equivalently regular tree grammars with constraints, have appeared to be a well suited framework for the decision of problems related to term rewriting (see [10] for a survey). This is the case for instance of ground reducibility, the property that all the ground instances of a given term are reducible by a given term rewriting system (TRS). This property was originally shown decidable for all TRS by David Plaisted [26]; it is reducible to the (decidable) problem of emptiness for tree automata with disequality constraints (see e.g. [11]). TA with constraints permit a finite representation of the set of constructor normal-forms when R C is a left-linear TRS (set of rewrite rules without multiple occurrences of variables in their left-handsides). Indeed, on one hand TA can do linear pattern-matching, hence they can recognize terms which are reducible by R C , and on the other hand, the class of TA languages is closed under complementation. When the axioms of R C are not linear, or are constrained, some extensions of TA (or grammars) are necessary, with transitions able to check constraints on the term in input, see e.g. [10].
In this paper, we propose a framework for inductive theorem proving for theories containing constrained rewrite rules between constructor terms and conditional and constrained rewrite rules for defined functions. The key idea is a strong and natural integration of tree grammars with constraints in an implicit induction procedure, where they are used as induction schema. Very roughly, our procedure starts with the automatic computation of an induction schema, in the form of a constrained tree grammar generating constructor normal form. This grammar is used later for the generation of subgoals from a conjecture C, by the instantiation of variables using the grammar's production rules, triggering induction steps during the proof. All generated subgoals are either deleted, following some criteria, or they are reduced, using axioms or induction hypotheses, or conjectures not yet proved, providing that they are smaller than the goal to be proved. Reduced subgoals become then new conjectures and C becomes an induction hypothesis. Moreover, constrained tree grammars are used as a decision procedure for checking the deletion criteria during induction steps.
Our method subsumes former test set induction procedures like [7,2,5], by reusing former theoretical works on tree automata with constraints. It is sound and refutationally complete (any conjecture that is not valid in the initial model will be disproved) when R is sufficiently complete and the constructor subsystem R C is terminating. Without the above hypotheses, it still remains sound and refutationally complete for a restricted kind of conjectures, where all the variables are constrained to belong to the language of constructor normal forms. This restriction is expressible in the specification language (see below). When the procedure fails, it implies that the conjecture is not an inductive theorem, provided that R is strongly complete (a stronger condition for sufficient completeness) and ground confluent. There is no requirement for termination of the whole set of rules R, unlike [7,2], but instead only for separate termination of the respective sets of rules for defined function and for the constructors.
Moreover, if a conjecture C restricted as above is proved in a sufficiently complete specification R and R is further consistently extended into R ′ with additional axioms for specifying partial (non-constructor) functions, then the former proof of C remains valid in R ′ , see Section 7.
The support of constraints permits in some cases to use the constrained completion technique of [23] in order to transform a non-terminating theory into a terminating one, by the addition of ordering constraints in constructor rules, see Section 5.6. It permits in particular to make proofs modulo non orientable axioms, without having to modify the core of our procedure.
We shall consider a specification of ordered lists as a running example throughout the paper. Consider first non-stuttering lists (lists which do not contain two equal successive elements) built with the constructor symbols ∅ (empty list) and ins (list insertion) and following this rewrite rule: ins(x, ins(x, y)) → ins(x, y) (c 0 ) Rewrite rules can be enriched with constraints built on predicates with a fixed interpretation on ground constructor terms. For example, using ordering constraints built with ≻ we can specify ordered lists by the following axiom: ins(x 1 , ins(x 2 , y)) → ins(x 2 , ins(x 1 , y)) x 1 ≻ x 2 (c 1 ) Another interesting example is the case of membership constraints of the form x : L where L is a fixed regular tree language (containing only terms made of constructor symbols). Such constraints can be useful in the context of system verification. Assume that we have specified a defined symbol trace characterizing the set of possible sequences of events of some system i.e. trace(ℓ) reduces to true iff ℓ is a correct list of events (represented as constructor terms). Now, assume also that we have defined a regular language Bad (of ground constructor terms) representing lists of faulty events, by mean e.g. of a (finite) tree grammar. We can express in this way, for instance, that some undesirable event occurs eventually, or that some event is always followed (eventually) by an expected answer, or any kind of linear temporal property. We can express with the constrained conjecture trace(y) = true y : Bad that no bad list is a trace of the system. Hence, showing that this conjecture is an inductive consequence of the specification of the system amounts to do verification of trace properties (i.e. reachability properties). More details about this problematic, in the context of security protocol verification, are given in Section 3.7.
We consider also stronger constraints which restrict constructor terms to be in normal form (i.e. not reducible by the axioms). Let us come back to the example of non-stuttering sorted lists (sorted lists without duplication), and add to the above rules the axioms below which define a membership predicate ⋐, using the information that lists are sorted: The constraint y 1 :NF expresses the fact that this subterm is a constructor term in normal form, i.e. that it is a sorted list. Without this constraint, the specification would be inconsistent. Indeed, let us consider the ground term t = 0 ⋐ ins(s(0), ins(0, ∅)). This term t can be reduced into both true and false, since ins(s(0), ins(0, ∅)) is not in normal form. In Section 3, we elaborate on these examples on sorted lists. Using constraints of the form . : NF as above also permits the user to specify, directly in the rewrite rules, some ad-hoc reduction strategies for the application of rewriting. Such strategies include for instance several refinements of the innermost strategy which corresponds to the call by value computation in functional programming languages, where arguments are fully evaluated before the function application.
Some non-trivial examples, including the above one, treated with our method are given in Section 3 (sorted lists and verification of trace properties) and Section 7 (powerlists). Our procedure yields very natural and readable proofs on these examples which are difficult (if not impossible) to specify and to carry on with the most of the other induction procedures.
Related work. The principle of our procedure is close to test-set induction approaches [7,2]. The real novelty here is that test-sets are replaced by constrained tree grammars, the latter being more precise induction schemes. Indeed, they provide an exact finite description of the initial model of the given specification, (under some assumptions like sufficient completeness and termination for axioms), whereas cover-sets and test-sets are over-approximative in similar cases.
The soundness of cover-set [30] and test-set [7,2] induction techniques do not require that the constructors are free. But, in this case, cover-sets and test-sets are over-approximating induction schemas, in the sense that they may represent some reducible ground terms. This may cause the failure (a result of the form "don't know") of the induction proof. On the other hand, the refutational completeness of test-set induction technique is not guaranteed in this case.
The first author and Jouannaud [5] have used tree automata techniques to generalize test set induction to specifications with non-free constructors. This work has been generalized in [6] for membership equational logic. These approaches, unlike the procedure presented in this paper, work by transforming the initial specification in order to get rid of rewrite rules for constructors. Moreover, the axioms for constructors are assumed to be unconstrained and unconditional left-linear rewrite rules, which is still too restrictive for the specification of structures like sets or sorted lists...
The theorem prover of ACL2 [22] is a new version of the Boyer-Moore theorem prover, Nqthm. Its input language is a subset of the programming language Common LISP. It is a very general formalism for the specification of systems, and therefore permits in particular the specification of complex data structures mentioned above. The example of sorted lists, presented in Section 3 can be processed with ACL2, but the proof requires the user to add manually some lemmas, whereas the proof with our procedure does not require any lemma (see Section 3.5). The specification language of our approach is much less expressive than the one of ACL2, but the intention is to minimize the interaction with the user during the proof process, in order to prevent the user from time consumption and the good level of expertise (both in the system to be verified and in the theorem prover) which are often required in order to come up with the necessary key lemmas. An interactive proof on the same specification with SPIKE is also presented in Section 3.
Kapur [20] has proposed a method (implemented in the system RRL) for mechanizing cover set induction if the constructors are not free. He defines particular specifications which may include in the declaration of function symbols (including constructors) some applicability conditions. This handles in particular the specification of powerlists, as illustrated by some examples. We show in Section 7 how our method can address similar problems.
In [27], Sengler proposes a system INKA for automated termination analysis of recursively defined algorithm over data types like sets and arrays. It can handle constructor relations, under restrictions. When it succeeds, this method provides an explicit induction scheme which can be exploited with an explicit inductive theorem proving procedure.
We lack a concrete base of comparison between our method and the two above approaches, because it was impossible for us to process our examples with INKA (which is discontinued since 1997) or RRL. Let us outline some other important differences between our procedure and these approaches. The above explicit induction procedures are not well suited for the refutation of false conjectures. When such a system fails, it is not possible to conclude whether the conjecture is not valid or if the system need assistance from the user in order to complete the proof. On the opposite, our implicit induction procedure is refutationally complete: any false conjecture will be refuted, under the assumptions mentioned above. This property is of particular interest for debugging specifications of flawed systems or programs or also for the detection of attacks on security protocols like in [3] (see Section 3.7). Finally, unlike explicit induction systems which are hierarchical, our procedure supports mutual induction. It is crucial for handling mutually recursive functions [2].

Preliminaries
The reader is assumed familiar with the basic notions of term rewriting [16] and first-order logic. Notions and notations not defined here are standard. Terms and substitutions. We assume given a many sorted signature (S, F ) (or simply F , for short) where S is a set of sorts and F is a finite set of function symbols with arities. We assume moreover that the signature F comes in two parts, F = C ⊎ D where C a set of constructor symbols, and D is a set of defined symbols. Let X be a family of sorted variables. We sometimes denote variables with sort exponent like x S in order to indicate that x has sort S ∈ S. The set of well-sorted terms over F (resp. constructor well-sorted terms) with variables in X will be denoted by T (F , X ) (resp. T (C, X )). The subset of T (F , X ) (resp. T (C, X )) of variable-free terms, or ground terms, is denoted T (F ) (resp. T (C)). We assume that each sort contains a ground term. The sort of a term t ∈ T (F , X ) is denoted sort (t).
A term t is identified as usual with a function from its set of positions (strings of positive integers) Pos(t) to symbols of F and X , where positions are strings of positive integers. We denote the empty string (root position) by Λ. The length of a position p is denoted |p|. The depth of a term t, denoted d (t), is the maximum of {|p| | p ∈ Pos(t)}. The subterm of t at position p is denoted by t| p . The result of replacing t| p with s at position p in t is denoted by t[s] p . This notation is also used to indicate that s is a subterm of t, in which case p may be omitted. We denote the set of variables occurring in t by var (t). A term t is linear if every variable of var (t) occurs exactly once in t.
A substitution is a finite mapping {x 1 → t 1 , . . . , x n → t n } where x 1 , . . . , x n ∈ X and t 1 , . . . t n ∈ T (F , X ). As usual, we identify substitutions with their morphism extension to terms. A variable renaming is a substitution mapping variables to variables. We use postfix notation for substitutions application and composition. A substitution σ is grounding for a term t if tσ is ground. The most general common instance of some terms t 1 , . . . , t n is denoted by mgi(t 1 , . . . , t n ).
Constraints and constrained terms. We assume given a constraint language L, which is a finite set of predicate symbols with a recursive Boolean interpre-tation in the domain of ground constructor terms of T (C). Typically, L may contain the syntactic equality . ≈ . (syntactic disequality . ≈ .), some (recursive) simplification ordering . ≺ . on ground constructor terms (for instance a lexicographic path ordering [16]), and membership . :L to a fixed tree language L ⊆ T (C) (like for instance the languages of well sorted terms or constructor terms in normal-form). Constraints on the language L are Boolean combinations of atoms of the form P (t 1 , . . . , t n ) where P ∈ L and t 1 , . . . , t n ∈ T (C, X ). By convention, an empty combination is interpreted to true.
The application of substitutions is extended from terms to constraints in a straightforward way, and we may therefore define a solution for a constraint c as a (constructor) substitution σ grounding for all terms in c and such that cσ is interpreted to true. The set of solutions of the constraint c is denoted sol (c). A constraint c is satisfiable if sol (c) = ∅ (and unsatisfiable otherwise).
A constrained term t c is a linear term t ∈ T (F , X ) together with a constraint c, which may share some variables with t. Note that the assumption that t is linear is not restrictive, since any non linearity may be expressed in the con- where the variable x ′ does not occur in c.

Constrained clauses.
A literal is an equation s = t or a disequation s = t or an oriented equation s → t between two terms. A constrained clause C c is a disjunction C of literals together with a constraint c. A constrained clause C c is said to subsume a constrained clause C ′ c ′ if there is a substitution σ such that Cσ is a sub-clause of C ′ and c ′ ∧ ¬cσ is unsatisfiable.
A tautology is a constrained clause s 1 = t 1 ∨ . . . ∨ s n = t n d such that d is a conjunction of equational constraints, d = u 1 ≈ v 1 ∧ . . . ∧ u k ≈ v k and there exists i ∈ [1.
.n] such that s i σ = t i σ where σ is the mgu of d.

Orderings.
A reduction ordering is a well-founded ordering on T (F , X ) monotonic wrt contexts and substitutions. A simplification ordering is a reduction ordering which moreover contains the strict subterm ordering. We assume from now on given a simplification ordering > total on T (F ), defined, e.g., on the top of a precedence as an lpo ≻ lpo [16].
The multiset extension > mul of an ordering > is defined as the smallest ordering relation on multisets such that M ∪ {t} > mul M ∪ {s 1 , . . . , s n } if t > s i for all i ∈ [1..n]. The extension > e of the ordering > on terms to literals is defined as the multiset extension > mul to the multisets containing the term arguments of the literals. The extension of the ordering > on terms to clauses is the multiset extension > mul e applied to the multiset of literals.
Constrained rewriting. A conditional constrained rewrite rule is a constrained clause of the form Γ ⇒ l → r c such that Γ is a conjunction of equations, called the condition of the rule, the terms l and r (called resp. left-and right-hand side) are linear and have the same sort, and c is a constraint. When the condition Γ is empty, it is called a constrained rewrite rule. A set of conditional constrained, resp. constrained, rules is called a conditional constrained (resp. constrained ) rewrite system.
Let R be a conditional constrained rewrite system. The relation s d rewrites to t d by R, denoted s d − − → R t d , is defined recursively by the existence of a rule ρ ≡ Γ ⇒ ℓ → r c ∈ R, a position p ∈ Pos(s), and a substitution σ such that s| p = ℓσ, t| p = rσ, dσ ∧ ¬cσ is unsatisfiable, and uσ ↓ R vσ for all u = v ∈ Γ . The transitive and reflexive transitive closures, Note the semantical difference between conditions and constraints in rewrite rules. The validity of the condition is defined wrt the system R whereas the interpretation of constraint is fixed and independent from R.
Otherwise s c is called irreducible, or an R-normal form. A substitution σ is irreducible by R if its image contains only R-normal forms. A constrained term t c is ground reducible (resp. ground irreducible) if tσ is reducible (resp. irreducible) for every irreducible solution σ of c grounding for t.
implies that v ↓ R w, and R is ground convergent if R is both ground confluent and terminating. The depth of a non-empty set R of rules, denoted d (R), is the maximum of the depths of the left-hand sides of rules in R.
Constructor specifications. We assume from now on given a conditional constrained rewrite system R. The subset of R containing only function symbols from C is denoted R C and R \ R C is denoted R D .
iff for all for all substitution σ grounding for C, R |= Cσ.
We shall need below to generalize the definition of inductive theorems to constrained clauses as follows: a constrained clause C c is an inductive theorem of R (denoted R |= Ind C c ) if for all substitutions σ ∈ sol (c) grounding for C we have R |= Cσ.

Completeness.
A function symbol f ∈ D is sufficiently complete wrt R iff for all t 1 , . . . , t n ∈ T (C), there exists t in T (C) such that f (t 1 , . . . , t n ) − − → + R t. We say that the system R is sufficiently complete iff every defined operator f ∈ D is sufficiently complete wrt R. Let f ∈ D be a function symbol and let: be a maximal subset of rules of R D whose left-hand sides are identical up to variable renamings µ 1 , . . . , µ n , i.e.
We say that f is strongly complete wrt R (see [2]) if f is sufficiently complete wrt R and R |= Ind Γ 1 µ 1 c 1 µ 1 ∨ . . . ∨ Γ n µ n c n µ n for every subset of R as above. The system R is said strongly complete if every function symbol f ∈ D is strongly complete wrt R.

Sorted Lists and Verification of Trace Properties
In this section, we present some examples for motivating the techniques introduced in this paper. These examples illustrate the fact that our approach supports constraints in the axioms (both for constructor and defined functions) and the conjectures. Note that constrained rules are not supported by test set induction procedures.

Constructor Specification, Normal Form Grammar
Consider a signature with sort S = {Bool, Nat, Set}, and constructor symbols: C = true, false : Bool, 0 : Nat, s : Nat → Nat, ∅ : Set, ins : Nat × Set → Set and a constructor rewrite system for ordered lists without duplication: Note the presence of constraints in these rewrite rules. The equality constraint in the first rule permits the elimination of (successive) redundancies in lists, and the ordering constraint in the second rule ensures that the application of this rule will sort the lists. Note that the first rule actually corresponds to the unconstrained rewrite rule: ins(x, ins(x, y)) → ins(x, y). As outlined in introduction, this rule cannot be handled by the procedures of [5,6], because it is not not left-linear. Constrained grammar are presented formally in Section 4. In this section, we shall only give a taste of this formalism and how their are used in the automatic inductive proof of conjectures. The set of ground R C -normal forms is described by the following set of patterns: We build a constrained grammar G NF (R C ) which generates NF(R C ) by means of non-terminal replacement guided by some production rules. The four first subsets of NF(R C ) are generated by a tree grammar from the four non-terminals: x Bool , x Nat , x Set , ins(x, y) and using the production rules (the non terminals are considered below modulo variable renaming): x Bool := true x Bool := false x Nat := 0 x Nat := s( x 2 Nat ) For the last subset of NF(R C ), we need to apply the negation of the constraint in the production rules of the grammar. For this purpose, we add the production rule: Note that the variables in the non terminal ins(x 2 , y 2 ) in the right member of the above production rule have been renamed in order to be distinguished from the variables in the non terminal in the left member.

Defined Symbols and Conjectures
We complete the above signature with the set of defined function symbols: and the conditional constrained TRS R D containing the following rules: Note that there is no axiom for the case x 1 x 2 . The defined function sorted is nevertheless sufficiently complete wrt R. We can show with an induction (on the size of the term) that every term t of the form sorted(ins(t 1 , ins(t 2 , ℓ))) can be reduced to a constructor term. If t 1 ≺ t 2 , then (s 2 ) applies and the term obtained is smaller than t. If and this latter term is furthermore reduced by the rule ( implements a membership test restricted to ordered lists. The function ∈ specified below another variant of a membership test on lists. Like sorted , the defined functions ∈ and ⋐ are sufficiently complete wrt R. The above version of the rule (m ′ 2 ) is the formal one (the version in introduction was given in a simplified notation). Note the presence of the membership constraint y 1 : ins(x 2 , y 2 ) in (m ′ 2 ). It refers to the above normal form grammar G NF (R C ) and hence restricts the variable y 1 to be a constructor term headed by ins and in normal form.
One may wonder why we added this membership constrained and why a rule would not be satisfying. The reason is that with the rule (m ′′ 2 ) instead of (m ′ 2 ), the specification is not consistent. Indeed, let us consider the ground term t = 0 ⋐ ins(s(0), ins(0, ∅)). Note that t is not in normal form. It can be rewritten on one hand into 0 ⋐ ins(0, ins(s(0), ∅)) by R C , which is in turn rewritten into true using (m ′ 1 ). On the other hand, t can be rewritten into false by (m ′′ 2 ). This second rewriting is not possible with (m ′ 1 ), because of the membership constraint in this rule.
Another idea to overcome this problem should be to add a condition as in: The specification with (m ′′′ 2 ) is inconsistent as well since the term t is rewritten by R C into sorted (ins(0, ins(s(0), ∅)), which is rewritten into true by R D . Therefore, the addition of the membership constraint in rule (m ′ 2 ) is necessary for the specification of ⋐.
Let us consider the two following conjectures that we are willing to prove by induction:

Test Set Induction
Roughly, the principle of a proof by test set induction [7,2] is the one presented in introduction except that: 1. the induction scheme is a test set (a finite set of terms). 2. variables in the goals are instantiated by terms from the test set.
Moreover, the instantiation in 2 can be restricted to so called induction variables (see [2]), which are the variables occurring (in a term of a goal) at a non-variable and non-root position of some left-hand sides of rules of R D . Let us try to prove (1) using the test set induction technique. A test set 3 for R (and sort Set) has to contain: We start by replacing y in (1) by the terms from the test set T S(Set, R), and obtain: Subgoals (3) and (4) are simplified by R D (respectively with rules (s 0 ) and (s 1 )) into true = true which is a tautology. Subgoal (5) cannot be simplified by R D , because of the constraints in rewrite rules. Subgoal (5) does not contain any induction variable, and therefore, it cannot be further instantiated. So, the proof stops without a conclusion. Hence, we fail to prove Conjecture (1) with test set induction technique.
Concerning Conjecture (2), the specification of the rules for ⋐ contains membership constraints. This kind of specification is not supported by the current test-set induction procedures.

Constrained Grammars based Induction
As discussed above, we need to add appropriate constraints while instantiating the induction goals. This is precisely what constrained tree grammars do.
Our procedure, presented in Section 5, roughly works as follows: given a conjecture C we try to apply the production rules of the normal form grammar to C (instead of instantiating by terms of a test set) as long as the depth of the clauses obtained is smaller or equal to the maximal depth of a left-hand-side of R D . All clauses obtained must be reducible by R, or by induction hypotheses or either by others conjectures not yet proved and smaller than C. If this succeeds, the clauses obtained after simplification are considered as new subgoals and for their proof we can use C as an induction hypothesis. Otherwise, the procedure fails and we have established a disproof under some assumptions on R.
In order to prove Conjecture (1), we constraint the variable y of this clause to belong to one of the languages defined by non-terminals (of a compatible sort) of the normal form grammar G NF (R C ). This is not restrictive since R C is terminating and R is sufficiently complete.
Let us apply the above principle to the proof of Conjecture (1). The application of the production rules of the grammar to (1.a) and (1.b) returns: For obtaining (4'), (5') and (5"), several steps of application of the production rules of the grammar are necessary. Subgoals (3'), (4') are simplified by R D into a tautology, like in Section 3.3. Unlike Section 3.3, Subgoal (5') can now be simplified using the rule (s 2 ) of R D , because of its constraint x 1 ≺ x 2 . Moreover, Subgoal (5") can be reduced by the rule (s 2 ) into: This latter subgoal can be itself simplified into true = true by (1), used here as an induction hypothesis. This terminates the inductive proof of (1).
For the proof of Conjecture (2), the situation is more complicated. The decoration of the variables of (2) with non terminals of the grammar G NF (R C ) returns: The application of the production rules of G NF (R C ) to these clauses gives: The clause (6) is reduced, using (m ′ 0 ) and (m 0 ), to the tautology false = false. In order to simplify (7), we restrict to the cases corresponding to the constraints of the rules (m ′ 1 ), (m ′ 2 ) and (m ′ 3 ). This technique, called Rewrite Splitting, is defined formally in Section 5. We obtain respectively: Note that the constraint in (7.2) implies that x 1 = x 2 . All these subgoal are reduced into tautologies true = true or false = false using respectively the following rules of R D : for the left member of (7.3), and (m 2 ) then (m 0 ) for its right member. The subgoal (8) is also treated by Rewrite Splitting with the rules (m ′ 1 ), (m ′ 2 ), (m ′ 3 ) of R D , similarly as above.
Let us now finish the proof of Conjecture (2), with the subgoal (9). By rewrite splitting with the rules (m ′ 1 ), (m ′ 2 ), (m ′ 3 ), we obtain: The subgoal (9.1) is simplified by (m 1 ) into the tautology true = true. The subgoal (9.3) is simplified by (m 2 ) into: At this point, we are allowed to use the goal (2) as an induction hypothesis since we have perform a reduction step on the subgoals. A simplification of (10) using (2) gives the tautology: For the subgoal (9.2), note that in the constraints, x ≺ x 4 implies x ≺ x 1 . Hence (9.2) can be simplified by (m 2 ) into: false = x ∈ ins(x 2 , y 2 ) . . . . A simplification of the above subgoal using (2) (as an induction hypothesis) gives: false = x ⋐ ins(x 2 , y 2 ) . . . . The above subgoal has the same constraints as (9.2), and it can be observed that this constraint implies x ≺ x 2 . Therefore, we can simplify this subgoal using (m ′ 2 ) into the tautology false = false. In conclusion, Conjecture (2) can be proved with our approach based on constrained grammars without the addition of any lemmas.

Proof with ACL2
A proof of Conjecture (2) was done by Jared Davis 4 with the ACL2 theorem prover, using his library osets for finite set theory [15]. In this library, sets are implemented on fully ordered lists (wrt an ordering <<). The definition in osets of a function insert a X, for insertion of an element a to a list X is the same as the above axioms of R C : (defun insert (a X) (declare (xargs :guard (setp X))) (cond ((empty X) (list a)) ((equal (head X) a) X) ((<< a (head X)) (cons a X)) (t (cons (head X) (insert a (tail X)))))) It refers to the functions head and tail which return respectively the first (smallest) element in list (the LISP car) and the rest of a list (LISP cdr). The guard (setp X) ensures that X is a fully ordered list without duplication.
The following lemma permits to finish the proof: (defthm head-minimal (implies (<< a (head X)) (not (in a X))) :hints(("Goal" :in-theory (enable primitive-order-theory)))) The lemma head-minimal was not available to users of the library osets. It will be incorporated (together with the technical lemma for its proof) in the appropriate file of the osets library.

Verification of Trace Properties
We have seen in the previous sections how membership constraints can be used in the axioms of R for the specification of operations on complex data structures, and how our method can handle it. Our procedure can also handle membership constraints in the conjecture. This feature can be used for instance in order to restrict some terms to a particular pattern. It is very useful in the context of the verification of infinite systems, in order to express that a trace of events belongs to a (regular) set of bad traces.
In [3] we follow this approach for the verification of security properties of cryptographic protocols, using an adaptation of the procedure of this paper in order to deal with specifications which are not necessarily confluent and sufficiently complete. In this section we wont describe in full details the specification of [3] but we shall roughly describe the main lines of the approach. Consider the following conjecture: Here, the membership constraint y: x List restricts y to be generated by the non terminal x List of the normal form constrained tree grammar. It means that y is a constructor term in normal form (as in the above example of sorted lists) representing a list of events of a system. The second membership constraint y: x Bad further restricts y to belong to a regular tree language representing faulty traces (traces which lead to a state of the system corresponding to a failure, an attack for instance). Finally the clause trace(y) = true expresses that y is not a trace of the system. Hence the above conjecture (11) means that every bad trace is not reachable. The defined function trace can be specified using constrained conditional rewrite rules. For instance, in [3], we follow the approach of Paulson [25] for the inductive specification of the messages exchanges of the protocol, and of the actions of the insecure communication environment. Note also that we extends this model with equations specifying the cryptographic operations, like the following non-left-linear equation for the decryption operator dec in a symmetric cryptosystem: dec enc(x, y), y → x. These axioms, sometimes referred as explicit destructors equations, permit a strict extension of the verification model (they allow strictly more attacks on protocols) and they are specified as constructor equations of R C in our model.

Constrained Tree Grammars
Constrained tree grammars have been introduced in [9], in the context of automated induction. The idea of using such formalism for induction theorem proving is also in e.g. [5,12], because it is known that they can generate the languages of normal-forms for arbitrary term rewriting systems.
In this paper, we push the idea one step beyond with a full integration of tree grammars with constraints in our induction procedure. Indeed, constrained tree grammars are used here: i. as an induction scheme (instead of test-sets), for triggering induction steps by instantiation of subgoals using production rules, ii. as a decision procedure for checking deletion criteria, including tests like ground irreducibility or validity in restricted cases, as long as emptiness is decidable.
iii. for the definition and treatment of constraints of membership in fixed tree languages, in particular languages of normal forms.
We present in this section the definitions and results suited to our purpose. The non-terminals are always considered modulo variable renaming. In particular, we assume wlog (for technical convenience) that the above term f (u 1 , . . . , u n ) is linear and that var (v) ∩ var (f (u 1 , . . . , u n )) = ∅.

Languages of Terms
We associate to a given constrained grammar G = (Q, ∆) a finite set of new unary predicates of constraint of the form . : u , where u ∈ Q (modulo variable renaming). Constraints of the form t: u called membership constraints and their interpretation is given below. The production relation between constrained terms ⊢ y G is defined by: . . . , u n ) = vτ , and y 1 ,. . . ,y n are fresh variables. The variable y, constrained to be in the language defined by the non-terminal v is replaced by f (y 1 , . . . , y n ) where the variables y 1 , . . . , y n are constrained to the respective languages of non-terminals u 1 , . . . , u n . The union of the relations ⊢ y G for all y is denoted ⊢ G and the reflexive transitive and transitive closures of the relation ⊢ G are respectively denoted by ⊢ * G and ⊢ + G (G may be omitted). Definition 2. The language L(G, u ) is the set of ground terms t generated by a constrained grammar G from a non-terminal u , i.e. such that y y: u ⊢ * t c where c is satisfiable. . , ins(s n k (0)))) | k ≥ 1, n 1 < . . . < n k }, 3 Note that every regular tree language L can be generated by a constrained tree grammar following Definitions 1 and 2, with production rules of the form: x S := f ( x S1 , . . . , x S1 ) where S 1 , . . . , S n , S are new sorts representing the non terminals of a regular tree grammar generating L.
The intersection between the language generated by a constrained tree grammar (in some non-terminal) and a regular tree language is generated by a constrained tree grammar. The constrained grammar for the intersection is built with a product construction.

Languages of Normal Forms
The constrained grammar G NF (R C ) = (Q NF (R C ), ∆ NF (R C )) defined in Figure 1 generates the language of ground R C -normal forms. Its construction is a generalization of the one of [11]. Intuitively, it corresponds to the complementation and completion of a grammar for R C -reducible terms (such a grammar does mainly pattern matching of left members of rewrite rules), where every subset of states (for the complementation) is represented by the most general common instance of its elements (if they are unifiable). For purpose of the the construction of G NF (R C ), a new sort Red is added to S, (the sort of reducible terms), and hence also a new variable x Red . An example of a constrained grammar for R C -normal  Figure 1: Constrained grammar G NF (R C ) for R C -normal forms forms constructed this way was given in Section 3.1.
Proof. We shall use the following Fact, which can be proved by a straightforward induction on the length of the derivation y y: u ⊢ * t c .
Let us now show the 'only if' direction by induction on the length of the derivation y y: u ⊢ * t c ′ (where c ′ is satisfiable).
If the length is 1, then t is a nullary symbol of C, and by construction t is R C -irreducible.
If y y: u ⊢ f (y 1 , . . . , y n ) y 1 : u 1 θ ∧ . . . ∧ y n : u n θ ∧cθ ⊢ * t c ′ = f (t 1 , . . . , t n ) c ′ for some production rule u := f ( u 1 , . . . , u n ) c ∈ ∆ NF (R C ) (θ is a variable renaming by fresh variables), then for every i ∈ [1..n], t i ∈ L(G NF (R C ), u i ), and u i = x Red (otherwise we would have u = x Red ). Hence, by induction hypothesis, every t i is a R C -normal form. Assume that t is R C -reducible (it must then be reducible at root position), and let l → r d ∈ R C be such that t = lτ , τ ∈ sol (d) and l is maximum wrt subsumption among the rules of R C satisfying these conditions. By construction, u = l and c = ¬dσ ∧ c ′ . It follows from the satisfiability of c ′ that τ ∈ sol (c) (the variables of c are instantiated by ground terms in the above grammar derivation). This is in contradiction with c = ¬dσ ∧ c ′ and τ ∈ sol (d).
We show now the 'if' direction by induction on t.
If t is a nullary function symbol of sort S and is R C -irreducible, then t is not the left-hand side of a rule of R C , and y y: x S ⊢ t.
If t = f (t 1 , . . . , t n ) and is R C -irreducible, then every t i is R C -irreducible for i ∈ [1..n], hence by induction hypothesis, .n], there is a derivation of G NF (R C ) of the form y y: u i ⊢ * t i c i . By Fact 1, every t i is an instance of u i , hence t = f (u 1 , . . . , u n )τ for some ground substitution τ . If there is a production rule u := f ( u 1 , . . . , u n ) c ∈ ∆ NF (R C ), with u ∈ Q NF (R C ) \ { x Red } and τ ∈ sol (c), then the following derivation is possible: y y: u ⊢ f (y 1 , . . . , y n ) y 1 : u 1 θ ∧ . . . ∧ y n : u n θ ∧cθ ⊢ * t c ′ where c ′ is satisfiable, and t ∈ L(G NF (R C ), u ). Assume that for every such production rule, we have τ ∈ sol (c). It means by construction that there is a rule u → r d ∈ R C such that τ ∈ sol (d), hence that t is R C -reducible, a contradiction. 2 Using the observation that every ground constructor term is generated by G NF (R C ), we obtain as a corollary that t ∈ L(G NF (R C ), x Red ) iff t is R Creducible.

Inference System
In this section, we present an inference system for our inductive theorem proving procedure. Let us first summarize the key steps of our procedure with the following pseudo-algorithm 6 . The complete inference system, introduced by the examples of Section 3, is presented in details in Subsections 5.2, 5.3 and 5.4.
We start with a conjecture (goal) G (a constrained clause) and a rewrite system (with conditions and constraints) R, with a subset R C of constructor constrained (unconditional) rewrite rules.
1. compute the constrained tree grammar G NF (R C ) 2. given a goal (or subgoal) C, generate instances of C by using the production rules of G NF (R C ). We obtain C 1 , . . . , C n . 3. for each C i , do: (a) if C i is a tautology or C i is a constructor clause and can be detected as inductively valid then delete it (b) else if we are in one of the two following cases: i. C i is a constructor clause and is reducible using R C , or ii. C i contains a non-constructor symbol and is reducible using R and induction hypotheses then reduce C i into C ′ i (c) else disproof (the initial conjecture is not an inductive theorem) 4. if 3 did not fail then C becomes an induction hypothesis i is a tautology or it is a constructor clause and can be detected as inductively valid or it is subsumed by an axiom or induction hypothesis then delete it (b) otherwise C ′ i becomes a new subgoal, go to 2.
If every subgoal is deleted, then G is an inductive theorem of R. The procedure may not terminate, and in this case appropriate lemmas should be added by the user in order to achieve termination. The deletion criteria (steps 3a and 5a) include tautologies, forward subsumption, clauses with an unsatisfiable constraint, and constructor clause and can be detected as inductively valid, under some conditions defined precisely below.The procedure for testing these criteria is based on a reduction to a tree grammar non-emptiness problem (does there exist at least one term generated by a given grammar), using G NF (R C ). In particular, it should be noted that we can decide validity this way for clauses C i which are ground irreducible [19,21] (a notion central in inductive theorem proving / proof by consistency). It is possible to decide ground irreducibility also by mean of reduction to non-emptiness, following the lines of [11]. In Section 6, we show how such tests can be achieved effectively, providing that R is ground confluent, for some classes of tree grammar with equality and disequality constraints studied in former works [1,8,14,11]. The extension to other kind of constraints (like e.g. ordering constraints) requires algorithms for corresponding classes of tree grammars (see discussions in Sections 7 and 8).
The reductions at step 3b are performed either with standard rewriting or with ind. contextual rewriting (case 3(b)ii) or by case analysis, (partial splitting in case 3(b)i and rewrite splitting in case 3(b)ii). These rules are defined formally in Sections 5.2 and 5.3.

Induction Ordering
The inference and simplification rules below rely on an ordering defined on the top of the following complexity measure on clauses.
Definition 3. The complexity of a constrained clause C c is the pair made of the two following components: C, ordered by the multiset extension of the ordering > e on literals, and the number of constraints dσ not occurring in c, such that there exists l → r d ∈ R C and lσ is a subterm of C.
We denote ≫ the ordering on constrained clauses defined as the lexicographic composition of the orderings on the two components on the complexities.

Simplification Rules for Defined Functions
Our procedure uses the simplification rules for defined symbols presented in Figure 2. The rules in this figure define the relation − − → H D for simplifying constrained clauses using R D , R and a given set H of constrained clauses considered as induction hypotheses.
Inductive Rewriting simplifies goals using the axioms of R D as well as instances of the induction hypotheses of H, provided that they are smaller than the goal. The underlying induction principle is based on the well-founded ordering ≫ on constrained clauses This approach is more general than structural induction which is more restrictive concerning simplification with induction hypotheses (see e.g. [7]). Inductive Contextual Rewriting can be viewed as a generalization of a rule in [29] to handle constraints by recursively discharging them as inductive conjectures. Rewrite Splitting simplifies a clause which contains a subterm matching some left member of rule of R D . This inference checks moreover that all cases are covered for the application of R D , i.e. that for each ground substitution τ , the conditions and the constraints of at least one rule is true wrt τ . Note that this condition is always true when R is sufficiently complete, and hence that this check is superfluous in this case. Inductive Deletion deletes tautologies and clauses with unsatisfiable constraints.

Simplification Rules for Constructors
The simplification rules for constructors are presented in Figure 3, they define the relation → C for simplifying constrained clauses using R C and R.
Rewriting simplifies goals with axioms from R C . Partial Splitting eliminates ground reducible terms in a constrained clause C c by adding to C c the negation of constraint of some rules of R C . Therefore, the saturated application of Partial splitting and Rewriting will always lead to Deletion or to ground irreducible constructor clauses. Finally, Deletion and Validity remove respectively tautologies and clauses with unsatisfiable constraints, and ground irreducible constructor theorems of R.

Induction Inference Rules
The main inference system is displayed in Figure 4. Its rules apply to pairs (E, H) whose components are respectively the sets of current conjectures and of inductive hypotheses. Two inference rules below, Narrowing and Inductive Narrowing, use the grammar G NF (R C ) for instantiating variables. In order to be able to apply these inferences, according to the definition of term generation in Section 4.1, we shall initiate the process by adding to the conjectures one membership constraint for each variable. The definition of decorate is extended to set of constrained clauses as expected.
A constrained clause C c is said decorated if c = d ∧ x 1 : u 1 ∧ . . . ∧ x n : u n where {x 1 , . . . , x n } = var (C), and for all i ∈ [1..n], u i ∈ Q NF (R C ), sort (u i ) = sort (x i ), and d does not contain membership constraints.
Simplification, resp. Inductive Simplification, reduces conjectures according to the rules of Section 5.3, resp. 5.2. Inductive Narrowing generates new subgoals by . . , Cn cn } is the set of all clauses such that C c ⊢ * Ci ci and d (Ci if no other rule applies to the clause C c Figure 4: Induction Inference Rules application of the production rules of the constrained grammar G NF (R C ) until the obtained clause is deep enough to cover left-hand side of rules of R D . Each obtained clause must be simplified by one the rules of Figure 2 (otherwise, if one instance cannot be simplified, then the rule Inductive Narrowing cannot be applied). For sake of efficiency, the application can be restricted to so called induction variables, as defined in [2] (see Section 3.3) while preserving all the results of the next section. Narrowing is similar and uses the rules of Figure 3 for simplification. This rule permits to eliminate the ground reducible constructor terms in a clause by simplifying their instances, while deriving conjectures considered as new subgoals. The criteria on depth is the same for Inductive Narrowing and Narrowing and is a bit rough, for sake of clarity of the inference rules. However, in practice, it can be replaced by a tighter condition (with, e.g., a distinction between R C and R D ) while preserving the results of the next section. Subsumption deletes clauses redundant with axioms of R, induction hypotheses of H and other conjectures not yet proved (in E).

Soundness and Completeness
We show now that our inference system is sound and refutationally complete. The proof of soundness is not straightforward. The main difficulty is to make sure that the exhaustve application of the rules preserve a counterexample when one exists. We will show more precisely that a minimal counterexample is preserved along a fair derivation.
A derivation is a sequence of inference steps generated by a pair of the form (E 0 , ∅), using the inference rules in I, written (E 0 , ∅) ⊢ I (E 1 , H 1 ) ⊢ I . . . It is called fair if the set of persistent constrained clauses (∪ i ∩ j≥i E j ) is empty or equal to {⊥}. The derivation is said to be a disproof in the latter case, and a success in the former.
Finite success is obtained when the set of conjectures to be proved is exhausted. Infinite success is obtained when the procedure diverges, assuming fairness. When it happens, the clue is to guess some lemmas which are used to subsume or simplify the generated infinite family of subgoals, therefore stopping the divergence. This is possible in principle with our approach, since lemmas can be specified in the same way as axioms are.
Theorem 1 (Soundness of successful derivations). Assume that R C is terminating and that R is sufficiently complete. Let D 0 be a set of unconstrained clauses and let E 0 = decorate(D 0 ). If there exists a successful derivation Proof. Assume that R |= Ind D 0 , and let (E 0 , ∅) ⊢ I (E 1 , H 1 ) ⊢ I · · · be an arbitrary successful derivation. By the following Fact, we have that R |= Ind E 0 .

Fact 2 Assume that R C is terminating and that
Proof. Assume that R |= Ind E 0 and that for some clause C ∈ D 0 we have Since R is sufficiently complete and R C is terminating, we can rewrite σ into a constructor and R C -irreducible ground substitution σ ′ . By Lemma 1, it follows that σ ′ ∈ sol (c i ) for some i ∈ [1..n], and therefore that R |= Cσ ′ , a contradiction with R |= Ind Cσ. 2 Let D 0 be a clause, minimal wrt ≫, in the set:

) is constructor and irreducible and R |= Dσ
Note that such a clause exists since we have proved that R |= Ind E 0 . Let C c be a clause of ∪ i E i minimal by subsumption ordering and θ ∈ sol (c), irreducible and constructor ground substitution, be such that Cθ = D 0 . We show that whatever inference, other than Disproof, is applied to C c , a contradiction is obtained, hence that the above derivation is not successful.
C c σ cannot be a tautology and c cannot be unsatisfiable and therefore the rule Inductive Deletion cannot be applied.
Let C ′ be the result of the application of the rule Inductive Rewriting to Cσ c ′ . The instances of clauses of H ∪ E ∪ {C} used in the rewriting step are smaller than Cθ wrt ≫, and therefore, they are inductive theorems of R. Hence R |= C ′ τ . Moreover, Cθ ≫ C ′ τ and C ′ ∈ ∪ i E i , which is a contradiction.
With similar arguments as above, we can show that the rule Inductive Contextual Rewriting cannot be applied to Cσ c ′ .
Assume that the rule Rewrite Splitting is applied to C[t] p σ c ′ . Let r 1 c 1 , . . . , Γ n ⇒ l n → r n c n } be the non-empty subset of R D such that for all i in [1..n], t = l i σ i and The result of the application of Rewrite Splitting is: On the other hand, Cθ ≫ C k δ since {t} > mul Γ k σ k , and t > r k σ k . This contradicts the minimality of Cθ.
Narrowing, Inductive Simplification and Simplification. These cases are similar to the previous one.
Subsumption: Since R |= Cθ, C c cannot be subsumed by an axiom of R. If there exists C ′ c ′ ∈ H ∪ (E \ {C c }) such that C c ≡ C ′ δ c ′ δ ∨ D, then we have R |= C ′ δθ (θ ∈ sol (c ′ )). Hence, r = ∅ and δ = ∅, since C c is minimum in ∪ i E i wrt subsumption ordering. Therefore, C ′ ∈ (E \ {C}). Moreover, C ′ ∈ H, otherwise the inference Inductive Narrowing or Narrowing could also be applied to C c , in contradiction with previous cases. Hence, Subsumption cannot be applied to C c . 2 Since there are only two kinds of fair derivations, we obtain as a corollary: Corollary 1 (Refutational completeness). Assume that R C is terminating and that R is sufficiently complete. Let D 0 be a set of unconstrained clauses and let E 0 = decorate(D 0 ). If R |= Ind E 0 , then all fair derivations starting from (E 0 , ∅) end up with (⊥, H).
When we assume that all the variables in goals are decorated (restricting the domain for this variables to ground constructor irreducible terms), the above hypotheses that R C is terminating and R is sufficiently complete can be dropped.
Proof. The proof is the same as for Theorem 1 except that we do no need the Fact 2 since the goals of E 0 are already decorated. Hence we do neither need the hypotheses that R C is terminating and that R is sufficiently complete which where only used for the proof of Fact 2. 2 As a consequence, of the above theorem, we immediately have the refutational completeness of our inference system if the goals are decorated constrained clauses.
Corollary 2 (Refutational completeness). Let E 0 be a set of decorated constrained clauses. If R |= Ind E 0 , then all fair derivations starting from (E 0 , ∅) end up with (⊥, H).
We shall see in Section 7 some example of applications of Theorem 2 and Corollary 2 to specifications which are not sufficiently complete.
Our inference system can refute false conjectures. This result is a consequence of the following lemma.
Proof. Let C c be a clause in E i and (E i ∪ {C c }, H i ) ⊢ I (E i+1 , H i+1 ) be a derivation step obtained by the application of an inference to C c and assume that R |= Ind E i ∪ H i . By hypothesis, the instances of clauses of H ∪ E ∪ {C c } which are used during rewriting steps, are valid. Hence, we can show that R |= Ind E i+1 ∪ H i+1 by a case analysis according to the rule applied to C c . 2 The following lemma is also used in the proof of soundness of disproof.
Lemma 3. If R is ground confluent and sufficiently complete then for every constructor clause C c , if R |= Ind C c then R C |= Ind C c .
Proof. Let τ ∈ sol (c) be a substitution grounding for C. By the sufficient completeness of R, we may assume without loss of generality that τ is a constructor substitution. By hypothesis, R |= Cτ . Assume that for some literal u = v of C, we have R |= uτ = vτ . Since R is ground confluent, it means that uτ ↓ R vτ , and hence that uτ ↓ RC vτ , i.e. R C |= uτ = vτ , because uτ, vτ ∈ T (C). Moreover, if R |= uτ = vτ then R C |= uτ = vτ because R C ⊆ R. 2 Theorem 3 (Soundness of disproof ). Assume that R is strongly complete and ground confluent. If a derivation starting from (E 0 , ∅) returns the pair (⊥, H), then R |= Ind E 0 .
Proof. Under our assumptions, there exists a step k in the derivation, such that Disproof applies to a constrained clause C c in E k . We prove first that C c is a constructor clause. Assume indeed that C c contains a term of the form f (t 1 , . . . , t n ), where f ∈ D and for all i ∈ [1..n], t i ∈ T (C, X ). The constraint c is satisfiable, otherwise Inductive Deletion could be applied. Let τ ∈ sol (c). Hence by Lemma 1, for each x ∈ var (C), xτ is in R C -normal form. We have now two possibilities: 1. for one i ∈ [1..n], t i τ is reducible. In this case, there exists a substitution σ such that τ = σθ and t i c ⊢ + t i σ c ′ and t i σ contains as a subterm an instance of a left-hand side of rule of R C . Therefore, either Rewriting or Partial Splitting can be applied to t i σ c ′ . It implies that Narrowing can be applied to C c , which is a contradiction. 2. every t i τ is irreducible. The term f (t 1 , . . . , t n )τ is reducible at root position because f is strongly complete wrt R. Then there exists σ such that τ = σθ and f (t 1 , . . . , t n ) c ⊢ + f (t 1 , . . . , t n )σ c ′ and moreover f (t 1 , . . . , t n )σ is an instance of a left-hand side of rule of R D . Therefore, either Inductive rewriting or Rewrite Splitting can be applied. Indeed the application condition of the latter inference is a consequence of the strongly completeness of R.
Hence, the inference Inductive Narrowing can be applied to C c , which is a contradiction.
In conclusion, the clause C c contains only constructor terms. Then, we deduce that C c contains ground irreducible terms only, otherwise Narrowing would apply. Since Validity does not apply either, C c is not an inductive consequence of R C . By lemma 3, and since R is ground confluent, we conclude that C c is not an inductive theorem of R. As a consequence, R |= Ind E k . Finally, by lemma 2, we deduce that R |= Ind E 0 . 2

Handling Non-Terminating Constructor Systems
Our procedure applies rules of R C and R D only when they reduce the terms wrt the given simplification ordering >. This is ensured when the rewrite relation induced by R C and R D is compatible with >, and hence that R C and R D are terminating (separately), like in the example of Section 3. Note that this is in contrast with other procedures like [7,2] where the termination of the whole system R is required. If R C is non-terminating then one can apply e.g. the constrained completion technique [23] in order to generate an equivalent orientable theory (with ordering constraints). The theory obtained (if the completion succeeds) can then be handled by our approach.

Decision Procedures for Conditions in Inference Rules
We present a reduction of the conditions in the inference rules of Figures 2, 3, and 4 to emptiness decision problems for tree automata with constraints. We deduce a decision procedure for these tests in the case where the constraints in the specification are limited to syntactic equality and disequality. We assume here that, like in Theorem 1, the inference system is applied to a set decorate(D 0 ) where D 0 is a set of unconstrained clauses.

Reductions
Consider the following decision problems, given two constrained grammars G, G ′ and two non terminals u , u ′ of respectively G and G ′ , Ground instances. Let t c be a constrained term (or clause) such that the constraint c has the form x 1 : u 1 ∧ . . . ∧ x m : u m ∧d where d contains no membership constraints. Note that starting with decorated clauses, any goal or subgoal occurring during the inference is of the above form. The set of ground instances of t satisfying c is recognized by a constrained grammar G(t c ) = Q(t c ), ∆(t c ) whose construction is described in Figure 5. For technical reasons concerning non-terminals separation, we use in the construction of G(t c ) a relabeling isomorphism • from the signature (S, F ) to the signature (S • , F • ), such that the function symbol f • has profile S • 1 × . . . × S • n → S • if f has profile S 1 ×. . .×S n → S, and its extension from T (F , X ) to T (F • , X), such that (recursively) f (t 1 , . . . , t n ) = f • (t • 1 , . . . , t • n ), and for each x ∈ X , x • = x.
xi: ui ∧d ) contains all the production rules of ∆NF(RC) plus:  Proof. The proofs of both directions ⊆ are straightforward inductions resp. on the length of a derivation of a term of L(G(t c ), t ) and on a ground instance tσ such that σ| var (c) is a solution of c. Ground (ir)reducibility. The rules Validity, hence Simplification, and Disproof (by negation) check ground irreducibility.
Lemma 6. Ground reducibility and ground irreducibility decision are reducible to (EI).
Proof. By definition and Lemmas 1 and 4, a constrained clause C c is ground Validity of ground irreducible constructor clauses. The rule Validity, hence Simplification, checks this property.
Lemma 7. When R is ground confluent, validity of ground irreducible constructor constrained clauses is reducible to (ED).
Proof. Let C c be a ground irreducible constructor constrained clause. LetC be the constraint obtained from C by replacement of every equation s = t (resp. disequation s = t) by the atom s ≈ t (resp. s ≈ t). Since C c is ground irreducible and R is ground-confluent, we have that C c is valid in the initial model of R iff every substitution σ ∈ sol (c) grounding for C is such that σ ∈ sol C . This is equivalent to L G(C c ∧ ¬C ) = ∅. 2

Decision
It remains to give decision procedures for (ED) and (EI). We proceed by reduction to analogous problems on tree automata with (dis)equality constraints [10], for a class of tree grammars defined as follows.

Handling Partial Specifications
The example of sorted lists in Section 3 can be treated with our procedure because it is based on a sufficiently complete and ground confluent conditional constrained TRS R whose constructor part R C is terminating. Indeed, under these hypotheses, Theorem 1 ensures the soundness of our procedure for proving inductive conjectures on this specification, and Corollary 1 and Theorem 3 ensure respectively refutational completeness and soundness of disproof. For sound proofs of inductive theorems wrt specifications which are not sufficiently complete, we can rely on Theorem 2 and Corollary 2 which do not require sufficient completeness of the specification but instead suppose that the conjecture is decorated, i.e. that each of its variables is constrained to belong to a language associated to a non-terminal of the normal-form (constrained) grammar. In this section, we propose two applications of this principle of decoration of conjectures to the treatment of partial specifications. We treat the case where the specification of defined function is partial in Section 7.1, and the case where axioms for constructors are partial in Section 7.2.

Partially Defined Functions
Under the condition that the conjecture is decorated, extending a given sufficiently complete specification with additional axioms for defining partial (defined) functions preserves successful derivations.
Theorem 5. Assume that R is sufficiently complete and let R ′ be an consistent extension of R where R C ′ = R C and R D ′ = R D ∪ R D ′′ (R D ′′ defines additional partial defined functions). Let E 0 be a set of decorated constrained clauses. Every derivation (E 0 , ∅) ⊢ I · · · successful wrt R is also a successful derivation wrt R ′ .
Proof. The grammars G NF (R C ′ ) and G NF (R C ) are the same. Therefore every inference step wrt R is also an inference step wrt R ′ . 2 We apply Theorem 5 to a partial extension of the specification of Section 3. Specification of min for sorted lists. Let us complete the specification of Section 3 with a new defined symbol min : Set → Nat and the following rules of R D : min(ins(x, ∅)) → x min(ins(x, ins(y, z))) → min(ins(x, z)) x ≺ y The function min is not sufficiently complete wrt R (the case min(∅) is missing). Proof of two conjectures for min. We shall prove, using our inference system, that the two following constrained and decorated conjectures are inductive theorems of R. min(ins(x, ins(y, z))) → min(ins(y, z)) x y ∧ x, y: x Nat ∧ z: x Set (12) min(ins(x, ins(y, z))) → min(ins(y, z)) x y ∧ x, y: x Nat ∧ z: Let us now prove that the conjecture (12) is an inductive theorem of R. We start by the simplification of (12) using a Partial Splitting. We obtain: min(ins(y, z)) = min(ins(y, z)) x ≈ y ∧ x y ∧ x, y: x Nat ∧ z: x Set (14) min(ins(x, ins(y, z))) = min(ins(y, z)) x ≈ y ∧ x y ∧ x, y: x Nat ∧ z: x Set (15) The clause (14) is a tautology. Subgoal (15) is simplified using Partial Splitting again. We obtain: min(ins(y, ins(x, z))) = min(ins(y, z)) x ≻ y ∧ x y ∧ x ≈ y ∧ x, y: x Nat ∧ z: x Set (16) min(ins(y, ins(x, z))) = min(ins(y, z)) x ⊁ y ∧ x y ∧ x ≈ y ∧ x, y: x Nat ∧ z: x Set (17) Subgoal (16) is simplified by R D into min(ins(y, z)) = min(ins(y, z)), a tautology. Subgoal (17) can also be deleted since the constraint x ⊁ y, x y, x ≈ y is unsatisfiable This ends the proof that (12) is an inductive theorem of R.
The proof of (13) follows the same steps. Note that by Theorem 5 the proofs of the decorated conjectures (1.a), (1.b) and (2.a), (2.b) in Section 3 remain valid for the above extended specification.

Partial Constructors and Powerlists
The restriction to decorated conjectures also permits to deal with partial constructor functions. In this case, we are generally interested in proving conjectures only for constructor terms in the definition domain of the defined function (wellformed terms). This is possible with our procedure when R C is such that the set of well-formed terms is the set of constructor R C -normal forms. Hence, decorating the conjecture with grammar's non-terminals, as in Theorem 2, amounts in this case at restricting the variables to be instantiated by well-formed terms.
We illustrate this approach in this section with an example of application of Theorem 2 to a non complete specification of powerlists. Specification of powerlists. A powerlist [24] is a list of length 2 n (for n ≥ 0) whose elements are stored in the leaves of a balanced binary tree. Kapur gives in [20] a specification of powerlists and some proofs of conjectures with an extension of RRL mentioned in introduction. This example is carried out with an extension of the algebraic specification approach where some partial constructor symbols are restricted by application conditions. We propose below another specification of powerlists which contains only constrained rewrite rules, and which can be efficiently handled by our method.
We consider a signature for representing powerlists of natural numbers, with the sorts: S = {Nat, List} and the constructor symbols: C = 0 : Nat, s : Nat → Nat, v : Nat → List, tie : List → List, ⊥ : List The symbols 0 and s are used to represent the natural numbers in unary notation, v creates a singleton powerlist v(n) of length 1 from a number n, and tie is the concatenation of powerlists. The operator tie is restricted to well balanced constructor terms of the same depth. In order to express this property, we shall consider a constructor rewrite system R C which reduces to ⊥ every term tie(s, t) which is not well balanced. This way, only the well defined powerlists are R Cirreducible. For this purpose, we shall use a new binary constraint predicate ∼ defined on constructor terms of sort List as the smallest equivalence such that: v(x) ∼ v(y) for all x, y : Nat tie(x 1 , x 2 ) ∼ tie(y 1 , y 2 ) iff x 1 ∼ x 2 ∼ y 1 ∼ y 2 The constructor TRS R C has one rule constrained by ∼: tie(y 1 , y 2 ) → ⊥ y 1 ∼ y 2 tie(⊥, y) → ⊥ tie(y, ⊥) → ⊥ Tree grammars with ∼-constraints on brother subterms. The normal form tree grammar G NF (R C ) associated to R C generates the well founded ground constructor terms. Its non-terminals, according to the construction in Section 4.2, are: x Nat , x List , ⊥ , tie(x 1 , x 2 ) and its production rules: x Nat := 0 x Nat := s( x 2 Nat ) x Note that all the constraints in these production rules are applied to brother subterms. We have omitted in the above list the non-terminal x Red , and production rules of the form: x Red := tie( x 1 List , x 2 List ) x List 1 ∼ x List 2 or x Red := tie( ⊥ , x 2 List ). The emptiness problem is decidable for such constrained tree grammars. This can be shown with an adaptation of the proof in [1] to ∼-constraints (instead of equality constraints) or also by an encoding into the visibly tree automata with one memory of [13].
Proof of a conjecture. We add to the specification a defined symbol rev : D = rev : List → List and a defined TRS R D : rev (tie(y 1 , y 2 )) → tie(rev (y 2 ), rev (y 1 )) (r 2 ) The conjecture is: rev (rev (x)) = x A proof of Conjecture (18) can be found in [20]. We prove (18) by the analysis of several cases, where each case is treated quickly. As explained above, we need

Conclusion
A fundamental issue in automatic theorem proving by induction is the computation of a suitable finite description of the set of ground terms in normal form, which can be used as an induction scheme. Normal form constrained tree grammars are perfect induction schemes in the sense that they generate exactly the set of constructor terms in normal form. At the opposite, test sets and cover sets are approximated induction schemes when the constructors are not free. They may indeed also represent some reducible ground terms, and therefore may cause the failure (a result of the form "don't know") of an induction proof when constructors are not free. In this case, refutational completeness is not guaranteed. This explains the choice of constrained grammars for the incremental generation of subgoals. Constrained tree grammars are also used (by mean of emptiness test) in order to detect in some cases that constructor subgoals are inductively valid. Moreover, this formalism permits to handle naturally constraint of membership in a fixed regular tree language.
Our inference system allows rewrite rules between constructors which can be constrained. Hence it permits to automate induction proofs on complex data structures. It is sound and refutationally complete, and allows for the refutation of false conjectures, even with constrained constructor rules. Moreover, all the conditions of inference rules are either recursive calls to the procedure (Rewrite Splitting or Inductive Contextual Rewriting), or either some tests decidable under some assumptions on the constraints of the rewrite system for constructors. These assumptions are required for decision of emptiness of constrained grammar languages.
Constraints in rules can serve to transform non terminating specifications into terminating ones, for instance in presence of associativity and commutativity axioms (ordering constraints), define ad-hoc evaluation strategies, like e.g. innermost rewriting, directly in the axioms (normal form constraints), or for the analysis of trace properties of infinite state systems like security protocols (constraints of membership in a regular tree language representing faulty traces [3]). The treatment of membership constraints permits to express in a natural way, in conjectures, trace properties for the verification of systems. This idea has been applied for the validation and research of attacks (by refutation) on security protocols in a model with explicit destructor functions [3]. These symbols represent operators like projection or decryption whose behaviour is specified with constructor axioms.
Our procedure can handle partial specifications: specifications which are not sufficiently complete and specifications with partial constructor functions in the lines of [20]. Moreover, it preserves the proofs of decorated conjectures made in a sufficiently complete specification when this specification is extended with partial symbols.
The definition of tree grammars with constraints in Section 4 is very general. It embeds some classes of grammars for which the emptiness problem is decidable (see Section 6) and also classes for which this problem is still open. Therefore, advances in tree automata theory can benefit our approach, and we are planing to study new classes of tree automata with constraints.