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