J. C. Baeten, J. A. Bergstra, and J. W. Klop, Term rewriting systems with priorities, LNCS, vol.256, pp.83-94, 1987.
DOI : 10.1007/3-540-17220-3_8
URL : http://dspace.library.uu.nl:8080/handle/1874/12932

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

M. G. Van-den-brand, P. Klint, and C. Verhoef, Term Rewriting for Sale, Electronic Notes in Theoretical Computer Science, vol.15, pp.139-161, 1998.
DOI : 10.1016/S1571-0661(05)80014-3

N. Marti-oliet, J. Meseguer, and A. Verdejo, Towards a Strategy Language for Maude, Electronic Notes in Theoretical Computer Science, vol.117, pp.417-441, 2004.
DOI : 10.1016/j.entcs.2004.06.020

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

L. Augustsson, A compiler for lazy ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming , LFP '84, 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, Proceedings of the 2007 ACM workshop on Formal methods in security engineering , FMSE '07, pp.71-80, 2007.
DOI : 10.1145/1314436.1314446
URL : https://hal.archives-ouvertes.fr/inria-00185710

C. K. Mohan, Priority rewriting: Semantics, confluence, and conditionals, LNCS, 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.
DOI : 10.1016/S0304-3975(97)00283-1

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

J. Van-de-pol and H. Zantema, Generalized Innermost Rewriting, RTA 2005, pp.2-16, 2005.
DOI : 10.1007/978-3-540-32033-3_2

P. Moreau, C. Ringeissen, and M. Vittek, A Pattern Matching Compiler for Multiple Target Languages, LNCS, 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.

I. Gnaedig, Termination of Priority Rewriting -Extended Version. HAL-INRIA Open Archive Number inria, p.349031, 2008.
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, pp.95-210, 1960.

T. Arts and J. Giesl, Proving innermost normalisation automatically, LNCS, vol.1232, pp.157-171, 1997.
DOI : 10.1007/3-540-62950-5_68
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.722

D. J. Dougherty, K. Fisler, and S. Krishnamurthi, Specifying and Reasoning About Dynamic Access-Control Policies, LNCS, vol.4130, pp.632-646, 2006.
DOI : 10.1007/11814771_51
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.79.8098

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

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

?. For-x and . 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(?)