?. F. , U. , X. , and W. }. {n}, s acc ) mul {@(F, n), U, X, W }, which reduces to 9. lim(F ) ? {n},s acc @(F, n) which succeeds since O = T S O, F is accessible in lim(F ) and s ? {n} n by case Case 1a. Our remaining goal 10. s ? {n} {@(F, n), ) which yields goals 8 and 12 by Case 1b 8. {lim(F ) } decomposes into three goals trivially solved by Case 1e, that is 11. s ? {n} {U, X, W }, and one additional goal 12. s ? {n} @(F, n) which yields two goals by Case 1c 13. s ? {n} F , which succeeds by Case 1f, and 14. s ? {n} n which succeeds by Case 1a, thus ending the computation

T. Arts and J. Giesl, Termination of term rewriting using dependency pairs, Theoretical Computer Science, vol.236, issue.1-2, pp.133-178, 2000.
DOI : 10.1016/S0304-3975(99)00207-8

F. Barbanera, Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved, Proceedings of the 2nd International Workshop on Conditional and Typed Rewriting Systems, 1990.
DOI : 10.1007/3-540-54317-1_96

F. Barbanera and M. Fernández, Combining first and higher order rewrite systems with type assignment systems, Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications, 1993.
DOI : 10.1007/BFb0037098

F. Barbanera and M. Fernández, Modularity of termination and confluence in combinations of rewrite systems with ????, Proceedings of the 20th International Colloquium on Automata , Languages and Programming, 1993.
DOI : 10.1007/3-540-56939-1_110

F. Barbanera, M. Fernández, and H. Geuvers, Modularity of strong normalization and confluence in the algebraic-??-cube, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, 1994.
DOI : 10.1109/LICS.1994.316049

G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu, Type-based termination of recursive definitions, Mathematical Structures in Computer Science, vol.14, issue.1, pp.97-141, 2004.
DOI : 10.1017/S0960129503004122

A. M. Ben-amram, N. D. Jones, and C. S. Lee, The size-change principle for program termination, Proceedings of the 28th ACM Symposium on Principles of Programming Languages, 2001.

F. Blanqui, Definitions by rewriting in the Calculus of Constructions (extended abstract), Proceedings of the 16th IEEE Symposium on Logic in Computer Science, 2001.

F. Blanqui, Higher-order dependency pairs, Proceedings of the 8th International Workshop on Termination, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00084821

F. Blanqui, Termination and Confluence of Higher-Order Rewrite Systems, Proceedings of the 11th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 1833, 2000.
DOI : 10.1007/10721975_4
URL : https://hal.archives-ouvertes.fr/inria-00105556

F. Blanqui, A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems, Proceedings of the 15th International Conference on Rewriting Techniques and Applications, 2004.
DOI : 10.1007/978-3-540-25979-4_2
URL : https://hal.archives-ouvertes.fr/inria-00100254

F. Blanqui, Definitions by rewriting in the Calculus of Constructions, Mathematical Structures in Computer Science, vol.15, issue.1, pp.37-92, 2005.
DOI : 10.1017/S0960129504004426
URL : https://hal.archives-ouvertes.fr/inria-00105568

F. Blanqui, Inductive Types in the Calculus of Algebraic Constructions, Fundamenta Informaticae, vol.65, issue.12, pp.61-86, 2005.
DOI : 10.1007/3-540-44904-3_4
URL : https://hal.archives-ouvertes.fr/inria-00105617

F. Blanqui, Computability closure: Ten years later In Rewriting, Computation and Proof ? Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol.4600, 2007.

F. Blanqui, J. Jouannaud, and M. Okada, Inductive-data-type systems, Theoretical Computer Science, vol.272, issue.1-2, pp.41-68, 2002.
DOI : 10.1016/S0304-3975(00)00347-9
URL : https://hal.archives-ouvertes.fr/inria-00105578

F. Blanqui, J. Jouannaud, and A. Rubio, Higher-Order Termination: From Kruskal to Computability, Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2006.
DOI : 10.1007/11916277_1
URL : https://hal.archives-ouvertes.fr/inria-00091308

F. Blanqui, J. Jouannaud, and A. Rubio, HORPO with Computability Closure: A Reconstruction, Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2007.
DOI : 10.1007/978-3-540-75560-9_12
URL : https://hal.archives-ouvertes.fr/inria-00168304

N. Bohr and N. Jones, Termination Analysis of the untyped lambda-calculus, Proceedings of the 15th International Conference on Rewriting Techniques and Applications, pp.1-23, 2004.

C. Borralleras, Ordering-based methods for proving termination automatically, 2003.

C. Borralleras and A. Rubio, A Monotonic Higher-Order Semantic Path Ordering, Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2001.
DOI : 10.1007/3-540-45653-8_37

C. Borralleras and A. Rubio, Orderings and Constraints: Theory and Practice of Proving Termination, Rewriting, Computation and Proof ? Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, 2007.
DOI : 10.1007/978-3-540-73147-4_2

