B. Bogaert and S. Tison, Equality and disequality constraints on direct subterms in tree automata, 9th Symp. on Theoretical Aspects of Computer Science, STACS, pp.161-171, 1992.
DOI : 10.1007/3-540-55210-3_181

A. Bouhoula, Using induction and rewriting to verify and complete parameterized specifications, Theoretical Computer Science, vol.170, issue.1-2, pp.245-276, 1996.
DOI : 10.1016/S0304-3975(96)80708-0

URL : http://doi.org/10.1016/s0304-3975(96)80708-0

A. Bouhoula and F. Jacquemard, Automated induction for complex data structures, 2005.

A. Bouhoula and J. Jouannaud, Automata-Driven Automated Induction, Information and Computation, vol.169, issue.1, pp.1-22, 2001.
DOI : 10.1006/inco.2001.3036

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

A. Bouhoula, J. Jouannaud, and J. Meseguer, Specification and proof in membership equational logic, Theoretical Computer Science, vol.236, issue.1-2, pp.35-132, 2000.
DOI : 10.1016/S0304-3975(99)00206-6

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

A. Bouhoula and M. Rusinowitch, Implicit induction in conditional theories, Journal of Automated Reasoning, vol.31, issue.2, pp.189-235, 1995.
DOI : 10.1007/BF00881856

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

H. Comon and F. Jacquemard, Ground reducibility is exptime-complete. Information and Computation, pp.123-153, 2003.
DOI : 10.1109/lics.1997.614922

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

H. Comon and V. Cortier, Tree automata with one memory set constraints and cryptographic protocols, Theoretical Computer Science, vol.331, issue.1, pp.143-214, 2005.
DOI : 10.1016/j.tcs.2004.09.036

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

N. Dershowitz and J. Jouannaud, Rewrite Systems, Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, pp.243-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

J. V. Guttag, The Specification and Application to Programming of Abstract Data Types, 1975.

J. V. Guttag, Notes on type abstraction, Program Construction, pp.593-616, 1978.
DOI : 10.1007/BFb0014684

J. V. Guttag and J. J. Horning, The algebraic specification of abstract data types, Acta Inf, vol.10, pp.27-52, 1978.

J. Hendrix, M. Clavel, and J. Meseguer, A Sufficient Completeness Reasoning Tool for Partial Specifications, Proc. ot the 16th Int. Conf. on Term Rewriting and Applications (RTA), pp.165-174, 2005.
DOI : 10.1007/978-3-540-32033-3_13

J. Hendrix, H. Ohsaki, and J. Meseguer, Sufficient completeness checking with propositional tree automata, 1825.
DOI : 10.1007/11805618_5

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

G. Huet and J. Hullot, Proofs by induction in equational theories with constructors, Journal of Computer and System Sciences, vol.25, issue.2, pp.239-266, 1982.
DOI : 10.1016/0022-0000(82)90006-X

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

D. Kapur, An automated tool for analyzing completeness of equational specifications, Proceedings of the 1994 international symposium on Software testing and analysis , ISSTA '94, pp.28-43, 1994.
DOI : 10.1145/186258.186496

D. Kapur, P. Narendran, D. J. Rosenkrantz, and H. Zhang, Sufficient-completeness, ground-reducibility and their complexity, Acta Informatica, vol.65, issue.4, pp.311-350, 1991.
DOI : 10.1007/BF01893885

D. Kapur, P. Narendran, and H. Zhang, On sufficient-completeness and related properties of term rewriting systems, Acta Informatica, vol.6, issue.5, pp.395-415, 1987.
DOI : 10.1007/BF00292110

E. Kounalis, Completeness in data type specifications, European Conference on Computer Algebra, pp.348-362, 1985.

A. Lazrek, P. Lescanne, and J. Thiel, Tools for proving inductive equalities, relative completeness, and ??-completeness, Information and Computation, vol.84, issue.1, pp.47-70, 1990.
DOI : 10.1016/0890-5401(90)90033-E

URL : http://doi.org/10.1016/0890-5401(90)90033-e

J. Misra, Powerlist: a structure for parallel recursion, ACM Transactions on Programming Languages and Systems, vol.16, issue.6, pp.1737-1767, 1994.
DOI : 10.1145/197320.197356