key: cord-0049785-an1pzm70
authors: Lochmann, Alexander; Middeldorp, Aart
title: Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
date: 2020-03-13
journal: Tools and Algorithms for the Construction and Analysis of Systems
DOI: 10.1007/978-3-030-45237-7_11
sha: 62b3eacd174c060c09b696a4d4182201256f39c0
doc_id: 49785
cord_uid: an1pzm70

We present a formalized proof of the regularity of the infinity predicate on ground terms. This predicate plays an important role in the first-order theory of rewriting because it allows to express the termination property. The paper also contains a formalized proof of a direct tree automaton construction of the normal form predicate, due to Comon.

Term rewriting [1, 18] is an abstract model of computation which underlies much of declarative programming and automated theorem proving. The foundation of rewriting is equational logic. Equations are used from left to right to direct the search for proofs. Fundamental properties like confluence (which ensures that different computation paths produce the same result) and termination (all computation paths produce a result) are undecidable in general. For terminating systems, one is interested in estimating the resources needed to evaluate expressions (space and time complexity). Much progress has been made in establishing sufficient and automatable criteria for confluence, termination, complexity, and other properties of rewrite systems. These criteria have been implemented in highly optimized automatic tools that compete on a yearly basis [12, 13] . These competitions, together with the recent advances in SAT [4] and SMT [2] solving, have on the one hand led to specialized techniques that are especially suitable for automation. On the other hand, software bugs observed in the tools gave rise to the more recent activity of certification of the output of termination, complexity, and confluence tools. This is done by formalizing the underlying methods in an interactive proof assistant like Coq [3] or Isabelle [15] , and using the code generation facilities of these proof assistants to obtain trustworthy programs that can certify the output of the tools.

In this paper we are concerned with the formalization of methods that are used in FORT [16, 17] , a tool that implements the first-order theory of rewriting for the decidable class of left-linear, right-ground rewrite systems. FORT can be used to decide properties of a given rewrite system and to synthesize rewrite systems that satisfy arbitrary properties expressible in the first-order theory of rewriting. The decision procedure is based on tree automata techniques and goes back to a paper by Dauchet and Tison [7] . In a recent paper [10] the authors formalized results concerning ground tree transducers and RR n automata for a fragment of the first-order theory that allows to express confluence, resulting in a formalized confluence prover for left-linear, right-ground rewrite systems. In this paper we cover the infinity predicate that is crucial for expressing the termination property in the first-order theory of rewriting and an efficient automaton construction of the normal form predicate that is employed in FORT. The former goes back to a technical report by Dauchet and Tison [8] and the latter is based on a paper by Comon [5] . The normal form predicate has other applications as well (e.g. [9, 14] ). A proof of the construction of [8] is given in [16] , but this proof contains a serious mistake that we report at the end of Section 3.

Our formalizations are based on IsaFoR [19] , 1 an Isabelle/HOL library containing numerous abstract results and concrete techniques from the rewriting literature. Our own development can be found at http://cl-informatik.uibk.ac.at/software/fortissimo/tacas2020/ Most definitions, theorems, and lemmata in this paper directly correspond to the formalization. These are indicated by the symbol, which links to a HTML presentation in the PDF version of the paper.

In the next section we recall basic definitions, notation, and results concerning term rewriting and tree automata that we need in the sequel. In Section 3 we present our first main result, a formalized correctness proof of the regularity of the infinity predicate for regular relations. The tree automaton constructed in the correctness proof is not directly executable due to the definition of Q ∞ which plays an important role in the construction of the tree automaton. In Section 4 we present our second main result, an equivalent definition of Q ∞ that is constructive. Our third result, a formalized correctness proof of an efficient tree automata construction of the normal form predicate for left-linear rewrite systems, is the topic of Section 5. We conclude in Section 6 with some statistics of our formalizations as well as a list of tasks that remain to be done for a certified version of FORT.

When we write "formalized" we always mean "formalized in Isabelle/HOL."

