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