I. Fissore, H. Gnaedig, and . 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

J. Fuhs, M. Giesl, P. Parting, S. Schneider-kamp, and . Swiderski, Proving Termination by Dependency Pairs and Inductive Theorem Proving, Journal of Automated Reasoning, vol.17, issue.1, pp.133-160, 2011.
DOI : 10.1007/s10817-010-9215-9

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.226.2845

A. Giesl and . Middeldorp, Innermost Termination of Context-Sensitive Rewriting, DLT '02, pp.231-244, 2002.
DOI : 10.1007/3-540-45005-X_20

A. Giesl and . Middeldorp, Transformation techniques for context-sensitive rewrite systems, Journal of functional Programming, vol.14, issue.4, pp.379-427, 2004.
DOI : 10.1017/S0956796803004945

M. Giesl, P. Raffelsieper, S. Schneider-kamp, R. Swiderski, and . Thiemann, Automated termination proofs for haskell by term rewriting, ACM Transactions on Programming Languages and Systems, vol.33, issue.2, p.7, 2011.
DOI : 10.1145/1890028.1890030

R. Giesl, S. Thiemann, and . Falke, Mechanizing and Improving Dependency Pairs, Journal of Automated Reasoning, vol.34, issue.2, 2006.
DOI : 10.1007/s10817-006-9057-7

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.302

H. Gnaedig and . Kirchner, Termination of rewriting under strategies, ACM Transactions on Computational Logic, vol.10, issue.2, 2009.
DOI : 10.1145/1462179.1462182

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

. Gräf, Left-to-right tree pattern matching, RTA '91, pp.323-334, 1991.
DOI : 10.1007/3-540-53904-2_107

A. Hirokawa and . Middeldorp, Automating the dependency pair method. Information and Computation, pp.172-199, 2005.

-. Jouannaud and C. Kirchner, Solving equations in abstract algebras: a rule-based survey of unification Completion of a set of rules modulo a set of equations, Computational Logic. Essays in honor of Alan Robinson, pp.257-3211155, 1986.

R. Kaiser and . Lämmel, An Isabelle/HOL-based model of stratego-like traversal strategies, Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, PPDP '09, pp.93-104, 2009.
DOI : 10.1145/1599410.1599423

C. Korp, H. Sternagel, A. Zankl, and . Middeldorp, Tyrolean Termination Tool 2, RTA '09, pp.295-304, 2009.
DOI : 10.1007/978-3-540-70590-1_23

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.514.8829

S. J. Lämmel, M. Thompson, and . Kaiser, Programming errors in traversal programs over structured data, Science of Computer Programming, vol.78, issue.10, pp.1770-1808, 2013.
DOI : 10.1016/j.scico.2011.11.006

C. Meseguer and . Braga, Modular Rewriting Semantics of Programming Languages, Algebraic Methodology and Software Technology, pp.364-378
DOI : 10.1007/978-3-540-27815-3_29

-. Moreau, C. Ringeissen, and M. Vittek, A Pattern Matching Compiler for Multiple Target Languages, CC '03, pp.61-76, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099427

H. Raffelsieper and . Zantema, A Transformational Approach to Prove Outermost Termination Automatically, Electronic Notes in Theoretical Computer Science, vol.237, pp.3-21, 2009.
DOI : 10.1016/j.entcs.2009.03.032

URL : http://doi.org/10.1016/j.entcs.2009.03.032

. Thiemann, From Outermost Termination to Innermost Termination, SOFSEM '09, pp.533-545, 2009.
DOI : 10.1007/978-3-540-70590-1_25

A. Thiemann and . Middeldorp, Innermost Termination of Rewrite Systems by Labeling, Electronic Notes in Theoretical Computer Science, vol.204, pp.3-19, 2008.
DOI : 10.1016/j.entcs.2008.03.050

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

Z. Visser, A. Benaissa, and . Tolmach, Building program optimizers with rewriting strategiest j ) for all j < i and S ? t i =? u i , and thus, One(S ) ? t =? u. Note that we can always get an u i ? T F at some point since otherwise we would eventually obtain the term ? fn (?(t 1 ), . . . , ?(t n )) which can be reduce only to ?(f (t 1 , . . . , t n )) which is not a term in T F and thus contradicts the original hypothesis. If B(?)?T (One(S ))?? One(S ) (t) ?? ?(t) and t is not a constant, because ? One(S ) (t) is in normal form wLemma 7), the first reduction can only be ? One(S ) (f (x 1 , t n ) and no rule can be applied at the top position until the ? S (t 1 ) is reduced to a term in T F or to a term of the form ?( ) As we have seen just before, the former case leads to a term in T F which does not correspond to our hypothesis. We have also already handled the second case but we supposed that at some point we have B(?) ? T (S ) ? ? S (t i ) ?? u i which would lead to an eventual reduction to a term in T F which, once again, does not correspond to our hypothesis. The only remaining possibility is B(?) ? T (S ) ? ? S (t i ) ?? ?( ) for all i ? n and thust i ) (in less steps than the original reduction) for all i ? n, ICFP '98 this case we have ? ? One(S ) (f (t 1 , . . . , t n )) ?? ? f1 (? S (t 1 ), t 2 , this case, we obtain ? fn (?(x 1 ), . . . , ?(x n )) ?(f (x 1 , . . . , x n )) ? ? fn (?(t 1 ), . . . , ?(t n )) ?? ?(f (t 1 , . . . , t n )). By induction, S ? t i =? Fail and thus One(S ) ? f (t 1 , . . . , t n ) =? Fail. If t is a constant c then ? One(S ) (c) ?(c) ? ? One(S ) (c) ?? ?(c). We also have One(S ) ? c =? Fail, pp.13-26, 1998.