Familiarity with term rewriting [1] and tree automata [6] is useful, but we briefly recall important definitions and notation that we use in the remainder. We assume a given signature F and a set of variables V. Function symbols in F are equipped with a fixed arity. Function symbols of arity zero are called constants. The set of terms built from F and V is denoted by T (F , V) and inductively defined: A term is either a variable x ∈ V or f (t 1 , . . . , t n ) for a function symbol f of arity n and terms t 1 , . . . , t n ∈ T (F , V). The set of variables occurring in a term t is denoted by Var(t). A term t with Var(t) = ∅ is called ground. We write T (F ) for the set of ground terms. Positions are strings of positive integers which are used to address subterms. The empty string is called root position and denoted by . The set of positions in a term t is denoted by Pos(t) and the subterm of t at position p ∈ Pos(t) by t| p . We write s t if s is a proper subterm of t, i.e., s = t| p with p = . We write t[u] p for the result of replacing the subterm of t at position p with the term u. The root symbol of a term t is denoted by root(t) and t(p) denotes root(t| p ). We write p < q if p is a proper prefix of q. A context C is a term with a hole . Here / ∈ F is a special constant. We write C[t] for the result of replacing the hole in C by t. A substitution σ is a mapping from variables to terms. We write tσ for the result of applying σ to the term t.

A term rewrite system (TRS for short) R consists of rewrite rules → r between terms and r over the same signature F such that Var(r) ⊆ Var( ). The rewrite relation → R is defined on terms as follows: s → R t if there exist a position p ∈ Pos(s), a rewrite rule → r ∈ R, and a substitution σ such that s| p = σ and t = s[rσ] p . The reflexive transitive closure of → R is denoted by → * R . A redex is a substitution instance of a left-hand side of a rewrite rule. Terms that contain a redex as subterm are called reducible. A normal form is a term without redexes. We write NF(R) for the set of ground normal forms of R. In this paper we consider finite TRSs over finite signatures. The TRSs handled by FORT are left-linear (no duplicate variables in left-hand sides of rewrite rules) and right-ground (no variables in right-hand sides of rewrite rules).

We now recall some basic notions related to tree automata. A tree automaton is a quadruple A = (F , Q, Q f , ∆) consisting of a finite signature F , a finite set Q of states, disjoint from F , a subset Q f ⊆ Q of final states, and a set of transition rules ∆. Every transition rule has one of the following two shapes:

f (p 1 , . . . , p n ) → q with f ∈ F and p 1 , . . . , p n , q ∈ Q, or p → q with p, q ∈ Q.

Transition rules of the second shape are called epsilon transitions. We write ∆ for the set of epsilon transitions. Furthermore, ∆ ¬ = ∆ \ ∆ . Transition rules can be viewed as rewrite rules between ground terms in T (F ∪ Q). The induced rewrite relation is denoted by

The set of all accepted terms is denoted by L(A) and a set L of ground terms is regular if L = L(A) for some tree automaton A.

Let A = (F , Q, Q f , ∆) be a tree automaton. A state q ∈ Q is reachable if t → * ∆ q for some term t ∈ T (F ). We say that q is productive if C[q] → * ∆ q f for some ground context C and final state q f ∈ Q f . The automaton A is trim if all states are both reachable and productive. Any tree automaton can be transformed into an equivalent trim automaton. This result has been formalized in IsaFoR by Felgenhauer and Thiemann [11] .

Below we present a formalized proof of a version of the pumping lemma that we need later. Lemma 1. Let A = (F , Q, Q f , ∆) be a tree automaton and t → * ∆ q with t ∈ T (F ) and q ∈ Q. If height(t) > |Q| then there exist contexts C 1 and C 2 = , a term u, and a state p such that

From the assumptions t → * ∆ q and height(t) > |Q| we obtain a sequence (t 1 , . . . , t n+1 , q 1 , . . . , q n+1 , D 1 , . . . , D n ) consisting of ground terms, states, and non-empty contexts with n > |Q| such that

for all i n, and q n+1 = q and t n+1 = t by a straightforward induction proof on t. Because n > |Q| there exist indices 1 i < j n such that q i = q j . We construct the contexts

We conclude this preliminary section with a brief account of RR 2 relations, which are binary relations on ground terms over a signature F whose encoding as sets of ground terms over the extended signature F (2) = (F ∪ {⊥}) 2 with a fresh constant ⊥ / ∈ F is regular. The arity of a symbol f g ∈ F (2) is the maximum of the arities of f and g. The encoding of two terms t, u ∈ T (F ) is the unique term t, u ∈ T (F (2) ) such that Pos( t, u ) = Pos(t) ∪ Pos(u) and t, u (p) = f g where

