YES Problem: a(a(a(b(b(x1))))) -> b(b(b(x1))) b(a(a(a(b(x1))))) -> a(a(a(b(a(a(a(x1))))))) a(a(a(x1))) -> a(a(x1)) b(b(x1)) -> a(b(a(x1))) Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [a](x0) = 2x0, [b](x0) = 6x0 orientation: a(a(a(b(b(x1))))) = 18x1 >= 18x1 = b(b(b(x1))) b(a(a(a(b(x1))))) = 18x1 >= 18x1 = a(a(a(b(a(a(a(x1))))))) a(a(a(x1))) = 6x1 >= 4x1 = a(a(x1)) b(b(x1)) = 12x1 >= 10x1 = a(b(a(x1))) problem: a(a(a(b(b(x1))))) -> b(b(b(x1))) b(a(a(a(b(x1))))) -> a(a(a(b(a(a(a(x1))))))) DP Processor: DPs: a#(a(a(b(b(x1))))) -> b#(b(b(x1))) b#(a(a(a(b(x1))))) -> a#(x1) b#(a(a(a(b(x1))))) -> a#(a(x1)) b#(a(a(a(b(x1))))) -> a#(a(a(x1))) b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) b#(a(a(a(b(x1))))) -> a#(b(a(a(a(x1))))) b#(a(a(a(b(x1))))) -> a#(a(b(a(a(a(x1)))))) b#(a(a(a(b(x1))))) -> a#(a(a(b(a(a(a(x1))))))) TRS: a(a(a(b(b(x1))))) -> b(b(b(x1))) b(a(a(a(b(x1))))) -> a(a(a(b(a(a(a(x1))))))) TDG Processor: DPs: a#(a(a(b(b(x1))))) -> b#(b(b(x1))) b#(a(a(a(b(x1))))) -> a#(x1) b#(a(a(a(b(x1))))) -> a#(a(x1)) b#(a(a(a(b(x1))))) -> a#(a(a(x1))) b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) b#(a(a(a(b(x1))))) -> a#(b(a(a(a(x1))))) b#(a(a(a(b(x1))))) -> a#(a(b(a(a(a(x1)))))) b#(a(a(a(b(x1))))) -> a#(a(a(b(a(a(a(x1))))))) TRS: a(a(a(b(b(x1))))) -> b(b(b(x1))) b(a(a(a(b(x1))))) -> a(a(a(b(a(a(a(x1))))))) graph: b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) -> b#(a(a(a(b(x1))))) -> a#(a(a(b(a(a(a(x1))))))) b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) -> b#(a(a(a(b(x1))))) -> a#(a(b(a(a(a(x1)))))) b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) -> b#(a(a(a(b(x1))))) -> a#(b(a(a(a(x1))))) b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) -> b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) -> b#(a(a(a(b(x1))))) -> a#(a(a(x1))) b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) -> b#(a(a(a(b(x1))))) -> a#(a(x1)) b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) -> b#(a(a(a(b(x1))))) -> a#(x1) b#(a(a(a(b(x1))))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(a(b(b(x1))))) -> b#(b(b(x1))) b#(a(a(a(b(x1))))) -> a#(a(a(x1))) -> a#(a(a(b(b(x1))))) -> b#(b(b(x1))) b#(a(a(a(b(x1))))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(a(b(b(x1))))) -> b#(b(b(x1))) b#(a(a(a(b(x1))))) -> a#(a(x1)) -> a#(a(a(b(b(x1))))) -> b#(b(b(x1))) b#(a(a(a(b(x1))))) -> a#(b(a(a(a(x1))))) -> a#(a(a(b(b(x1))))) -> b#(b(b(x1))) b#(a(a(a(b(x1))))) -> a#(x1) -> a#(a(a(b(b(x1))))) -> b#(b(b(x1))) a#(a(a(b(b(x1))))) -> b#(b(b(x1))) -> b#(a(a(a(b(x1))))) -> a#(a(a(b(a(a(a(x1))))))) a#(a(a(b(b(x1))))) -> b#(b(b(x1))) -> b#(a(a(a(b(x1))))) -> a#(a(b(a(a(a(x1)))))) a#(a(a(b(b(x1))))) -> b#(b(b(x1))) -> b#(a(a(a(b(x1))))) -> a#(b(a(a(a(x1))))) a#(a(a(b(b(x1))))) -> b#(b(b(x1))) -> b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) a#(a(a(b(b(x1))))) -> b#(b(b(x1))) -> b#(a(a(a(b(x1))))) -> a#(a(a(x1))) a#(a(a(b(b(x1))))) -> b#(b(b(x1))) -> b#(a(a(a(b(x1))))) -> a#(a(x1)) a#(a(a(b(b(x1))))) -> b#(b(b(x1))) -> b#(a(a(a(b(x1))))) -> a#(x1) Arctic Interpretation Processor: dimension: 1 interpretation: [b#](x0) = 2x0 + 0, [a#](x0) = x0 + 0, [a](x0) = 1x0, [b](x0) = 3x0 + 1 orientation: a#(a(a(b(b(x1))))) = 8x1 + 6 >= 8x1 + 6 = b#(b(b(x1))) b#(a(a(a(b(x1))))) = 8x1 + 6 >= x1 + 0 = a#(x1) b#(a(a(a(b(x1))))) = 8x1 + 6 >= 1x1 + 0 = a#(a(x1)) b#(a(a(a(b(x1))))) = 8x1 + 6 >= 2x1 + 0 = a#(a(a(x1))) b#(a(a(a(b(x1))))) = 8x1 + 6 >= 5x1 + 0 = b#(a(a(a(x1)))) b#(a(a(a(b(x1))))) = 8x1 + 6 >= 6x1 + 1 = a#(b(a(a(a(x1))))) b#(a(a(a(b(x1))))) = 8x1 + 6 >= 7x1 + 2 = a#(a(b(a(a(a(x1)))))) b#(a(a(a(b(x1))))) = 8x1 + 6 >= 8x1 + 3 = a#(a(a(b(a(a(a(x1))))))) a(a(a(b(b(x1))))) = 9x1 + 7 >= 9x1 + 7 = b(b(b(x1))) b(a(a(a(b(x1))))) = 9x1 + 7 >= 9x1 + 4 = a(a(a(b(a(a(a(x1))))))) problem: DPs: a#(a(a(b(b(x1))))) -> b#(b(b(x1))) b#(a(a(a(b(x1))))) -> a#(a(a(b(a(a(a(x1))))))) TRS: a(a(a(b(b(x1))))) -> b(b(b(x1))) b(a(a(a(b(x1))))) -> a(a(a(b(a(a(a(x1))))))) EDG Processor: DPs: a#(a(a(b(b(x1))))) -> b#(b(b(x1))) b#(a(a(a(b(x1))))) -> a#(a(a(b(a(a(a(x1))))))) TRS: a(a(a(b(b(x1))))) -> b(b(b(x1))) b(a(a(a(b(x1))))) -> a(a(a(b(a(a(a(x1))))))) graph: b#(a(a(a(b(x1))))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(a(b(b(x1))))) -> b#(b(b(x1))) a#(a(a(b(b(x1))))) -> b#(b(b(x1))) -> b#(a(a(a(b(x1))))) -> a#(a(a(b(a(a(a(x1))))))) Arctic Interpretation Processor: dimension: 4 interpretation: [b#](x0) = [-& 0 -& -&]x0 + [0], [a#](x0) = [0 0 0 0]x0 + [0], [-& 0 0 -&] [0] [-& -& -& 0 ] [0] [a](x0) = [-& 0 0 0 ]x0 + [0] [-& 0 0 -&] [0], [0 1 0 0 ] [1 ] [-& 0 -& -&] [0 ] [b](x0) = [0 0 -& 0 ]x0 + [-&] [-& 0 0 0 ] [0 ] orientation: a#(a(a(b(b(x1))))) = [0 1 0 0]x1 + [1] >= [-& 0 -& -&]x1 + [0] = b#(b(b(x1))) b#(a(a(a(b(x1))))) = [0 0 0 0]x1 + [0] >= [-& 0 0 0 ]x1 + [0] = a#(a(a(b(a(a(a(x1))))))) [0 1 0 0] [1] [0 1 0 0 ] [1] [0 1 0 0] [1] [-& 0 -& -&] [0] a(a(a(b(b(x1))))) = [0 1 0 0]x1 + [1] >= [0 1 0 0 ]x1 + [1] = b(b(b(x1))) [0 1 0 0] [1] [0 1 0 0 ] [1] [1 1 1 1] [1] [-& 0 0 0 ] [0] [0 0 0 0] [0] [-& 0 0 0 ] [0] b(a(a(a(b(x1))))) = [0 0 0 0]x1 + [0] >= [-& 0 0 0 ]x1 + [0] = a(a(a(b(a(a(a(x1))))))) [0 0 0 0] [0] [-& 0 0 0 ] [0] problem: DPs: b#(a(a(a(b(x1))))) -> a#(a(a(b(a(a(a(x1))))))) TRS: a(a(a(b(b(x1))))) -> b(b(b(x1))) b(a(a(a(b(x1))))) -> a(a(a(b(a(a(a(x1))))))) EDG Processor: DPs: b#(a(a(a(b(x1))))) -> a#(a(a(b(a(a(a(x1))))))) TRS: a(a(a(b(b(x1))))) -> b(b(b(x1))) b(a(a(a(b(x1))))) -> a(a(a(b(a(a(a(x1))))))) graph: Qed