+. ~i-q-', Soit s'un sous-terme de ra (éventuellement non strict) et ql E Q'. Par induction sur la taille de s', nous montrons maintenant que Norma(s' -+ ql) ç ~I implique s' -+~I ql: -si Si = ql, alors on a trivialement s

. -si-s-'=-qlf-e-q-', tel que q" f. q' alors, pqr le cas 2 de la définition de N orm, on obtient que NormO/(s' -+ Q') = {s' -+ Q'}. Puisque Normoe(s' -+ Q') ç 6

-. Si and =. .. , en appliquant le cas 3 de la définition de Norm, on obtient que Ca) {g(a(td,··· ,a(tm)) -+ ql} ç ~I, et (b) U~=l NormO/(ti -+ a(ti» ç 6.', où Vi = 1 ... n, a{td E Qnew ç Q'. En appliquant l'hypothèse d'induction à (b), on déduit que Vi = 1. .. n, ti -+~I a(ti)' D'autre part, (a) implique que g(a(td, ... , a(tm)) -+ ~' Q'

. En-conséquence, ,tm ) -+~I g(a(td,· .. ,a(tm )} -+~I q

D. Normoe, ra -+ q) ç 6.' implique ra -+~I q, et la condition de la proposition 6.1 est satisfaite par Tn t (A)

. En, arité des symboles de F est finie, si Q est fini et si l'ensemble des nouveaux états Qnew est fini, alors Q' = Qu Qnew est fini, le nombre de transition pouvant être ajoutées à 6. 1 est fini, et donc l'automate Tn t (A) est fini Comme nous ne considérons que le cas où :F et Q sont finis, afin de prouver que Tn t (A) est fini, il est suffisant de montrer que Qnew is. Dans le cas particulier de l'approximation ancêtre, ) Qnew = {1fi(r(l-+ r,q)) 1 l-+ r E R,q E QI,1 ::; i ::; Card(Pos.r(r))}

Q. Si-l-'on-applique-le-fait-que and . Qnew-À, on obtient que Qnew = QI U Q2 où: QI ={1fi(r(l -+ r,q)) l -+ r E R,q E Q,l ::; i ::; Card

E. R. Qnew, l ::; i ::; Card(Pos.:F(r))} sorted(nil) -> true. sorted(cons(x2, nil» -> true. sorted(cons(x2,cons(xl,x4») -> false if, pp.2-3

O. and O. True, leq(O,s(x) -> true. leq(s(x),s(y» -> Ieq(x,y)

. Le-tour-de-carte-de-gilbreath-var, append(cons(x,y),z) -> cons(x,append(y,z». rotate(null) -> null. rotate(cons(x,y» -> append(y,cons(x,null». even(null) -> true. even(cons(x,null» -> false. even(cons(xl,cons(x2,y») -> even(y). opposite(null,y) -> false. opposite(x,null) -> false. opposite(cons(xl,yl),cons(x2,y2» -> paired(xl,x2). pairedlist(null) -> true. pairedlist(cons(x,null» -> true. pairedIist(cons(xl,cons(x2,x») -> pairedIist(x) if [paired(xl,x2) = true]. pairedlist(cons(xl,cons(x2,x») -> false if [paired(xl,x2)=false] . alter(null) -> true, pp.2-3

. Ar, fact(s(x)) -> mult(s(x) , fact(x». fact(O) -> seO). mult(O, x) -> O. mult(s(x), y) -> plus(mult(x, y), y). pIus(x, 0) -> x. plus(x, s(y») -> s(plus(x, y). end. 7.3. Quelques systèmes de réécriture et leur preuve de terminaison Solving is successful Precedence: Car > minus, ar > fact, ar > div, tact> muIt, mult > plus, plus> s] Termination proof done in 0.42 seconds, fact(minus

E. Vf, . F-n, . .. Vtl, and E. Tn, Comme dans le cas précédent, en ajoutant les états et transitions de l'automate B, un des problèmes principaux reste d

]. T. Bibliographieag97a, J. Arts, and . Giesl, Automatically proving termination where simplification orderings fail, Proceedings 22nd International Colloquium on Trees in Algebra and Programming, pp.261-272, 1997.

T. Arts and J. Giesl, Proving innermost normalisation automatically, Proceedings 8th Conference on Rewriting Techniques and Applications, Sitges (Spain), pp.157-171, 1997.
DOI : 10.1007/3-540-62950-5_68

]. T. Ag97c, J. Arts, and . Giesl, Termination of rewriting using dependency pairs, 1997.

J. [. Arts and . Giesl, Modularity of termination using dependency pairs, Proceedings 9th Conference on Rewriting Techniques and Applications, pp.226-240, 1998.
DOI : 10.1007/BFb0052373

A. Arts, Termination by absence of infinite chains of dependency pairs, Proceedings 21st International Colloquium on Trees in Algebra and Programming, pp.196-210, 1996.
DOI : 10.1007/3-540-61064-2_38

]. T. Art97 and . Arts, Automatically proving termination and innermost normalisation of term rewriting systems, 1997.

R. Azaiez and I. Lorraine, Vérification automatique de programmes réactifs, 1998.

P. [. Cherifa and . Lescanne, An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities beteween polynomial interpretations, Proceedings 8th International Conference on Automated Deduction, pp.42-51, 1986.

P. Borovansky, C. Kirchner, H. Kirchner, P. Moreau, and M. Vittek, ELAN, Proceedings of the First International Workshop on Rewriting Logic, 1996.
DOI : 10.1016/S1571-0661(04)00032-5

URL : https://hal.archives-ouvertes.fr/inria-00098518

A. Bouhoula, E. Kounalis, and M. Rusinowitch, SPIKE, an automatic theorem prover, Proceedings of the lst International Conference on Logic Programming 201
DOI : 10.1007/BFb0013087

F. Bellegarde and P. Lescanne, Termination by completion, Applicable Algebra in Engineering, Communication and Computing, vol.3, issue.2, pp.79-96, 1990.
DOI : 10.1145/322217.322230

URL : https://hal.archives-ouvertes.fr/inria-00075384

A. Bouhoula, Preuves A utomatiques par Récurrence dans les Théories Conditionnelles, Thèse de Doctorat d'Université, 1994.

S. Walter and . Brainerd, Thee generating regular systems, Information and Control, vol.14, pp.217-231, 1969.

B. Bogaert and S. Tison, Automata with equality test, 1991.

B. Bogaert and S. Tison, Equality and disequality constraints on direct subterms in tree automata, Proceedings of the 9th Symposium on Theoretical Computer Science, pp.161-172, 1992.
DOI : 10.1007/3-540-55210-3_181

M. Clavel, F. Duran, S. Eker, P. Lincoln, and J. Meseguer, An Introduction to Maude (Beta Version), 1998.

C. J. Coquidé, M. Dauchet, R. Gilleron, and S. Vagvolgyi, Bottom-up tree pushdown automata and rewrite systems, Proceedings 4th Conference on Rewriting Techniques and ApplicationsCorn] H. Comon. About proofs by consistency. Invited talk at RTA'98, pp.287-298, 1991.
DOI : 10.1007/3-540-53904-2_104

]. H. Com86 and . Camon, Sufficient completeness, term rewriting system and anti-unification, Proceedings 8th International Conference on Automated Deduction, pp.128-140, 1986.

]. H. Com90 and . Comon, Solving Inequations in term algebras, Proceedings 5th IEEE Symposium on Logic in Computer Science, pp.62-69, 1990.

J. [. Comon and . Rémy, How to characterize the language of ground normal forms, Technical Report, vol.676, 1987.
URL : https://hal.archives-ouvertes.fr/inria-00075877

]. M. Dau89 and . Dauchet, Simulation of Turing machines by a left-linear rewrite ruie, Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (N. C., USA), pp.109-120, 1989.

]. N. Der82 and . Dershowitz, Orderings for term-rewriting systems. Theoretical Compute?' Science, pp.279-301, 1982.

N. Der87j and . Dershowitz, Termination of rewriting, Special issue on Rewriting Techniques and Applications, pp.69-116, 1987.

N. Der95} and . Dershowitz, Hierarchical termination, Proceedings 4th International Workshop on Conditional Term Rewriting Systems, pp.89-105, 1995.

C. [. Dershowitz and . Hoot, Natural termination, Theoretical Computer Science, vol.142, issue.2, pp.179-207, 1995.
DOI : 10.1016/0304-3975(94)00275-4

J. [. Dershowitz and . Jouannaud, Handbook of Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pp.244-320, 1990.

Z. [. Dershowitz and . Manna, Proving termination with multiset orderings, Communications of the ACM, vol.22, issue.8, pp.465-476, 1979.
DOI : 10.1145/359138.359142

M. [. Dershowitz, G. Okada, . Sivakumar, and . Ca, 1onical conditional rewrite systems, Proceedings 9th International Conference on Automated Deduction, Argonne (Ill., USA), 1988.

S. [. Dauchet and . 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

F. R. Forgaard and D. Detlefs, An incremental algorithm for proving termination of term rewriting systems, Proceedings lst Conference on Rewriting Techniques and Applications, pp.255-270, 1985.

]. M. Fer95 and . Ferreira, T'ermination of Rewriting, 1995.

J. [. Forgaard and . Guttag, Reve: A term rewriting system generator with failure-resistant Knuth-Bendix, 1984.

]. Gau84 and . Gaudel, A first introduction to pluss. Meteor report, LRI, 1984.

R. [. Gallier and . Book, Reductions in tree replacement systems, Theoretical Computer Science, vol.37, pp.123-150, 1985.
DOI : 10.1016/0304-3975(85)90089-1

T. Genet, Decidable approximations of sets of descendants and sets of normal forms (extended version), 1997.
URL : https://hal.archives-ouvertes.fr/inria-00073364

T. Genet, Proving termination of sequential reduction relation using tree automata, 1997.

]. T. Gen98 and . Genet, Decidable approximations of sets of descendants and sets of normal forms, Proceedings 9th Conference on Rewriting Techniques and Applications, pp.151-165, 1998.

O. Geu89j and . Geupel, Overlap closure and termination of term rewriting systems, 1989.

T. Genet and I. Gnaedig, Termination proofs using gpo ordering constraints, Proceedings 22nd International Colloquium on Trees in Algebra and Programming, pp.249-260, 1997.
DOI : 10.1007/BFb0030601

URL : https://hal.archives-ouvertes.fr/inria-00073604

T. Genet and I. Gnaedig, Termination proofs using gpo ordering constraints (extended version), 1997.
URL : https://hal.archives-ouvertes.fr/inria-00073604

J. [. Guttag, S. J. Horning, K. D. Garland, A. Jones, J. M. Modet et al., Larch: Languages and Tools for Formal Specification, 1993.
DOI : 10.1007/978-1-4612-2704-5

URL : http://www.ii.uib.no/~magne/i123-tekster/larchbook-1993-utdrag.ps

]. J. Gie95a and . Giesl, Generating polynomial orderings for termination proofs, Proceedings 6th Conference on Rewriting Techniques and Applications, 1995.

J. Giesl, Polo -a system for termination proofs using polynomial orderings, 1995.

]. I. Gna92 and . Gnaedig, Termination of order-sorted rewriting, Proceedings 3m International Conference on Aigebraic and Logic Programming, pp.37-52, 1992.

). B. Gra94 and . Gramlich, Generalized sufficient conditions for modular termination of rewriting, Applicable Algebra in Engineering, Communication and Computation, vol.5, pp.131-158, 1994.

[. Gramlich, Termination and Confluence Properties of Structured Rewrite Systems, 1996.

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

T. [. Goguen and . Winkler, Introducing OBJ3, 1988.

D. [. Huet and . Lankford, On the uniform halting problem for term rewriting systems, Proof of termination of the rewriting system SUBST on CCL. Theoretical Computer Science, pp.205305-312, 1978.

]. C. Hoo97 and . Hoot, Termination of non-simple rewrite systems, 1997.

]. F. Jac96a and . Jacquemard, Automates d'arbres et réécriture de termes, 1996.

F. Jac96bj and . Jacquemard, Decidable approximations of term rewriting systems, Proceedings 7th Conference on Rewriting Techniques and Applications, pp.362-376, 1996.

[. Jouannaud and P. Lescanne, On multiset orderings, Information Processing Letters, vol.15, issue.2, pp.57-63, 1982.
DOI : 10.1016/0020-0190(82)90107-7

[. Johann and R. Socher-ambrosius, Solving simplification ordering constraints
DOI : 10.1007/BFb0016865

[. Jouannaud and B. Waldmann, Reductive conditional term rewriting systems

]. S. Kap84, ]. S. Kaplankap87, and . Kaplan, Fair conditional term rewriting systems: Unification, termination, and confluence Simplifying conditional term rewriting systems: Unification, termination and confluence, Journal of Symbolic Computation, vol.4, issue.3, pp.295-334, 1984.

E. Donald, P. B. Knuth, and . Bendix, Simple word problems in universal algebras

I. [. Kurihara and . Kaji, Modular term rewriting systems and the termination, Information Processing Letters, vol.34, issue.1, pp.1-4, 1990.
DOI : 10.1016/0020-0190(90)90221-I

J. [. Kamin and . Lévy, Two generalizations ofthe recursive path ordering, 1980.

K. S. Kamin and J. Lévy, Attempts for generalizing the recursive path ordering, 1982.

]. P. Kli93 and . Klint, The ASF+SDF Meta-environment User's Guide, 1993.

K. M. Krishnamoorthy and P. Narendran, A note on recursive path ordering, Theoretical Computer Science, pp.323-328, 1985.

D. Kapur, P. Narendran, and H. Zhang, On sufficient-completeness and related properties of term rewriting systems, Acta Informatica, vol.6, issue.5, pp.395-415, 1987.
DOI : 10.1016/B978-0-08-012975-4.50028-X

M. Kurihara and A. Ohuchi, Modular term rewriting systems with shared constructors, Journal of Information Processing of Japan, vol.14, issue.3, pp.357-358, 1991.
DOI : 10.1016/0304-3975(92)90015-8

URL : https://doi.org/10.1016/0304-3975(92)90015-8

]. E. Kou85 and . Kounalis, Completeness in data type specifications, Proceedings EUROCAL Conference, Linz (Austria), pp.348-362, 1985.

J. B. Kru60}, Well-quasi ordering, the tree theorem and Vazsonyi's conjecture, Trans. Amer. Math. Soc, vol.95, pp.210-225, 1960.

]. D. Lan75 and . Lankford, Canonical algebraic simplifications, 1975.

]. D. Lan79 and . Lankford, On proving term rewriting systems are noetherian, 1979.

]. P. Les83 and . Lescanne, Computer experiments with the REVE term rewriting systems generator, Proceedings of 10th ACM Symposium on Principles of Programming Languages, pp.99-108, 1983.

P. Les84} and . Lescanne, Uniform termÏnation of term rewriting systems Recursive decomposition ordering with status A finite termÏnation criterion, Proceedings 9th Colloquium on Trees in Aigebra and Programming, pp.182-194, 1978.

P. [. Limet and . Réty, E-unification by means of tree tuple synchronized grammars, Proceedings 22nd International Colloquium on Trees in Algebra and Programming, pp.429-440, 1997.
DOI : 10.1007/BFb0030616

URL : https://hal.archives-ouvertes.fr/hal-00809528

C. Lynch and P. Strogova, Sour graphs for efficient completion, 1995.
URL : https://hal.archives-ouvertes.fr/hal-00958899

B. [. Middeldorp and . Gramlich, Simple termination is difficult, Applicable Aigebra in Engineering, Communication and Computation, 1994.
DOI : 10.1007/bf01225647

URL : http://www.score.is.tsukuba.ac.jp/~ami/research/papers/aaecc95.ps.gz

]. A. Mid89 and . Middeldorp, A sufficient condition for the termination of the direct sum of term rewriting systems, Proceedings 4th IEEE Symposium on Logic in Computer Science, pp.396-401, 1989.

]. A. Mid90 and . Middeldorp, Modular Properties of Term Rewriting Systems, 1990.

S. [. Manna and . Ness, On the termination of markov algorithms, Third Hawai International Conference on System Sciences, pp.789-792, 1970.

]. J. Mon81 and . Mongy, Transformations de noyaux reconnaissables d'arbres

P. Moreau, A choice-point library for backtrack programming, JICSLP'9S Post-Conference Workshop on Implementation Technologies for Programming Languages based on Logic, 1998.

M. Meier and J. Schimpf, ECLiPSe User Manual, ECRC, 1993.

]. M. New42 and . Newman, On theories with a combinatorial definition of equivalence, Annals of Math, pp.223-243, 1942.

R. Nieuwenhuis, Simple LPO constraint solving methods, Information Processing Letters, vol.47, issue.2, 1993.
DOI : 10.1016/0020-0190(93)90226-Y

URL : http://www.lsi.upc.es/~roberto/papers/ipl93.ps.gz

R. Nieuwenhuis and A. Rubio, Theorem proving with ordering constrained clauses
DOI : 10.1007/3-540-55602-8_186

G. [. Nipkow and . Weikum, A decidability result about sufficient-completeness of axiomatically specified abstract data types, 6th GI Conference, pp.257-268, 1983.
DOI : 10.1007/BFb0036486

P. Olveszky, C. , and O. Lysne, Order-sorted termination: The unsorted way, Michael Hanus and Mario Hanus Proceedings 5th International Conference on Aigebraic and Logic Programming, pp.92-106, 1996.
DOI : 10.1007/3-540-61735-3_6

]. E. Ohi94 and . Ohlebusch, Modular Properties of Composable Term Rewriting Systems, 1994.

]. D. Pla93 and . Plaisted, Polynomial time termination and constraint satisfaction tests, Proceedings 5th Conference on Rewriting Techniques and Applications, pp.405-420, 1993.

]. C. Roc97 and . Rocques, Modularité dans les spécifications algébriques, 1997.

]. M. Rus87 and . Rusinowitch, On termination of the direct sum of term rewriting systems, Information Processing Letters, vol.26, issue.2, pp.65-70, 1987.

]. K. Sa188 and . Salomaa, Deterministic Tree Pushdown Automata and Monadic Tree Rewriting Systems, Journal of Computer and System Sciences, vol.37, pp.367-394, 1988.

U. [. Steinbach and . Kühler, Check your ordering -termination proofs and open problems, 1993.

]. J. Ste89 and . Steinbach, Extensions and comparisons of simplification orderings, Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (N. C., USA), pp.434-448, 1989.

J. Steinbach, Generating polynomial orderings, Information Processing Letters, vol.49, issue.2, pp.85-93, 1994.
DOI : 10.1016/0020-0190(94)90032-9

J. Steinbach, Simplification orderings: history of results, Fundamenta Informaticae, vol.24, pp.47-87, 1995.

. Toyama, Counterexamples to termination for the direct sum of term rewriting systems, Information Processing Letters, vol.25, issue.3, pp.141-143, 1986.
DOI : 10.1016/0020-0190(87)90122-0

C. Walther, On proving the termination of algorithms by machine, Artificial Intelligence, vol.71, issue.1, 1994.
DOI : 10.1016/0004-3702(94)90063-9

H. Zantema, Termination of term rewriting: interpretation and type elimination, Journal of Symbolic Computation, vol.17, issue.1, pp.23-50, 1994.
DOI : 10.1006/jsco.1994.1003

H. Zantema, Termination of term rewriting by semantic labelling, Fundamenta Informaticae, vol.24, pp.89-105, 1995.