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
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
Term Rewriting for Sale, WRLA 1998, vol.15, pp.139-161, 1998. ,
Towards a strategy language for Maude, WRLA 2004, vol.117, pp.417-441, 2004. ,
Functional Programming and Parallel Graph Rewriting, 1993. ,
A compiler for lazy ML, LFP 1984, pp.218-227, 1984. ,
DOI : 10.1145/800055.802038
, Réécriture et Modularité pour les Politiques de Sécurité, 2008.
Weaving rewrite-based access control policies, FMSE 2007, pp.71-80, 2007. ,
URL : https://hal.archives-ouvertes.fr/inria-00185710
, Priority rewriting: Semantics, confluence, and conditionals, vol.355, pp.278-291, 1989.
DOI : 10.1007/3-540-51081-8_114
Operational semantics of rewriting with priorities, Theoretical Computer Science, vol.200, issue.1-2, pp.289-312, 1998. ,
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
Generalized innermost rewriting, RTA 2005, vol.3467, pp.2-16, 2005. ,
A Pattern Matching Compiler for Multiple Target Languages, CC 2003, vol.2622, pp.61-76, 2003. ,
URL : https://hal.archives-ouvertes.fr/inria-00099427
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
Term rewriting and all that, 1998. ,
, Term Rewriting Systems. Number 55 in Cambridge Tracts in Theoretical Computer Science, 2003.
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
Well-quasi ordering, the tree theorem and Vazsonyi's conjecture, Trans. Amer. Math. Soc, vol.95, pp.210-225, 1960. ,
DOI : 10.2307/1993287
Tree automata techniques and applications, 2007. ,
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
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
Let us consider (µ?) B , which can be divided as follows: (µ?) B = (µ?) B?Dom(?) ? (µ?) B?Dom(?) ,
we have Var (?x) ? Ran(?), and then (µ?)x = µ(?x) = µ Ran(?) (?x) = (µ Ran(?) ?)x. Therefore (µ?) B?Dom(?) = (µ Ran(?) ?) 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)