C. Annexe, Preuves des résultats concernant J'ordre de récurrence -Le deuxième cas serait al = 0:2, mais il n'est pas possible

C. Et-par-le-lemme, 5 appliqué à (C.15), on peut déterminer deux cas: -a,[u(t,)]w > a2, p.14

@. Q~, > lY(t,) par

. Dans-ce-cas-on, 2 > art,) par "'2 = a(t1) > art

~. Soit and A. , Dans ce cas par le lemme C.5 appliqué à (C.2Ü), on a trois sous-cas : ? al > Q~- Dans ce cas on a 0:1 > art,) par 0:1 >, p.2

C. Annexe, Preuves des résultats concernant l'ordre de récurrence

. La-règle-est-utilisée-après-avoir-réduit-le-but-en-oe~-~-o, Puisque 0:1 ::::: 0:2 -+n o:~ ~ a~, on a : par hypothèse, on a : a

C. Par-la-définition, 2 appliquée à (C.26), on peut déterminer trois cas : -0:1 > o:~

C. Et-par-le-lemme, S appliqué à (C.27), on peut déterminer deux sous-cas

. Dans-ce-cas, en reprenant la définition C.2 appliquée à (C.26), on a deux sous-cas * Soit OEl > a~, p.2

*. Soit and O. Oe~, 28) et a, > o-(t,) (C.3I), donc a

C. Et-par-le-lemme, S appliqué à (C.27), on peut déterminer deux sous-cas

. Dans-ce-cas, en reprenant la définition C.2 appliquée à (C.26), on a deux sous-cas * Soit QI > a~. Dans ce cas on a oe > o-(t2) par "'1>, pp.2-2

*. Soit and O. , Dans ce cas on a "2 > o-(t2) par, p.2

M. Abadi, L. Cardelli, P. Curien, and J. Lévy, Abstract, Journal of Functional Programming, vol.34, issue.04, pp.375-416, 1991.
DOI : 10.1016/B978-0-12-115350-2.50017-8

]. L. Bac88 and . Bachmair, Proofby consistency in equational theories, Proceedings 3rd IEEE Symposium on Logic in Computer Science, pp.228-233, 1988.

]. H. Bar84 and . Barendregt, The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics, 1984.

[. Barendregt and E. Barendsen, Autartik computations in formai proofs, 1997.

P. Borovansky, C. Kirchner, H. Kirchner, P. Moreau, and C. Ringeissen, An overview of ELAN html, Pont-à-Mousson (France), Proceedings of the second International Workshop on Rewriting Logic and Applications, 1998.

A. Bouhoula, E. Kounalis, and M. Rusinowitch, Automated Mathematical Induction, Journal of Logic and Computation, vol.5, issue.5, pp.631-668, 1995.
DOI : 10.1093/logcom/5.5.631

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

R. Bruni, J. Meseguer, and U. Montanari, Tiling Transactions in Rewriting Logic, Proceedings of the 4 t h International Workshop on Rewriting Logic and Its Applications, pp.43-62, 2002.
DOI : 10.1016/S1571-0661(05)82530-7

]. A. Bou94 and . Bouhoula, Preuves A utomatiques par Récurrence dans les Théories Conditionnelles, Thèse de Doctorat d'Université, 1994.

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

]. A. Bun01 and . Bundy, The automation of proofby mathematical induction, Handbook of Automated Reasoning, volume I, chapter 13, pp.845-911, 2001.

P. Curien, T. Hardin, and J. Lévy, Confluence properties of weak and strong calculi of explicit substitutions, Journal of the ACM, vol.43, issue.2, 1992.
DOI : 10.1145/226643.226675

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

E. Contejean and C. Marché, CiME: Completion modulo E, International Conference on Rewriting Techniques and Applications, pp.416-419, 1996.
DOI : 10.1007/3-540-61464-8_70

. Springer-verlag, System Description available at http :f/www

H. Comon and R. Nieuwenhuis, Induction=I-Axiomatization+First-Order Consistency, Information and Computation, vol.159, issue.1-2, pp.151-186, 2000.
DOI : 10.1006/inco.2000.2875

). H. Comol and . Comon, Induction!ess induction, Handbook of Automated Reasoning, pp.913-962, 2001.

N. De-bruijn, Lambda calculus notation with nameless dummies, a too1 for automatic formula manipulation, with application ta the chureh-rosser theorem, Indagationes Mathematicae, vol.34, issue.5, pp.381-392, 1972.

E. Deplagne, Une comparaison d'efficacité entre différents calculs de substitutions explicites, 1997.

E. Deplagne, Sequent calculus viewed modulo, Proceedings of the ESSLLI-2000 Student Session, pp.66-76, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00099056

N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982.
DOI : 10.1016/0304-3975(82)90026-3

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo Rapport de Recherche 3400, Institut National de Recherche en Informatique et en Automatique, 1998.

G. Dowek, T. Hardin, and C. Kirchner, Higher-order unification via explicit substit.utions. Information and Computation, pp.183-235, 2000.
DOI : 10.1109/lics.1995.523271

G. Dowek, T. Hardin, and C. Kirchner, HOL-????: an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, vol.11, issue.1, pp.21-45, 2001.
DOI : 10.1017/S0960129500003236

URL : https://hal.archives-ouvertes.fr/hal-01199524