for all positions p ∈ Pos(t) ∪ Pos(u). We illustrate this on a concrete example. For the ground terms t = f(g(a), f(b, a)) and u = f(a, g(g(b))) we obtain t, u = ff(ga(a⊥), fg(bg(⊥b), a⊥)). A tree automaton operating on terms in T (F (2) ) is called an RR 2 automaton. The two projection operations effectively transform RR 2 relations on T (F ) to regular subsets of T (F ).

The following formula in the first-order theory of rewriting expresses the termination property: 2

The predicate FIN → + holds for t ∈ T (F ) if there are only finitely many terms u ∈ T (F ) such that t → + u. We consider its complement as it leads to smaller automata:

Definition 1. Let • be an arbitrary binary relation on T (F). We write INF • for the set {t ∈ T (F ) | (t, u) ∈ • for infinitely many terms u ∈ T (F)}.

In [8] the construction of a tree automaton that accepts FIN • for an arbitrary RR 2 relation • 3 is given. In [16, Appendix A] a correctness proof of the construction is presented, which contains a serious mistake (reported at the end of this section). In this section we give a rigorous and formalized proof of the regularity of INF • for arbitrary RR 2 relations •.

The following definition originates from [8] . a, b) )) | n = 2 and m 1 or n 3 and m = 1}

A = (F (2) , Q, Q f , ∆), the set Q ∞ ⊆ Q consists of all states q ∈ Q such that ⊥, t → * ∆ q for infinitely many terms t ∈ T (F ).

The encoding of • is accepted by the RR 2 automaton A = (F (2) 

, and ∆ consisting of the following transition rules:

For instance, f(a, g(g(b))), g(f(a, b)) = fg(af(⊥a, ⊥b), g⊥(g⊥(b⊥))) a, b) ) for all n 0. 3 The relation → + R is an RR2 relation for left-linear, right-ground TRSs R. Other uses of FIN (INF) can be found in [16] .

Given a tree automaton A = (F (2) , Q, Q f , ∆), we define the tree automaton A ∞ = (F (2) , Q ∪Q,Q f , ∆ ∪∆). HereQ is a copy of Q where every state is dashed:q ∈Q if and only if q ∈ Q. For every transition rule f g(q 1 , . . . , q n ) → q ∈ ∆ we have the following transition rules in∆:

Moreover, for every -transition p → q ∈ ∆ we add p →q (3) to∆. We write ∆ for ∆ ∪∆.

Dashed states are created by rules of shape (1) and propagated by rules of shapes (2) and (3). The above construction differs from the one in [8] ; instead of (1) the latter contains f g(q 1 , . . . , q n ) →q if q i ∈ Q ∞ for some i > arity(f ). In an implementation, rather than adding all dashed states and all transition rules of shape (2), the necessary rules would be computed by propagating the dashes created by (1) in order to avoid the appearance of unreachable dashed states. When A ∞ is used in isolation, a single bit suffices to record that a dashed state occurred during a computation.

Example 2. For the tree automaton A from Example 1 we obtain A ∞ by adding the following transition rules (the missing rules of shape (2) involve unreachable states):

The unique final state of A ∞ is0. We have f(a, g(g(b))), g(f(a, b)) ∈ L(A ∞ ) but there is no term u such that f(a, g(b)), u ∈ L(A ∞ ).

The following preliminary lemma is proved by a straightforward induction argument.

Proof. From t ∈ INF • and • = L(A) we obtain t, u ∈ L(A) for infinitely many terms u ∈ T (F ). Since the signature is finite, there are only finitely many ground terms of any given height. Moreover, height( t, u ) = max (height(t), height(u)).

Hence there must exist a term u ∈ T (F ) with t, u ∈ L(A) such that

This is only possible if there are positions p and q such that p / ∈ Pos(t), pq ∈ Pos(u), and |Q| < |q|. From Pos( t, u ) = Pos(t) ∪ Pos(u) we obtain t, u | p = ⊥, u| p . Since t, u ∈ L(A) there exist states r ∈ Q and q ∈ Q f such that

where we assume without loss of generality that the last step in the subsequence ⊥, u| p → * A r uses a non-epsilon transition rule. From |Q| < |q| and pq ∈ Pos(u) we infer |Q| < height( ⊥, u| p ). Hence we can use the pumping lemma (Lemma 1) to conclude the existence of infinitely many terms v ∈ T (F ) such that ⊥, v → * A r. Hence r ∈ Q ∞ by Definition 2. Since the last step ⊥, u| p → * A r uses a non-epsilon transition rule, we obtain ⊥, u| p → * A∞r using Lemma 2 and a final application of a rule of shape (1). Also using Lemma 2 we obtain t, u [r] p → * A∞q f as t, u [r] p → * A q f . We conclude t, u ∈ L(A ∞ ) as desired.

