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