TORPAcyc is applied to the string rewriting system a b a -> b b a b -> b b b b b -> a a a Tropical matrix interpretation interpretation of a: / 0 1 \ \ 1 3 / interpretation of b: / 3 2 \ \ 2 1 / remove rule 2 continue with: a b a -> b b b -> a a a interpretation of a: 0 interpretation of b: 10 remove rule 2 continue with: a b a -> b interpretation of a: 7 interpretation of b: 10 remove rule 1 termination has been proved