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