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