For the reverse direction of Theorem 3 we need two auxiliary results. The first result is proved by a straightforward induction argument. Here the mapping ϕ : T (F (2) ∪ Q ∪Q) → T (F (2) ∪ Q) erases all dashes from states.

With a little bit more effort, we obtain the second auxiliary result. The key step in the proof is identifying the rule of shape (1) that is used to create the first dashed state.

Lemma 4. If t ∈ T (F (2) ) and t → * A∞p then there exist a state q ∈ Q ∞ , a context C, and a term s such that C[s] = t, root(s) = ⊥f for some f ∈ F , s → * A∞q , and C[q] → * A∞p .

Proof. From t, u ∈ L(A ∞ ) we obtain a final stateq f ∈Q with t, u → * A∞q f . Using Lemma 4, we obtain a context C, a term s with root(s) = ⊥f for some f ∈ F , and a state q ∈ Q ∞ such that C[s] = t, u , s → * A∞q , and C[q] → * A∞q f . Let p be the position of the hole in C. From C[s] = t, u and root(s) = ⊥f , we infer p ∈ Pos(u) \ Pos(t).

It follows that t, u[w] p ∈ L(A) and thus there are infinitely many terms u such that t, u ∈ L(A). Since • = L(A) we conclude the desired t ∈ INF • .

The final step to conclude that the infinity predicate is indeed regular is now easy.

Proof (of Theorem 1). Combining Theorem 2 and Theorem 3 yields the following equivalence:

Hence a tree automaton that accepts INF • is obtained by subjecting A ∞ to a projection operation (on the first argument).

Projection on RR n automata has been formalized in Isabelle/HOL as part of [10] .

The mistake in the proof given in the appendix of [16] is quoted below and corresponds to the proof of Theorem 2:

The set U = {u ∈ T (F ) | (t, u) ∈ •} is infinite. Since the signature F is finite, infinitely many terms u in U have a height greater than t. Hence there exists a position p / ∈ Pos(t) such that the set U = {u ∈ U | p ∈ Pos(u)} is infinite. For every u ∈ U we have t, u | p = ⊥, u| p . Since t, u is accepted by A and Q is finite, there must exist a state q such that ⊥, u| p → * A q for infinitely many terms u ∈ U . Therefore q ∈ Q ∞ . The following example refutes the above reasoning, which is the key step in the proof in [16] . It was found in attempt to formalize the proof. with ∆ consisting of the transition rules ff(q 4 , q 5 ) → q 6 ⊥a → q 2 bg(q 1 ) → q 5 ⊥b → q 1 af(q 2 , q 3 ) → q 4 ⊥b → q 3 ⊥g(q 1 ) → q 1 accepts the relation • = {t} × U . Consider the position p = 11. We have p / ∈ Pos(t) and p ∈ Pos(u) for all terms u ∈ U . Hence U = U . Moreover, t, u | p = ⊥, a = ⊥a for all terms u ∈ U . The only state reachable from ⊥a is q 2 and clearly q 2 / ∈ Q ∞ .

Owing to the definition of Q ∞ , the automaton A ∞ defined in Definition 3 is not executable. In this section we give an equivalent but executable definition of Q ∞ , which we name Q e ∞ :

Q e ∞ = {q | p p and p q for some state p ∈ Q}

Here the relation is defined using the inference rules in Figure 1 . Before proving that the two definitions are equivalent, we illustrate the definition of Q e ∞ by revisiting Example 1.

⊥f (p1, . . . , pn) →∆ p p1 p · · · pn p p q q →∆ r p r p q q r p r The proof of the next lemma is straightforward. Note that the relations → * ∆ and * ∆ do not coincide on mixed terms, involving function symbols and states.

Lemma 5. Let C be a ground context. We have C[p] → * ∆ q if and only if p → * ∆ p and C[p ] * ∆ q for some state p .

We start by proving the following claim:

if C[p] * ∆ q and C is a non-empty right-only context then p q ( * )

