J. C. Baeten, J. A. Bergstra, and J. W. Klop, Term rewriting systems with priorities, RTA 1987, vol.256, pp.83-94, 1987.
DOI : 10.1007/3-540-17220-3_8

URL : https://link.springer.com/content/pdf/10.1007%2F3-540-17220-3_8.pdf

J. C. Baeten, J. A. Bergstra, J. W. Klop, and W. P. Weijland, Term-rewriting systems with rule priorities, Theoretical Computer Science, vol.67, issue.2-3, pp.283-301, 1989.
DOI : 10.1016/0304-3975(89)90006-6

URL : https://doi.org/10.1016/0304-3975(89)90006-6

M. G. Van-den-brand, P. Klint, and C. Verhoef, Term Rewriting for Sale, WRLA 1998, vol.15, pp.139-161, 1998.

N. Marti-oliet, J. Meseguer, and A. Verdejo, Towards a strategy language for Maude, WRLA 2004, vol.117, pp.417-441, 2004.

R. Plasmeijer and M. Van-eekelen, Functional Programming and Parallel Graph Rewriting, 1993.

L. Augustsson, A compiler for lazy ML, LFP 1984, pp.218-227, 1984.
DOI : 10.1145/800055.802038

A. S. De-oliveira, Réécriture et Modularité pour les Politiques de Sécurité, 2008.

A. S. De-oliveira, E. K. Wang, C. Kirchner, and H. Kirchner, Weaving rewrite-based access control policies, FMSE 2007, pp.71-80, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00185710

C. K. Mohan, Priority rewriting: Semantics, confluence, and conditionals, vol.355, pp.278-291, 1989.
DOI : 10.1007/3-540-51081-8_114

J. Van-de-pol, Operational semantics of rewriting with priorities, Theoretical Computer Science, vol.200, issue.1-2, pp.289-312, 1998.

M. Sakai and Y. Toyama, Semantics and strong sequentiality of priority term rewriting systems, Theoretical Computer Science, vol.208, issue.1-2, pp.87-110, 1998.
DOI : 10.1016/s0304-3975(98)00080-2

URL : https://doi.org/10.1016/s0304-3975(98)00080-2

J. Van-de-pol and H. Zantema, Generalized innermost rewriting, RTA 2005, vol.3467, pp.2-16, 2005.

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

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

F. Baader and T. Nipkow, Term rewriting and all that, 1998.

T. , Term Rewriting Systems. Number 55 in Cambridge Tracts in Theoretical Computer Science, 2003.

I. Gnaedig, Termination of Priority Rewriting-Extended Version. HAL-INRIA Open Archive Number, 2008.
DOI : 10.1007/978-3-642-00982-2_33

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

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

H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard et al., Tree automata techniques and applications, 2007.

T. Arts and J. Giesl, Proving innermost normalisation automatically, RTA 1997, vol.1232, pp.157-171, 1997.
DOI : 10.1007/3-540-62950-5_68

URL : https://dspace.library.uu.nl/bitstream/1874/18360/1/arts_97_proving.pdf

D. J. Dougherty, K. Fisler, and S. Krishnamurthi, Specifying and reasoning about dynamic access-control policies, IJCAR 2006, vol.4130, pp.632-646, 2006.
DOI : 10.1007/11814771_51

URL : http://www.cs.wpi.edu/~kfisler/Pubs/ijcar06.pdf

, For the proof of the lemma, we need the two following propositions

, Proposition 1. Let t ? T (F, X ) and ? be a substitution of T (F, X ). Then V ar(?t) = (V ar(t) ? Dom(?)) ? Ran

, Suppose we have substitutions ?, µ, ? and sets A, B of variables such that (B ? Dom(?)) ? Ran(?) ? A

. Proof, Let us consider (µ?) B , which can be divided as follows: (µ?) B = (µ?) B?Dom(?) ? (µ?) B?Dom(?)

. For-x-?-b-?-dom, we have Var (?x) ? Ran(?), and then (µ?)x = µ(?x) = µ Ran(?) (?x) = (µ Ran(?) ?)x. Therefore (µ?) B?Dom(?) = (µ Ran(?) ?) B?Dom(?)

. For-x-?-b-?-dom, we have ?x = x, and then (µ?)x = µ(?x) = µx. Therefore we have (µ?) B?Dom(?) = µ B?Dom(?), Henceforth we get (µ?) B = (µ Ran(?) ?) B?Dom(?) ?µ B?Dom(?)

, By a similar reasoning, we get (??) B = (? Ran(?) ?) B?Dom(?) ? ? B?Dom(?). By hypothesis, we have Ran(?) ? A and µ = ?

, Then we have (µ?) B = (µ Ran(?) ?) B?Dom(?) ? µ B?Dom(?) = (? Ran(?) ?) B?Dom(?) ? ? B?Dom(?) = (??) B, Then µ Ran(?) = ? Ran(?)

, In the following, we assume that Y ? Var (l) = ? for every l ? r ? R. If ?s ? IP p,l?r t , then there is a substitution ? such that Dom(? ) ? Var (l) and (?s)| p = ? l. Moreover, since p is a non variable position of s, we have (?s)| p = ?(s| p ), Lemma 1)