YES Problem: c(c(x1)) -> a(a(a(b(b(b(x1)))))) b(b(b(a(x1)))) -> b(b(b(b(b(b(b(b(x1)))))))) b(b(c(c(x1)))) -> c(c(c(a(a(a(a(x1))))))) Proof: Arctic Interpretation Processor: dimension: 2 interpretation: [0 0 ] [a](x0) = [-& -&]x0, [0 0] [b](x0) = [0 0]x0, [0 1] [c](x0) = [0 0]x0 orientation: [1 1] [0 0 ] c(c(x1)) = [0 1]x1 >= [-& -&]x1 = a(a(a(b(b(b(x1)))))) [0 0] [0 0] b(b(b(a(x1)))) = [0 0]x1 >= [0 0]x1 = b(b(b(b(b(b(b(b(x1)))))))) [1 1] [1 1] b(b(c(c(x1)))) = [1 1]x1 >= [1 1]x1 = c(c(c(a(a(a(a(x1))))))) problem: b(b(b(a(x1)))) -> b(b(b(b(b(b(b(b(x1)))))))) b(b(c(c(x1)))) -> c(c(c(a(a(a(a(x1))))))) String Reversal Processor: a(b(b(b(x1)))) -> b(b(b(b(b(b(b(b(x1)))))))) c(c(b(b(x1)))) -> a(a(a(a(c(c(c(x1))))))) Bounds Processor: bound: 2 enrichment: match automaton: final states: {4} transitions: a1(27) -> 28* a1(29) -> 30* a1(26) -> 27* a1(28) -> 29* c1(25) -> 26* c1(24) -> 25* c1(23) -> 24* b1(20) -> 21* b1(15) -> 16* b1(17) -> 18* b1(19) -> 20* b1(14) -> 15* b1(21) -> 22* b1(16) -> 17* b1(18) -> 19* a2(50) -> 51* a2(52) -> 53* a2(51) -> 52* a2(53) -> 54* a0(4) -> 4* c2(55) -> 56* c2(57) -> 58* c2(47) -> 48* c2(59) -> 60* c2(49) -> 50* c2(81) -> 82* c2(61) -> 62* c2(63) -> 64* c2(48) -> 49* b0(4) -> 4* c0(4) -> 4* 4 -> 23,14 14 -> 59* 15 -> 4,14 16 -> 81* 17 -> 63* 18 -> 57* 19 -> 55,14,23 20 -> 47,23 21 -> 61,23 22 -> 4* 30 -> 25,24,4 54 -> 60,48,49,24,4,25 56 -> 48* 58 -> 48* 60 -> 48* 62 -> 48* 64 -> 48* 82 -> 48* problem: Qed