Omega-Termination is Undecidable for Totally Terminating Term Rewriting Systems

We give a complete proof of the fact that the following problem is undecidable:Given:A term rewriting system, where the termination of its rewrite relation is provable by a total reduction order on ground terms,Wanted:Does there exist a strictly monotonic interpretation in the positive integers that proves termination?