N. Martí-oliet and J. Meseguer, Rewriting logic: roadmap and bibliography, Theoretical Computer Science, vol.285, issue.2, pp.121-154, 2002.
DOI : 10.1016/S0304-3975(01)00357-7

M. All-about, A High-Performance Logical Framework, Lecture Notes in Computer Science, vol.4350, 2007.

P. Borovansky, C. Kirchner, H. Kirchner, P. ?. Moreau, and M. Vittek, ELAN, Proc. of the First Int. Workshop on Rewriting Logic, 1996.
DOI : 10.1016/S1571-0661(04)00032-5
URL : https://hal.archives-ouvertes.fr/inria-00098518

R. Diaconescu and K. Futatsugi, Logical foundations of CafeOBJ, Theoretical Computer Science, vol.285, issue.2, pp.289-318, 2002.
DOI : 10.1016/S0304-3975(01)00361-9

J. Meseguer, Membership algebra as a logical framework for equational specification, Lecture Notes in Computer Science, vol.1376, pp.18-61, 1997.
DOI : 10.1007/3-540-64299-4_26

R. Bruni and J. Meseguer, Semantic foundations for generalized rewrite theories, Theoretical Computer Science, vol.360, issue.1-3, pp.386-414, 2006.
DOI : 10.1016/j.tcs.2006.04.012

S. Eker, J. Meseguer, and A. Sridharanarayanan, The Maude LTL Model Checker, Electronic Notes in Theoretical Computer Science, vol.71, 2002.
DOI : 10.1016/S1571-0661(05)82534-4

J. Meseguer, M. Palomino, and N. Martí-oliet, Equational Abstractions, Lecture Notes in Computer Science, vol.2741, pp.2-16, 2003.
DOI : 10.1007/978-3-540-45085-6_2

M. Clavel, M. Palomino, and A. Riesco, Introducing the itp tool: a tutorial, J. Universal Computer Science, vol.12, issue.11, pp.1618-1650, 2006.

J. Meseguer and P. Thati, Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols, International Workshop on Rewriting Logic and Applications, 2004.

G. Ro¸suro¸su, Hidden Logic, 2000.

W. Kong, K. Ogata, and K. Futatsugi, Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System, Integrated Formal Methods, 6th International Conference IFM 2007, pp.393-412, 2007.
DOI : 10.1007/978-3-540-73210-5_21

M. Clavel, M. Palomino, and J. Santa-cruz, Integrating decision procedures in reflective rewriting-based theorem provers, 4th International Workshop on Reduction Strategies in Rewriting and Programming, pp.15-24, 2004.

E. ?. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-Guided Abstraction Refinement, Lecture Notes in Computer Science, vol.1855, pp.154-169, 2000.
DOI : 10.1007/10722167_15

S. Owre, J. Rushby, and N. Shankar, PVS: A prototype verification system, 11th International Conference on Automated Deduction (CADE), pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217

J. Rushby, Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving, Theoretical and Practical Aspects of SPIN Model Checking: 5th and 6th International SPIN Workshops, pp.1-11, 1999.
DOI : 10.1007/3-540-48234-2_1

. Proof, (?) is proved by routine induction on the number of rewrite rules used in R (?X)t ? t , and (?) is proved by routine induction on n

R. Assume, By Lemma 12, this means that there exists a kind-preserving substitution ? : X ? T ? (Y ) such that ? E (?Y )t = l?, hence, a fortiori )t : Reachable} (?Y )t = l?; then, using the Membership and Membership' rules of mel (cf, we obtain (e) E M(R) ? {(?Y )t : Reachable} (?Y )l? : Reachable