TORPAcyc is applied to the string rewriting system a a -> b b b b b b b b -> a a a interpretation of a: 8 interpretation of b: 5 remove rule 2 continue with: a a -> b b b interpretation of a: 8 interpretation of b: 0 remove rule 1 termination has been proved