Y. Boichut, T. Genet, T. Jensen, and L. Leroux, Rewriting Approximations for Fast Prototyping of Static Analyzers, RTA'07, pp.48-62, 2007.
DOI : 10.1007/978-3-540-73449-9_6
URL : https://hal.archives-ouvertes.fr/hal-00463418

J. Kochems and L. Ong, Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars, of LIPIcs, Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, 2011.

T. Genet, Y. Tang-talpin, V. Viet-triem, and . Tong, Verification of Copy Protection Cryptographic Protocol using Approximations of Term Rewriting Systems, 2003.

A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna et al., The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, LNCS, vol.3576, pp.281-285, 2005.
DOI : 10.1007/11513988_27
URL : https://hal.archives-ouvertes.fr/inria-00000408

A. Geser, D. Hofbauer, J. Waldmann, and H. Zantema, On tree automata that certify termination of left-linear term rewriting systems, RTA'05, pp.353-367, 2005.

G. Feuillade, T. Genet, V. Viet-triem, and . Tong, Reachability Analysis over Term Rewriting Systems, Journal of Automated Reasoning, vol.37, issue.1?2, pp.3-4, 2004.
DOI : 10.1007/s10817-004-6246-0
URL : https://hal.archives-ouvertes.fr/inria-00071609

T. Genet and R. Rusu, Equational approximations for tree automata completion, Journal of Symbolic Computation, vol.45, issue.5, pp.574-597, 2010.
DOI : 10.1016/j.jsc.2010.01.009
URL : https://hal.archives-ouvertes.fr/inria-00495405

T. Genet, Reachability analysis of rewriting for software verification, 2009.
URL : https://hal.archives-ouvertes.fr/tel-00477013

T. Genet, Towards Static Analysis of Functional Programs Using Tree Automata Completion, WRLA'14, 2014.
DOI : 10.1007/978-3-319-12904-4_8
URL : https://hal.archives-ouvertes.fr/hal-00921814

T. Takai, A Verification Technique Using Term Rewriting Systems and Abstract Interpretation, RTA'04, pp.119-133, 2004.
DOI : 10.1007/978-3-540-25979-4_9

P. Réty, Regular Sets of Descendants for Constructor-Based Rewrite Systems, Proc. 6th LPAR Conf., Tbilisi (Georgia), 1999.
DOI : 10.1007/3-540-48242-3_10

T. Takai, Y. Kaji, and H. Seki, Right-Linear Finite Path Overlapping Term Rewriting Systems Effectively Preserve Recognizability, LNCS, vol.1833, issue.11, 2000.
DOI : 10.1007/10721975_17

T. Genet, Y. Boichut, B. Boyer, V. Murat, and Y. Salmon, Reachability Analysis and Tree Automata Calculations

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

F. Jacquemard, Decidable approximations of term rewriting systems, Proc. 7th RTA Conf, pp.362-376, 1996.
DOI : 10.1007/3-540-61464-8_65

T. Genet, Decidable approximations of sets of descendants and sets of normal forms, Proc. 9th RTA Conf., Tsukuba (Japan), pp.151-165, 1998.
DOI : 10.1007/BFb0052368
URL : https://hal.archives-ouvertes.fr/inria-00073364

A. Lisitsa, Finite Models vs Tree Automata in Safety Verification, RTA'12, pp.225-239, 2012.

Y. Boichut, R. Courbis, P. Héam, and O. Kouchnarenko, Handling non leftlinear rules when completing tree automata, IJFCS, vol.20, issue.5
URL : https://hal.archives-ouvertes.fr/hal-00561373

R. Gilleron and S. Tison, Regular tree languages and rewrite systems, Fundamenta Informaticae, vol.24, pp.157-175, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00538882

P. Réty and J. Vuotto, Tree automata for rewrite strategies, Journal of Symbolic Computation, vol.40, issue.1, pp.749-794, 2005.
DOI : 10.1016/j.jsc.2004.12.008

A. Gascon, G. Godoy, and F. Jacquemard, Closure of Tree Automata Languages under Innermost Rewriting, WRS'08, pp.23-38, 2008.
DOI : 10.1016/j.entcs.2009.03.033
URL : https://hal.archives-ouvertes.fr/inria-00578966

M. Dauchet and S. Tison, The theory of ground rewrite systems is decidable, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.242-248, 1990.
DOI : 10.1109/LICS.1990.113750

W. S. Brainerd, Tree generating regular systems, Information and Control, vol.14, issue.2, pp.217-231, 1969.
DOI : 10.1016/S0019-9958(69)90065-5

K. Salomaa, Deterministic tree pushdown automata and monadic tree rewriting systems, Journal of Computer and System Sciences, vol.37, issue.3, pp.367-394, 1988.
DOI : 10.1016/0022-0000(88)90014-1
URL : http://doi.org/10.1016/0022-0000(88)90014-1

J. Coquidé, M. Dauchet, R. Gilleron, and S. Vágvölgyi, Bottom-up tree pushdown automata and rewrite systems, Proc. 4th RTA Conf., Como (Italy), pp.287-298, 1991.
DOI : 10.1007/3-540-53904-2_104

