Many functional programs and higher order term rewrite systems contain, besides higher order rules, also a significant first order part. We discuss how an automatic termination prover can split a rewrite system into a first order and a higher order part. The results are applicable to all common styles of higher order rewriting with simple types, although some dependency pair approach is needed to use them. © 2011 Springer-Verlag.
Bibliographical noteProceedings title: Proc. 8th Symposium on Frontiers of Combining Systems - FroCoS'11
Editors: C. Tinelli, V. Sofronie-Stokkermans