G. Ro?u and T. F. ?erb?nu??, An overview of the K semantic framework, The Journal of Logic and Algebraic Programming, vol.79, issue.6, pp.397-434, 2010.
DOI : 10.1016/j.jlap.2010.03.012

M. Clavel, F. Durán, S. Eker, J. Meseguer, P. Lincoln et al., All About Maude, A High-Performance Logical Framework, LNCS, vol.4350, 2007.

A. Arusoaie, D. Lucanu, and V. Rusu, A Generic Framework for Symbolic Execution, 6th International Conference on Software Language Engineering, pp.281-301, 2013.
DOI : 10.1007/978-3-319-02654-1_16
URL : https://hal.archives-ouvertes.fr/hal-00853588

C. Rocha, J. Meseguer, and C. A. Muñoz, Rewriting modulo SMT and open system analysis, Journal of Logical and Algebraic Methods in Programming, vol.86, issue.1, pp.247-262, 2014.
DOI : 10.1016/j.jlamp.2016.10.001
URL : http://hdl.handle.net/2060/20150014338

D. Lucanu and T. F. ?erb?nu??, CinK -an exercise on how to think in K, 2013.

G. Ro?u and A. ?tef?nescu, Checking reachability using matching logic, OOPSLA, ACM, pp.555-574, 2012.

F. Durán and J. Meseguer, On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, The Journal of Logic and Algebraic Programming, vol.81, issue.7-8, pp.816-850, 2012.
DOI : 10.1016/j.jlap.2011.12.004

P. Viry, Equational rules for rewriting logic, Theoretical Computer Science, vol.285, issue.2, pp.487-517, 2002.
DOI : 10.1016/S0304-3975(01)00366-8
URL : http://doi.org/10.1016/s0304-3975(01)00366-8

J. Meseguer, Software specification and verification in rewriting logic, 2003.

G. Ro?u, A. ?tef?nescu, ?. Ciobâc?, and B. M. Moore, One-path reachability logic, Proceedings of the 28th Symposium on Logic in Computer Science (LICS'13), pp.358-367, 2013.

J. Meseguer, M. Palomino, and N. Martí-oliet, Equational abstractions, Theoretical Computer Science, vol.403, issue.2-3, pp.239-264, 2008.
DOI : 10.1016/j.tcs.2008.04.040
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.183.9812

A. Farzan and J. Meseguer, State Space Reduction of Rewrite Theories Using Invisible Transitions, Proceedings of the 21st German Annual Conference on Artificial Intelligence, pp.142-157, 2006.
DOI : 10.1007/11784180_13

L. M. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, Lecture Notes in Computer Science, vol.4963, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

T. F. ?erbanu?? and G. Ro?u, K-Maude: A Rewriting Based Tool for Semantics of Programming Languages, Rewriting Logic and Its Applications -8th International Workshop, pp.104-122, 2010.
DOI : 10.1007/978-3-642-16310-4_8

D. Lucanu, T. F. ?erb?nu??, and G. Ro?u, $\mathbb{K}$ Framework Distilled, 9th International Workshop on Rewriting Logic and its Applications, pp.31-53, 2012.
DOI : 10.1007/978-3-642-34005-5_3

T. Cfg, T. =. , and D. , If ? 1 and ? are concretely unifiable there is a valuation ? : Var ? T (?\? d )(D) such that ?(? 1 ) = A ?(?) We obtain ?(? 1 ) ? = A ?(?(?) ? ) by Lemma 8, where ? is a variable renaming There are a substitution ? 1 and a valuation ? 1 such that ? 1 (? 1 (y)) = ?(y), for all y ? Y , by Lemma 7. Moreover, ? 1 (? 1 ) = ?(? 1 ) ? by Corollary 5. Since ? includes only variables of data sort, it follows that any position p in the data-abstraction ?(?) ? is a position in ? as well and hence ? is an instance of ?(?) ? . It follows that ? is an instance of ?(?(?) ? ) as well, i.e. there is a substitution ? 2 such, that ? 2 ((?(?(?) ? )) = ?. From ?(? 1 ) ? = A ?(?(?) ? ) and ? 1 (? 1 ) = ?(? 1 ) ? we obtain ? 2 (? 1 (? 1 )) = A ? 2 (?(?(?) ? )) (= A is closed under substitution), which implies ? 2 (? 1 (? 1 )) = A ?, i.e. ? = ? 2 ? ? 1 is in match A (? 1 , ?)

@. and ?. Var, Then y ? Var d , which implies ? 1 (y) = y. Then ?(?(y)) = ?(? 2 (y)) = ?(y) by the definition of ?