V. Breazu-tannen, Combining algebra and higher-order types, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, 1988.
DOI : 10.1109/LICS.1988.5103

V. Breazu-tannen and J. Gallier, Polymorphic rewriting conserves algebraic strong normalization, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, 1989.
DOI : 10.1016/0304-3975(91)90037-3
URL : http://doi.org/10.1016/0304-3975(91)90037-3

W. N. Chin and S. C. Khoo, Calculating sized types, Higher-Order and Symbolic Computation, vol.14, issue.2/3, pp.261-300, 2001.
DOI : 10.1023/A:1012996816178
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.4005

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.404.4058

D. Dougherty, Adding algebraic rewriting to the untyped lambda calculus, Information and Computation, vol.101, issue.2, pp.251-267, 1992.
DOI : 10.1016/0890-5401(92)90064-M

J. Giesl, S. Swiderski, P. Schneider-kamp, and R. Thiemann, Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages, Proceedings of the 17th International Conference on Rewriting Techniques and Applications, 2006.
DOI : 10.1007/11805618_23

J. Giesl, R. Thiemann, and P. Schneider-kamp, The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs, Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2004.
DOI : 10.1007/978-3-540-32275-7_21

J. Goubault-larrecq, Well-Founded Recursive Relations, Proceedings of the 15th International Conference on Computer Science Logic, 2001.
DOI : 10.1007/3-540-44802-0_34

J. Hughes, L. Pareto, and A. Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, 1996.
DOI : 10.1145/237721.240882

C. B. Jay, The pattern calculus, ACM Transactions on Programming Languages and Systems, vol.26, issue.6, pp.911-937, 2004.
DOI : 10.1145/1034774.1034775

J. Jouannaud and M. Okada, A computation model for executable higher-order algebraic specification languages, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, 1991.
DOI : 10.1109/LICS.1991.151659

J. Jouannaud and M. Okada, Abstract data type systems, Theoretical Computer Science, vol.173, issue.2, pp.349-391, 1997.
DOI : 10.1016/S0304-3975(96)00161-2
URL : http://doi.org/10.1016/s0304-3975(96)00161-2

J. Jouannaud and A. Rubio, Higher-Order Orderings for Normal Rewriting, Proceedings of the 17th International Conference on Rewriting Techniques and Applications, 2006.
DOI : 10.1007/11805618_29

J. Jouannaud and A. Rubio, The higher-order recursive path ordering, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), 1999.
DOI : 10.1109/LICS.1999.782635

J. Jouannaud and A. Rubio, Rewrite orderings for higher-order terms in ??-long ??-normal form and the recursive path ordering, Theoretical Computer Science, vol.208, issue.1-2, pp.33-58, 1998.
DOI : 10.1016/S0304-3975(98)00078-4

J. Jouannaud and A. Rubio, Higher-order recursive path orderings " ` a la carte, 2001.

J. Jouannaud and A. Rubio, Polymorphic higher-order recursive path orderings, Journal of the ACM, vol.54, issue.1, pp.1-48, 2007.
DOI : 10.1145/1206035.1206037

S. Kamin and J. Lévy, Two generalizations of the Recursive Path Ordering, 1980.

M. S. Krishnamoorthy and P. Narendran, On recursive path ordering, Theoretical Computer Science, vol.40, issue.2-3, pp.323-328, 1985.
DOI : 10.1016/0304-3975(85)90175-6

C. Loria-saenz and J. Steinbach, Termination of combined (rewrite and ??-calculus) systems, Proceedings of the 3rd International Workshop on Conditional and Typed Rewriting Systems, 1992.
DOI : 10.1007/3-540-56393-8_10

M. Okada, Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system, Proceedings of the 1989 International Symposium on Symbolic and Algebraic Computation

M. Sakai and K. Kusakari, On dependency pair method for proving termination of higherorder rewrite systems, IEICE Transactions on Information and Systems, issue.3, pp.88-583, 2005.

M. Sakai, Y. Watanabe, and T. Sakabe, An extension of dependency pair method for proving termination of higher-order rewrite systems, IEICE Transactions on Information and Systems, issue.8, pp.84-1025, 2001.

J. Van, Termination proofs for higher-order rewrite systems, Proceedings of the 1st International Workshop on Higher-Order Algebra, Logic and Term Rewriting, 1993.

J. Van, Termination of higher-order rewrite systems, 1996.

J. Van-de-pol and H. Schwichtenberg, Strict functionals for termination proofs, Proceedings of the 2nd International Conference on Typed Lambda Calculi and Applications, 1995.
DOI : 10.1007/BFb0014064

D. Walukiewicz-chrzaszcz, Termination of rewriting in the Calculus of Constructions, Journal of Functional Programming, vol.13, issue.02, pp.339-414, 2003.
DOI : 10.1017/S0956796802004641

H. Xi, Dependent types for program termination verification, Higher-Order and Symbolic Computation, vol.15, issue.1, pp.91-131, 2002.
DOI : 10.1023/A:1019916231463