TORPAcyc is applied to the string rewriting system R E -> L E a L -> L Aa b L -> L Ab c L -> L Ac R Aa -> a R R Ab -> b R R Ac -> c R a b L -> b a a R c b L -> b b c R Normal matrix interpretation interpretation of R: / 1 2 \ \ 1 0 / interpretation of E: / 2 0 \ \ 0 0 / interpretation of L: / 1 2 \ \ 1 0 / interpretation of a: / 1 0 \ \ 0 1 / interpretation of Aa: / 1 0 \ \ 0 1 / interpretation of b: / 1 2 \ \ 0 1 / interpretation of Ab: / 1 0 \ \ 1 1 / interpretation of c: / 3 0 \ \ 0 1 / interpretation of Ac: / 1 0 \ \ 1 3 / remove rule 9 continue with: R E -> L E a L -> L Aa b L -> L Ab c L -> L Ac R Aa -> a R R Ab -> b R R Ac -> c R a b L -> b a a R Normal matrix interpretation interpretation of R: / 1 2 \ \ 0 1 / interpretation of E: / 1 0 \ \ 1 0 / interpretation of L: / 1 0 \ \ 0 1 / interpretation of a: / 1 2 \ \ 0 1 / interpretation of Aa: / 1 2 \ \ 0 1 / interpretation of b: / 1 1 \ \ 0 3 / interpretation of Ab: / 1 0 \ \ 0 3 / interpretation of c: / 1 1 \ \ 0 1 / interpretation of Ac: / 1 1 \ \ 0 1 / remove rule 1 continue with: a L -> L Aa b L -> L Ab c L -> L Ac R Aa -> a R R Ab -> b R R Ac -> c R a b L -> b a a R interpretation of R: 1 interpretation of E: 5 interpretation of L: 3 interpretation of a: 1 interpretation of Aa: 1 interpretation of b: 0 interpretation of Ab: 0 interpretation of c: 0 interpretation of Ac: 0 remove rule 7 continue with: a L -> L Aa b L -> L Ab c L -> L Ac R Aa -> a R R Ab -> b R R Ac -> c R Tropical matrix interpretation interpretation of R: / 1 - \ \ 0 - / interpretation of E: / 0 0 \ \ 0 0 / interpretation of L: / 0 0 \ \ 2 0 / interpretation of a: / 0 0 \ \ - 0 / interpretation of Aa: / 0 - \ \ 3 0 / interpretation of b: / 2 1 \ \ 1 - / interpretation of Ab: / 2 - \ \ 0 0 / interpretation of c: / 3 0 \ \ 3 0 / interpretation of Ac: / 0 - \ \ 1 0 / remove rule 2 continue with: a L -> L Aa c L -> L Ac R Aa -> a R R Ab -> b R R Ac -> c R interpretation of R: 6 interpretation of E: 0 interpretation of L: 0 interpretation of a: 4 interpretation of Aa: 4 interpretation of b: 3 interpretation of Ab: 4 interpretation of c: 3 interpretation of Ac: 3 remove rule 4 continue with: a L -> L Aa c L -> L Ac R Aa -> a R R Ac -> c R Tropical matrix interpretation interpretation of R: / 0 - \ \ 0 - / interpretation of E: / 0 0 \ \ 0 0 / interpretation of L: / 0 - \ \ - - / interpretation of a: / 2 0 \ \ - 0 / interpretation of Aa: / 1 - \ \ - - / interpretation of b: / 0 0 \ \ 0 0 / interpretation of Ab: / 0 0 \ \ 0 0 / interpretation of c: / 1 0 \ \ - 0 / interpretation of Ac: / 1 - \ \ - - / remove rule 4 continue with: a L -> L Aa c L -> L Ac R Aa -> a R interpretation of R: 10 interpretation of E: 8 interpretation of L: 3 interpretation of a: 4 interpretation of Aa: 4 interpretation of b: 0 interpretation of Ab: 0 interpretation of c: 1 interpretation of Ac: 0 remove rule 2 continue with: a L -> L Aa R Aa -> a R Tropical matrix interpretation interpretation of R: / 0 - \ \ 0 - / interpretation of E: / 0 0 \ \ 0 0 / interpretation of L: / 0 - \ \ - - / interpretation of a: / 2 0 \ \ - 0 / interpretation of Aa: / 1 - \ \ 1 0 / interpretation of b: / 0 0 \ \ 0 0 / interpretation of Ab: / 0 0 \ \ 0 0 / interpretation of c: / 0 0 \ \ 0 0 / interpretation of Ac: / 0 0 \ \ 0 0 / remove rule 1 continue with: R Aa -> a R interpretation of R: 1 interpretation of E: 0 interpretation of L: 0 interpretation of a: 0 interpretation of Aa: 1 interpretation of b: 0 interpretation of Ab: 0 interpretation of c: 0 interpretation of Ac: 0 remove rule 1 termination has been proved