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