We use induction on the structure of C. If C = there is nothing to show. Suppose C = ⊥f (t 1 , . . . , C , . . . , t n ) where C is the i-th subterm of C. The sequence C[p] * ∆ q can be rearranged as C[p] = ⊥f (t 1 , . . . , C [p], . . . , t n ) * ∆ ⊥f (q 1 , . . . , q n ) → ∆ q → * ∆ q. We obtain q i q and subsequently q i q by using the inference rules in Figure 1 . If C = then p = q i and if C = then the induction hypothesis yields p q i and thus p q by transitivity. This concludes the proof of ( * ).

Assume q ∈ Q ∞ , so there exist infinitely many terms t such that ⊥, t → * ∆ q. Since the signature is finite, there exist terms of arbitrary height. Thus there exists an arbitrary but fixed term t such that the height of t is greater than the number of states of Q. Write t = f (t 1 , . . . , t n ). Since the height of t is greater than the number of the states in Q, there exist a subterm s of t, a state p, and contexts C 1 and C 2 = such that

∆ p, and 4. C 1 [p] → * ∆ q. From Lemma 5 we obtain a state q such that p → * ∆ q and C 2 [q ] * ∆ p. Hence q p by ( * ). We obtain q q from q p in connection with the inference rule for epsilon transitions. We perform a case analysis of the context C 1 .

-If C 1 = then p → * ∆ q and thus q q follows from q p in connection with the inference rule for epsilon transitions. Hence q ∈ Q e ∞ . -If C 1 = then Lemma 5 yields a state q such that p → * ∆ q and C 1 [q ] * ∆ q. Hence q q by ( * ). We also have C 2 [q ] * ∆ q and thus q q by ( * ). We obtain q q from the transitivity rule. Hence also in this case we obtain q ∈ Q e ∞ . For the following lemma, we need the fact that A can be assumed to be trim, so every state is productive and reachable. We may do so because Theorem 1 talks about regular relations, and any automaton that accepts the same language as A will witness the fact that the given relation • is regular.

In connection with the fact that A accepts • ⊆ T (F ) × T (F ), trimness of A entails that any run t → * ∆ q is embedded into an accepting run

and hence t must be a well-formed term. Moreover, if root(t) = ⊥f for some f ∈ F then t = ⊥, u for some term u ∈ T (F ). We now show the converse of claim ( * ) in the proof of Lemma 6 for the relation → * ∆ : if p q then C[p] → * ∆ q for some ground right-only context C = ( * * )

We prove the claim by induction on the derivation of p q. First suppose p q is derived from the transition rule ⊥f (p 1 , . . . , p i , . . . , p n ) → q in ∆ with p i = p. Because all states are reachable by well-formed terms, there exist terms t 1 , . . . , t n ∈ T (F ) such that ⊥, t → * ∆ p i for all 1 i n. Let C 1 = ⊥f ( ⊥, t 1 , . . . , , . . . , ⊥, t n ) where the hole is the i-th argument. We have C 1 [p] → * ∆ ⊥f (p 1 , . . . , p i , . . . , p n ) → ∆ q. Next suppose p q is derived from p q and q → ∆ q. The induction hypothesis yields a ground right-only context C = such that C[p] → * ∆ q . Hence also C[p] → * ∆ q. Finally, suppose p q is derived from p r and r q. The induction hypothesis yields non-empty ground right-only contexts C 1 and C 2 such that C 1 [p] → * ∆ r and

]. This concludes the proof of ( * * ). Now let q ∈ Q e ∞ . So there exists a state p such that p p and p q. Using ( * * ), we obtain non-empty ground right-only contexts C 1 and C 2 such that C 1 [p] → * ∆ p and C 2 [p] → * ∆ q. Since all states are reachable, there exists a ground term t ∈ T (F (2) ) such that t → * ∆ p. Hence C 2 [t] → * ∆ q and, by the observation made at the beginning of the proof, C 2 [t] is a well-formed term. Since C 2 is right-only, it follows that t = ⊥, u for some term u ∈ T (F ). Now consider the infinitely many terms t n = C 2 [C n 1 [t]] for n 0. We have t n → * ∆ q and t n is right-only by construction. Hence q ∈ Q ∞ . Corollary 1. Q e ∞ = Q ∞ , provided that A is trim.

The normal form predicate NF can be defined in the first-order theory of rewriting as

and this gives rise to the following procedure:

1. An RR 2 automaton is constructed that accepts the encoding of the rewrite relation →.

2. The RR 2 automaton of step 1 is projected into a tree automaton that accepts the set of reducible ground terms.

3. Complementation is applied to the automaton of step 2 to obtain a tree automaton that accepts the set of ground normal forms.