N. Dershowitz and M. Okada, A rationale for conditional equational programming, Theoretical Computer Science, vol.75, issue.1-2, pp.111-138, 1990.
DOI : 10.1016/0304-3975(90)90064-O

G. Dowek and . La, Thèse d'habilit.ation, Universit, 1999.

H. Jean and . Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, volume 5 of Computer Science and Technology Series, 1986.

E. Gascard, Méthodes pour la Vérification Formelle de systèmes matériels et logiciels à architecture régulière, Thèse de doctorat, 2002.

J. Girard, Une extension de l'interprétation de Gôdel à l'analyse et son application à l'éliminat.ion des coupures dans l'analyse et la théorie des types, Second Scandinavian Logic Symposium. Nort.h-Holland, 1970.

J. Girard, Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur, 1972.

J. Girard, Y. Lafont, and P. Taylor, Proo]s and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science, 1989.

G. Huet and J. Hullot, Proofs by induction in equational theories with constructors, Preliminary version in Proceedings 21st Symposium on Foundations of Computer Science, pp.239-266, 1980.
DOI : 10.1016/0022-0000(82)90006-X

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

G. Huet, Induction principles formalized in t.he calculus of const.ruct.ions, Programming of Future Generation Computers : Proceedings of the first Franco-Japanese Symposium on Programming of Future Generation Computers, pp.205-216, 1986.

J. Jouannaud and H. Kirchner, Completion of a Set of Rules Modulo a Set of Equations, Preliminary version in Proceedings llth ACM Symposium on Principles of Programming Languages, pp.1155-1194, 1984.
DOI : 10.1137/0215084

J. Jouannaud and E. Kounalis, Automatic proofs by induction in theories without constructors, Information and Computation, vol.82, issue.1, pp.1-33, 1989.
DOI : 10.1016/0890-5401(89)90062-X

D. Kesner, Confluence properties of extensional and non-extensional ??-calculi with explicit substitutions (extended abstract), Proceedings of the 7 t h International Conference on Rewriting Techniques and Applications, pp.184-199, 1996.
DOI : 10.1007/3-540-61464-8_52

F. Karmareddine and A. Rios, A ??-calculus ?? la de Bruijn with explicit substitutions, Proceedings of the 7'h International Symposium on Programming Language Implementation and Logic Programming, pp.45-62, 1995.
DOI : 10.1007/BFb0026813

F. Karmareddine and A. Rios, Generalized ??-reduction and explicit substitutions, Proceedings of the 8 th International Symposium on Programming Language Implementation and Logic Programming, pp.378-392, 1996.
DOI : 10.1007/3-540-61756-6_98

J. Krivine, Lambda calculus, types and models, 1993.
URL : https://hal.archives-ouvertes.fr/cel-00574575

P. Lescanne, From Àa-ta À v a journey through calculi of explicit substitutions, Proceedings of the 21" Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.60-69, 1994.

P. Melliès, Typed ??-calculi with explicit substitutions may not terminate, Int. Conf. on Typed Lambda Calculus and Applications, pp.328-334, 1995.
DOI : 10.1007/BFb0014062

A. Middledorp, A sufficient condition for the termination of the direct sum of term rewrite systems, Proceedings of the 4'h annual IEEE Symposium on Logic in Computer Science (LICSS9), pp.396-401, 1989.

D. R. Musser, On proving inductive properties of abstract data types, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '80, pp.154-162, 1980.
DOI : 10.1145/567446.567461

Q. Nguyen, Calcul de réécriture et automatisation du raisonnement dans les assistants de preuve, Thèse de doctorat, 2002.

E. Ohlebusch, A simple proof of sufficient conditions for the termination of the disjoint union of term rewriting systems, Bulletin of the European Association for Theoretical Computer Science, vol.50, pp.223-228, 1993.

H. Poincaré, La science et l'hypothèse, Flammarion, 1902.

G. Peterson, M. E. Sticke, and !. , Complete Sets of Reductions for Some Equational Theories, Journal of the ACM, vol.28, issue.2, pp.233-264, 1981.
DOI : 10.1145/322248.322251

U. S. Reddy, Term rewriting induction, Proceedings lOth International Conference on Automated Deduction, pp.162-177, 1990.
DOI : 10.1007/3-540-52885-7_86

M. Rusinowitch, On termination of the direct sum of term-rewriting systems, Information Processing Letters, vol.26, issue.2, pp.65-70, 1987.
DOI : 10.1016/0020-0190(87)90039-1

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

Y. Toyama, On the Church-Rosser property for the direct sum of term rewriting systems, Journal of the ACM, vol.34, issue.1, pp.128-143, 1987.
DOI : 10.1145/7531.7534

X. Urbain, Approche incrémentale des preuves automatiques de terminaison, Thèse de doctorat

P. Viry, Rewriting modulo a rewrite system, 1995.

P. Viry, Adventures in sequent calculus modulo equations, Electronic Notes in Theoretical Computer Science, vol.15
DOI : 10.1016/S1571-0661(05)82550-2

H. Kirchner, Preface, Proceedings of the znd International Workshop on Rewriting Logic and its Applications, pp.367-378, 1998.
DOI : 10.1016/S1571-0661(05)80022-2

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 : https://doi.org/10.1016/s0304-3975(01)00366-8

W. Wechler, Universel Algebra for Computer Scientists, EATCS Monographs on Theoretical Computer Science, vol.25, 1992.