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