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