C. The, To prove Lemma 6.2.1, we need the next three lemmas. The first two ones are pretty obvious from the definition of the usable rules

C. Lemma, Let R be a rewrite system on a set F of symbols and t ? T (F, X ? X A ) Then, every symbol f ? F occurring in t is such that Rls(f ) ? U(t)

?. X. ?if-t, the property is trivially true; ?if t is a constant a, U(t = a) = Rls(a) ? l?r?Rls(a) U(r); the only symbol of t is a, and we have Rls

C. Lemma, Let R be a rewrite system on a set F of symbols and

C. Lemma and ?. T. , For any ground normalized substitution ? and any rewrite chain ?t ? p1,l1?r1 t 1 ? p2,l2?r2 t 2 ? . . . ? pn,ln?rn t n , the defined symbol of t k , 1 ? k ? n at a redex position of t k is either a symbol of t or one of the r i

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

T. Arts and J. Giesl, Termination of term rewriting using dependency pairs, Theoretical Computer Science, vol.236, issue.1-2, pp.133-178, 2000.
DOI : 10.1016/S0304-3975(99)00207-8

B. Cherifa, A. Lescanne, and P. , Termination of rewriting systems by polynomial interpretations and its implementation, Science of Computer Programming, vol.9, issue.2, pp.137-160, 1987.
DOI : 10.1016/0167-6423(87)90030-X
URL : https://hal.archives-ouvertes.fr/inria-00075876

C. Borelleras, M. Ferreira, and A. Rubio, Complete Monotonic Semantic Path Orderings, Proceedings of the 17th International Conference on Automated Deduction, pp.346-364, 2000.
DOI : 10.1007/10721959_27

P. Borovansk´yborovansk´y, C. Kirchner, H. Kirchner, P. Moreau, and C. And-ringeissen, An Overview of ELAN, Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications Electronic Notes in Theoretical Computer Science, 1998.

M. Clavel, S. Eker, P. Lincoln, and J. Meseguer, Principles of Maude, Proceedings of the 1st International Workshop on Rewriting Logic and its Applications, 1996.
DOI : 10.1016/S1571-0661(04)00034-9

H. Comon, Disunification: a survey Essays in honor of Alan Robinson, Computational Logic, pp.322-359, 1991.

N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982.
DOI : 10.1016/0304-3975(82)90026-3

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

N. Dershowitz and J. Jouannaud, Handbook of Theoretical Computer Science, Chapter 6: Rewrite Systems, pp.244-320, 1990.

S. Eker, Term Rewriting with Operator Evaluation Strategies, Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications, 1998.
DOI : 10.1016/S1571-0661(05)80019-2

M. Fernández, G. Godoy, and A. Rubio, Orderings for Innermost Termination, RTA, pp.17-31, 2005.
DOI : 10.1007/978-3-540-32033-3_3

O. Fissore, Terminaison de la réécriture sous stratégies, 2003.

O. Fissore, I. Gnaedig, and H. Kirchner, Termination of rewriting with local strategies, Eds. Electronic Notes in Theoretical Computer Science, vol.58, 2001.

O. Fissore, I. Gnaedig, and H. Kirchner, CARIBOO : An induction based proof tool for termination with strategies, Proceedings of the 4th International Conference on Principles and Practice of Declarative Programming, pp.62-73, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00107557

O. Fissore, I. Gnaedig, and H. Kirchner, Outermost Ground Termination, Proceedings of the 4th International Workshop on Rewriting Logic and Its Applications, 2002.
DOI : 10.1016/S1571-0661(05)82535-6
URL : https://hal.archives-ouvertes.fr/inria-00099654

O. Fissore, I. Gnaedig, and H. Kirchner, Outermost ground termination -Extended version, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00101079

O. Fissore, I. Gnaedig, and H. Kirchner, CARIBOO: A multi-strategy termination proof tool based on induction, Proceedings of the 6th International Workshop on Termination 2003, pp.77-79, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099467

O. Fissore, I. Gnaedig, and H. Kirchner, Simplification and termination of strategies in rule-based languages, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming , PPDP '03, pp.124-135, 2003.
DOI : 10.1145/888251.888264
URL : https://hal.archives-ouvertes.fr/inria-00099655

O. Fissore, I. Gnaedig, and H. Kirchner, A Proof of Weak Termination Providing the Right Way to Terminate, 1st International Colloquium on, pp.356-371, 2004.
DOI : 10.1007/978-3-540-31862-0_26
URL : https://hal.archives-ouvertes.fr/inria-00100120

O. Fissore, I. Gnaedig, H. Kirchner, and L. Moussa, Cariboo, a termination proof tool for rewriting-based programming languages with strategies, Version 1.1. Free GPL Licence, APP registration IDDN, 2005.

K. Futatsugi and A. Nakagawa, An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks, Proceedings First IEEE International Conference on Formal Engineering Methods, 1997.
DOI : 10.1109/ICFEM.1997.630424

T. Genet, Decidable approximations of sets of descendants and sets of normal forms, Proceedings 9th Conference on Rewriting Techniques and Applications, 1998.
DOI : 10.1007/BFb0052368
URL : https://hal.archives-ouvertes.fr/inria-00073364

