R. Iosif and A. Rogalewicz, “Automata-Based Termination Proofs”, Comput. Inform., vol. 32, no. 4, pp. 739–775, Nov. 2013.