Total Termination of Term Rewriting is Undecidable

Usually termination of term rewriting systems (TRSʹs) is proved by means of a monotonic well-founded order. If this order is total on ground terms, the TRS is called totally terminating. In this paper we prove that total termination is an undecidable property of finite term rewriting systems. The proof is given by means of Postʹs Correspondence Problem.