J. Giesl and A. Middeldorp, Transforming Context-Sensitive Rewrite Systems, Proceedings of the 10th International Conference on Rewriting Techniques and Applications, pp.271-285, 1999.
DOI : 10.1007/3-540-48685-2_23

J. Giesl and A. Middeldorp, Innermost Termination of Context-Sensitive Rewriting, Proceedings of the 6th International Conference on Developments in Language Theory, pp.231-244, 2002.
DOI : 10.1007/3-540-45005-X_20

J. Giesl, R. Thiemann, P. Schneider-kamp, and S. Falke, Improving Dependency Pairs, Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '03, pp.165-179, 2003.
DOI : 10.1007/978-3-540-39813-4_11

I. Gnaedig and H. Kirchner, Computing constructor forms with non terminating rewrite programs, Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming , PPDP '06, pp.121-132, 2006.
DOI : 10.1145/1140335.1140351
URL : https://hal.archives-ouvertes.fr/inria-00112083

I. Gnaedig, H. Kirchner, and T. Genet, Induction for Termination, 1999.
URL : https://hal.archives-ouvertes.fr/inria-00099315

J. Goubault-larreck, Well-Founded Recursive Relations, Proc. 15th Int. Workshop Computer Science Logic (CSL'2001, 2001.
DOI : 10.1007/3-540-44802-0_34

B. Gramlich, Abstract relations between restricted termination and confluence properties of rewrite systems, Fundamenta Informaticae, vol.24, pp.3-23, 1995.

B. Gramlich, On proving termination by innermost termination, Proceedings 7th Conference on Rewriting Techniques and Applications, pp.93-107, 1996.
DOI : 10.1007/3-540-61464-8_45

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

C. Kirchner, Strategic Rewriting, Electronic Notes in Theoretical Computer Science, vol.124, issue.2, pp.3-9, 2005.
DOI : 10.1016/j.entcs.2004.11.017
URL : https://hal.archives-ouvertes.fr/inria-00107802

C. Kirchner, H. Kirchner, and M. Rusinowitch, Deduction with symbolic constraints. Revue d, Intelligence Artificielle, vol.4, issue.3, pp.9-52, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00077103

P. Klint, A meta-environment for generating programming environments, ACM Transactions on Software Engineering and Methodology, vol.2, issue.2, pp.176-201, 1993.
DOI : 10.1145/151257.151260

K. Rao and M. , Some characteristics of strong normalization, Theoretical Computer Science, vol.239, pp.141-164, 2000.

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

D. S. Lankford, On proving term rewriting systems are noetherian, 1979.

S. Lucas, Termination of context-sensitive rewriting by rewriting, Proceedings of the 23rd International Colloquium on Automata, Languages and Programming, pp.122-133, 1996.
DOI : 10.1007/3-540-61440-0_122

S. Lucas, Termination of on-demand rewriting and termination of OBJ programs, Proceedings of the 3rd ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '01, pp.82-93, 2001.
DOI : 10.1145/773184.773194

S. Lucas, Termination of Rewriting with Strategy Annotations, Proc. of 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp.669-684, 2001.
DOI : 10.1007/3-540-45653-8_46

S. Lucas, Context-Sensitive Rewriting Strategies, Information and Computation, vol.178, issue.1, pp.294-343, 2002.
DOI : 10.1016/S0890-5401(02)93176-7

A. Middeldorp and E. Hamoen, Completeness results for basic narrowing, Applicable Algebra in Engineering, Communication and Computing, vol.7, issue.1, pp.213-253, 1994.
DOI : 10.1007/BF01190830

P. Moreau, C. Ringeissen, and M. Vittek, A Pattern Matching Compiler for Multiple Target Languages, 12th Conference on Compiler Construction, pp.61-76, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099427

M. Nakamura and K. Ogata, The evaluation strategy for head normal form with and without on-demand flags, Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications, pp.211-227, 2000.
DOI : 10.1016/S1571-0661(05)80143-4

Q. Nguyen, Compact Normalisation Trace via Lazy Rewriting, Proc. 1st International Workshop on Reduction Strategies in Rewriting and Programming, 2001.
DOI : 10.1016/S1571-0661(04)00269-5
URL : https://hal.archives-ouvertes.fr/inria-00107874

S. E. Panitz and M. Schmidt-schauss, TEA: Automatically proving termination of programs in a non-strict higher-order functional language, Proceedings of Static Analysis Symposium'97, pp.345-360, 1997.
DOI : 10.1007/BFb0032752

D. Plaisted, Well-founded orderings for proving termination of systems of rewrite rules, 1978.

E. Visser, Stratego: A Language for Program Transformation Based on Rewriting Strategies System Description of Stratego 0.5, Rewriting Techniques and Applications (RTA'01, pp.357-361, 2001.
DOI : 10.1007/3-540-45127-7_27

E. Visser, Program Transformation with Stratego/XT, Eds. Lecture Notes in Computer Science, vol.3016, pp.216-238, 2004.
DOI : 10.1007/978-3-540-25935-0_13

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