YES Problem: a(l(x1)) -> l(a(x1)) r(a(a(x1))) -> a(a(r(x1))) b(l(x1)) -> b(a(r(x1))) r(b(x1)) -> l(b(x1)) Proof: String Reversal Processor: l(a(x1)) -> a(l(x1)) a(a(r(x1))) -> r(a(a(x1))) l(b(x1)) -> r(a(b(x1))) b(r(x1)) -> b(l(x1)) Matrix Interpretation Processor: dim=3 interpretation: [1 1 0] [0] [b](x0) = [0 0 0]x0 + [0] [1 0 0] [1], [1 0 1] [0] [r](x0) = [0 0 0]x0 + [1] [0 0 0] [0], [1 0 0] [a](x0) = [0 0 1]x0 [0 1 0] , [1 0 0] [l](x0) = [0 0 1]x0 [0 1 0] orientation: l(a(x1)) = x1 >= x1 = a(l(x1)) [1 0 1] [0] [1 0 1] [0] a(a(r(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = r(a(a(x1))) [0 0 0] [0] [0 0 0] [0] [1 1 0] [0] [1 1 0] [0] l(b(x1)) = [1 0 0]x1 + [1] >= [0 0 0]x1 + [1] = r(a(b(x1))) [0 0 0] [0] [0 0 0] [0] [1 0 1] [1] [1 0 1] [0] b(r(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(l(x1)) [1 0 1] [1] [1 0 0] [1] problem: l(a(x1)) -> a(l(x1)) a(a(r(x1))) -> r(a(a(x1))) l(b(x1)) -> r(a(b(x1))) Arctic Interpretation Processor: dimension: 2 interpretation: [0 1] [b](x0) = [0 2]x0, [1 1] [r](x0) = [0 0]x0, [0 0 ] [a](x0) = [-& 0 ]x0, [0 2] [l](x0) = [0 2]x0 orientation: [0 2] [0 2] l(a(x1)) = [0 2]x1 >= [0 2]x1 = a(l(x1)) [1 1] [1 1] a(a(r(x1))) = [0 0]x1 >= [0 0]x1 = r(a(a(x1))) [2 4] [1 3] l(b(x1)) = [2 4]x1 >= [0 2]x1 = r(a(b(x1))) problem: l(a(x1)) -> a(l(x1)) a(a(r(x1))) -> r(a(a(x1))) KBO Processor: weight function: w0 = 1 w(r) = w(a) = w(l) = 1 precedence: l > a > r problem: Qed