Since projection may transform a deterministic tree automaton into a nondeterministic one, this is inefficient. In this section we provide a direct construction of a tree automaton that accepts the set of ground normal forms of a left-linear TRS, which goes back to Comon [5] , and present a formalized correctness proof. Throughout this section R is assumed to be left-linear.

We start with defining some preliminary concepts.

Definition 5. Given a signature F , we write F ⊥ for the extension of F with a fresh constant symbol ⊥. Given t ∈ T (F , V), t ⊥ denotes the result of replacing all variables in t by ⊥:

We define the partial order on T (F ⊥ ) as the least congruence that satisfies ⊥ t for all terms t ∈ T (F ⊥ ):

The partial map ↑ :

is defined as follows:

It is not difficult to show that t ↑ u is the least upper bound of comparable terms t and u.

Let R be a TRS over a signature F . We write T ⊥ for the set {t ⊥ | t for some → r ∈ R} ∪ {⊥}. The set T ↑ is obtained by closing T ⊥ under ↑.

Example 5. Consider the TRS R consisting of following rules:

We start by collecting the subterms of the left-hand sides: Although the above proof is simple enough, we formalized the proof below which is based on a concrete algorithm to compute T ↑ . Actually, the algorithm presented below is based on a general saturation procedure, which is of independent interest.

Definition 7. Let f : U × U → U be a (possibly partial) function and let S be a finite subset of U . The closure C f (S) is the least extension of S with the property that f (a, b) ∈ C f (S) whenever a, b ∈ C f (S) and f (a, b) is defined.

The following lemma provides a sufficient condition for closures to exist. The proof gives a concrete algorithm to compute the closure.

Lemma 9. If f is a total, associative, commutative, and idempotent function then C f (S) exists and is finite.

Proof. A straightforward induction proof reveals that for every a ∈ C f (S) there exist elements a 1 , . . . , a n ∈ S such that a = f (a 1 , f (a 2 , . . . f (a n−1 , a n ) . . . )). Select an arbitrary element b ∈ S. If b is among a 1 , . . . , a n then, using the properties of f , we obtain a ∈ {f (b, c) | c ∈ C f (S \ {b})}. If b is not among a 1 , . . . , a n then a ∈ C f (S \ {b}). Hence

for every b ∈ S. Since S is finite, this gives rise to an iterative algorithm to compute C f (S), which is given in Listing 5. In each iteration only finitely many elements are added. Hence C f (S) is finite. Since our function ↑ is partial, we need to lift it to a total function that preserves associativity and commutativity. In our abstract setting this entails finding a binary predicate P on U such that f (a, b) is defined if P (a, b) holds. In addition, the following properties need to be fulfilled:

-P is reflexive and symmetric, if P (a, f (b, c)) and P (b, c) hold then P (a, b) and P (f (a, b), c) hold as well, for all a, b, c ∈ U .

For the details we refer to the formalization.

The tree automaton A NF(R) = (F , Q, Q f , ∆) is defined as follows: Q = Q f = T ↑ and ∆ consists of all transition rules f (p 1 , . . . , p n ) → q such that f (p 1 , . . . , p n ) is no redex and q is the maximal element of Q satisfying q f (p 1 , . . . , p n ). 4 Example 6. For the TRS R of Example 5, the tree automaton A NF(R) consists of the following transition rules:

Here we use the following abbrevations: As can be seen from the above example, the tree automaton A NF(R) is not completely defined. Unlike the construction in [5] , we do not have an additional state that is reached by all reducible ground terms.

Before proving that A NF(R) accepts the ground normal forms of R, we first show that A NF(R) is well-defined, which amounts to showing that for every f (p 1 , . . . , p n ) with f ∈ F and p 1 , . . . , p n ∈ T ↑ the set of states q such that q f (p 1 , . . . , p n ) has a maximum element with respect to the partial order .

Lemma 10. For every term t ∈ T ↑ the set {s ∈ T ↑ | s t} has a unique maximal element.

Proof. Let S = {s ∈ T ↑ | s t}. Because ⊥ t and ⊥ ∈ T ↑ , S = ∅. If s 1 , s 2 ∈ T then s 1 t and s 2 t and thus s 1 ↑ s 2 is defined and satisfies s 1 ↑ s 2 t. Since T ↑ is closed under ↑, s 1 ↑ s 2 ∈ T ↑ and thus s 1 ↑ s 2 ∈ P . Consequently, S has a unique maximal element.