I. Durand and A. Middeldorp, Decidable call-by-need computations in term rewriting, Information and Computation, vol.196, issue.2, pp.4-18, 1997.
DOI : 10.1016/j.ic.2004.10.003
URL : https://hal.archives-ouvertes.fr/hal-00338565

T. Nagaya and Y. Toyama, Decidability for left-linear growing term rewriting systems, LNCS, vol.1631, pp.256-270, 1999.

H. Seki, T. Takai, Y. Fujinaka, and Y. Kaji, Layered Transducing Term Rewriting System and Its Recognizability Preserving Property, Proc. 13th RTA Conf, 2002.
DOI : 10.1007/3-540-45610-4_8

P. Gyenizse and S. Vágvölgyi, Linear generalized semi-monadic rewrite systems effectively preserve recognizability, Theoretical Computer Science, vol.194, issue.1-2, pp.87-122, 1998.
DOI : 10.1016/S0304-3975(96)00333-7
URL : http://doi.org/10.1016/s0304-3975(96)00333-7

I. Durand and M. Sylvestre, Left-linear bounded trss are inverse recognizability preserving, of LIPIcs, Schloss Dagstuhl -Leibniz- Zentrum fuer Informatik, 2011.

S. Tison, Finiteness of the set of E-equivalence classes is undecidable, 2010.

B. Boyer, T. Genet, and T. Jensen, Certifying a Tree Automata Completion Checker, IJCAR'08, 2008.
DOI : 10.1007/978-3-540-71070-7_43
URL : https://hal.archives-ouvertes.fr/inria-00258275

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., All About Maude, A High-Performance Logical Framework, Lecture Notes in Computer Science, vol.4350, 2007.

J. Meseguer, M. Palomino, and N. Martí-oliet, Equational abstractions, Equational abstractions, pp.239-264, 2008.
DOI : 10.1016/j.tcs.2008.04.040

F. Oehl, G. Cécé, O. Kouchnarenko, and D. Sinclair, Automatic Approximation for the Verification of Cryptographic Protocols, Proc. of FASE'03, pp.34-48, 2003.
DOI : 10.1007/978-3-540-40981-6_5
URL : https://hal.archives-ouvertes.fr/inria-00071986

Y. Boichut, T. Dao, and V. Murat, Characterizing Conclusive Approximations by Logical Formulae, LNCS, vol.6945, issue.11, pp.72-84, 2011.
DOI : 10.1007/978-3-642-24288-5_8
URL : https://hal.archives-ouvertes.fr/inria-00606100

Y. Boichut and P. Héam, A theoretical limit for safety verification techniques with regular fix-point computations, Information Processing Letters, vol.108, issue.1, pp.1-2, 2008.
DOI : 10.1016/j.ipl.2008.03.012
URL : https://hal.archives-ouvertes.fr/inria-00328487

N. D. Jones and N. Andersen, Flow analysis of lazy higher-order functional programs, Theoretical Computer Science, vol.375, issue.1-3, pp.120-136, 2007.
DOI : 10.1016/j.tcs.2006.12.030

N. Kobayashi, N. Tabuchi, and H. Unno, Higher-order multi-parameter tree transducers and recursion schemes for program verification, pp.495-508, 2010.

L. Ong and S. Ramsay, Verifying higher-order functional programs with pattern-matching algebraic data types, 2011.

N. Kobayashi, Model Checking Higher-Order Programs, Journal of the ACM, vol.60, issue.3
DOI : 10.1145/2487241.2487246

T. Genet and Y. Salmon, Tree Automata Completion for Static Analysis of Functional Programs, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00780124

Y. Boichut, B. Boyer, T. Genet, and A. Legay, Equational Abstraction Refinement for Certified Tree Regular Model Checking, ICFEM'12, 2012.
DOI : 10.1007/978-3-642-34281-3_22
URL : https://hal.archives-ouvertes.fr/hal-00759149

T. Genet and Y. Salmon, Reachability Analysis of Innermost Rewriting, RTA'15, LIPIcs, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01194530

X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon, The Objective Caml system release 3.12 ? Documentation and user's manual, INRIA, 2012.

T. Genet, T. L. Gall, A. Legay, and V. Murat, A Completion Algorithm for Lattice Tree Automata, CIAA'13, pp.134-145, 2013.
DOI : 10.1007/978-3-642-39274-0_13

. Proof, We prove this by contradiction Assume that there exist configurations c

. However, the state q will no longer be new for ? ? {f (q 1 , . . . , q n ) ? q } and no other transition leading to q can be added except the same transition f (q 1, all following recursive calls of N orm

@. Finally, ?. , ?. Orm, and ?. , Assume that c ? q is added to N orm ? (t ? q) using the first case of the definition of N orm Then q = q but since c ? q ? ? this contradicts the fact that q is new for ?. Assume, now, that c ? q is added to N orm ? (t ? q) using the second case of the definition. As above, this means that c = f (q 1 , . . . , q n ) and one recursive call of N orm is of the form: {f (q 1 , . . . , q n ) ? q } ? N orm ??{f (q1,...,qn)?q } (C[q ] ? q). However, in this case of the definition, either the transition f (q 1 , . . . , q n ) ? q ? ? or q is a new state for ?. If f (q 1