The next lemma is a trivial consequence of the fact that A NF(R) has no epsilon transitions.

Lemma 11. The tree automaton A NF(R) is deterministic.

Lemma 12. If t ∈ T (F ) with t → * ∆ q and s ⊥ t ⊥ for a proper subterm s of some left-hand side of R then s ⊥ q.

Proof. We use structural induction on t. Let t = f (t 1 , . . . , t n ). We have t → * ∆ f (q 1 , . . . , q n ) → ∆ q. We procede by case analysis on s. If s is a variable then s ⊥ = ⊥ and, as ⊥ is minimal in , we obtain s ⊥ q. Otherwise we must have root(s) = f from the assumption s ⊥ t ⊥ . So we may write s = f (s 1 , . . . , s n ). The induction hypothesis yields s ⊥ i q i for all 1 i n. Hence s ⊥ = f (s ⊥ 1 , . . . , s ⊥ n ) f (q 1 , . . . , q n ). Additionally we have s ⊥ ∈ Q by Definition 8 as s is a proper subterm of a left-hand side of R. Since f (q 1 , . . . , q n ) → q is a transition rule, we obtain f (s 1 , . . . , s n ) ⊥ q from the maximality of q.

Using the previous result we can prove that no redex of R reaches a state in A NF(R) .

Lemma 13. If t ∈ T (F ) is a redex then t → * ∆ q for no state q ∈ T ↑ .

Proof. We have ⊥ t for some left-hand side of R. For a proof by contradiction, assume t → * ∆ q. Write t = f (t 1 , . . . , t n ). We have t → * ∆ f (q 1 , . . . , q n ) → ∆ q and obtain ⊥ f (q 1 , . . . , q n ) by a case analysis on and Lemma 12. Therefore the transition rule f (q 1 , . . . , q n ) → ∆ q cannot exist by Definition 8.

If t → * ∆ q and t ∈ T (F ) then q t.

Proof. We use structural induction on t. Let t = f (t 1 , . . . , t n ). We have t → * ∆ f (q 1 , . . . , q n ) → * ∆ q. The induction hypothesis yields q i t i for all 1 i n and thus also f (q 1 , . . . , q n ) f (t 1 , . . . , t n ). We have q f (q 1 , . . . , q n ) by Definition 8 and thus q t by the transitivity of .

In this paper we presented formalized correctness proofs of the regularity of the infinity and normal form predicates in the first-order theory of rewriting. For the former we also provided an executable version, which is important for checking certificates that will be provided in a future version of FORT. Our results are an important step towards the ultimate goal of proving the correctness of the decisions reported by FORT, but much work remains to be done. We are developing a certification language which reflects the high-level proof steps in the decision procedure for the full first-order theory of rewriting. This language will be independent of FORT. In particular, details of the intermediate tree automata computed by FORT will not be part of certificates. This keeps the certificates small and avoids having to implement a verified (and expensive) equivalence check on tree automata. We will provide executable Isabelle code for each of the constructs in the certification language, and so this involves replaying the automata constructions in Isabelle.

We conclude the paper by providing some details of the size of our formalization in Table 1 . 

We use structural induction on t. Let t = f (t 1

R) ) = NF(R). all states in T ↑ are final, t ∈ L(A NF(R) ). Next assume t / ∈ NF(R). Hence t = C[s] for some redex s. According to Lemma 13 s does not reach a state in A NF(R)

Term Rewriting and All That

6 years of SMT-COMP

Interactive Theorem Proving and Program Development -Coq'Art: The Calculus of Inductive Constructions

Handbook of Satisfiability

Sequentiality, monadic second-order logic and tree automata

Tree automata techniques and applications

The theory of ground rewrite systems is decidable

The theory of ground rewrite systems is decidable (extended version)

Proving non-termination by finite automata

A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL

Reachability, confluence, and termination analysis with state-compatible automata

The termination and complexity competition

Confluence competition

Decidability for left-linear growing term rewriting systems

Isabelle/HOL -A Proof Assistant for Higher-Order Logic

Automating the first-order theory of left-linear rightground term rewrite systems

Proc. 9th International Joint Conference on Automated Reasoning. LNAI

Term Rewriting Systems

Certification of termination proofs using CeTA

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use

Acknowledgments. We thank Bertram Felgenhauer and T. V. H. Prathamash for contributions in the early stages of this work. The comments by the reviewers helped to improve the presentation of the paper.