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: 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))))))) b#(b(x1)) -> a#(x1) b#(b(x1)) -> b#(a(x1)) b#(b(x1)) -> a#(b(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))))))) a(a(a(x1))) -> a(a(x1)) b(b(x1)) -> a(b(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))))))) b#(b(x1)) -> a#(x1) b#(b(x1)) -> b#(a(x1)) b#(b(x1)) -> a#(b(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))))))) a(a(a(x1))) -> a(a(x1)) b(b(x1)) -> a(b(a(x1))) graph: b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) -> b#(b(x1)) -> a#(b(a(x1))) b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) -> b#(b(x1)) -> b#(a(x1)) b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) -> b#(b(x1)) -> a#(x1) 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))) b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) -> a#(b(a(x1))) b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) -> a#(x1) b#(b(x1)) -> b#(a(x1)) -> b#(a(a(a(b(x1))))) -> a#(a(a(b(a(a(a(x1))))))) b#(b(x1)) -> b#(a(x1)) -> b#(a(a(a(b(x1))))) -> a#(a(b(a(a(a(x1)))))) b#(b(x1)) -> b#(a(x1)) -> b#(a(a(a(b(x1))))) -> a#(b(a(a(a(x1))))) b#(b(x1)) -> b#(a(x1)) -> b#(a(a(a(b(x1))))) -> b#(a(a(a(x1)))) b#(b(x1)) -> b#(a(x1)) -> b#(a(a(a(b(x1))))) -> a#(a(a(x1))) b#(b(x1)) -> b#(a(x1)) -> b#(a(a(a(b(x1))))) -> a#(a(x1)) b#(b(x1)) -> b#(a(x1)) -> b#(a(a(a(b(x1))))) -> a#(x1) b#(b(x1)) -> a#(b(a(x1))) -> a#(a(a(b(b(x1))))) -> b#(b(b(x1))) b#(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#(b(x1)) -> a#(b(a(x1))) a#(a(a(b(b(x1))))) -> b#(b(b(x1))) -> b#(b(x1)) -> b#(a(x1)) a#(a(a(b(b(x1))))) -> b#(b(b(x1))) -> b#(b(x1)) -> a#(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) = 4x0 + 1, [a#](x0) = x0 + 14, [a](x0) = 2x0 + 11, [b](x0) = 6x0 + 15 orientation: a#(a(a(b(b(x1))))) = 16x1 + 25 >= 16x1 + 25 = b#(b(b(x1))) b#(a(a(a(b(x1))))) = 16x1 + 25 >= x1 + 14 = a#(x1) b#(a(a(a(b(x1))))) = 16x1 + 25 >= 2x1 + 14 = a#(a(x1)) b#(a(a(a(b(x1))))) = 16x1 + 25 >= 4x1 + 14 = a#(a(a(x1))) b#(a(a(a(b(x1))))) = 16x1 + 25 >= 10x1 + 19 = b#(a(a(a(x1)))) b#(a(a(a(b(x1))))) = 16x1 + 25 >= 12x1 + 21 = a#(b(a(a(a(x1))))) b#(a(a(a(b(x1))))) = 16x1 + 25 >= 14x1 + 23 = a#(a(b(a(a(a(x1)))))) b#(a(a(a(b(x1))))) = 16x1 + 25 >= 16x1 + 25 = a#(a(a(b(a(a(a(x1))))))) b#(b(x1)) = 10x1 + 19 >= x1 + 14 = a#(x1) b#(b(x1)) = 10x1 + 19 >= 6x1 + 15 = b#(a(x1)) b#(b(x1)) = 10x1 + 19 >= 8x1 + 17 = a#(b(a(x1))) a(a(a(b(b(x1))))) = 18x1 + 27 >= 18x1 + 27 = b(b(b(x1))) b(a(a(a(b(x1))))) = 18x1 + 27 >= 18x1 + 27 = a(a(a(b(a(a(a(x1))))))) a(a(a(x1))) = 6x1 + 15 >= 4x1 + 13 = a(a(x1)) b(b(x1)) = 12x1 + 21 >= 10x1 + 19 = a(b(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))))))) a(a(a(x1))) -> a(a(x1)) b(b(x1)) -> a(b(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))))))) a(a(a(x1))) -> a(a(x1)) b(b(x1)) -> a(b(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 -& 1 0 ]x0 + [0], [a#](x0) = [0 0 -& 0 ]x0 + [0], [0 -& 0 0 ] [0] [-& -& 0 -&] [0] [a](x0) = [-& -& -& 0 ]x0 + [0] [0 -& 0 0 ] [0], [0 -& 0 0 ] [0] [0 -& 1 0 ] [1] [b](x0) = [-& -& 0 -&]x0 + [0] [-& 0 -& -&] [0] orientation: a#(a(a(b(b(x1))))) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 + [1] = b#(b(b(x1))) b#(a(a(a(b(x1))))) = [1 1 1 1]x1 + [1] >= [0 -& 0 0 ]x1 + [0] = a#(a(a(b(a(a(a(x1))))))) [0 0 1 0] [1] [0 0 1 0 ] [1] [0 0 1 0] [1] [0 0 1 0 ] [1] a(a(a(b(b(x1))))) = [0 0 1 0]x1 + [1] >= [-& -& 0 -&]x1 + [0] = b(b(b(x1))) [0 0 1 0] [1] [0 0 1 0 ] [1] [0 0 0 0] [0] [0 -& 0 0 ] [0] [1 1 1 1] [1] [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] [0 -& 0 0 ] [0] [0 -& 0 0 ] [0] [0 -& 0 0 ] [0] [-& -& -& 0 ] [0] a(a(a(x1))) = [0 -& 0 0 ]x1 + [0] >= [0 -& 0 0 ]x1 + [0] = a(a(x1)) [0 -& 0 0 ] [0] [0 -& 0 0 ] [0] [0 0 0 0 ] [0] [0 -& 0 0 ] [0] [0 0 1 0 ] [1] [-& -& -& 0 ] [0] b(b(x1)) = [-& -& 0 -&]x1 + [0] >= [-& -& 0 -&]x1 + [0] = a(b(a(x1))) [0 -& 1 0 ] [1] [0 -& 0 0 ] [0] problem: DPs: a#(a(a(b(b(x1))))) -> b#(b(b(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))))))) a(a(a(x1))) -> a(a(x1)) b(b(x1)) -> a(b(a(x1))) EDG Processor: DPs: a#(a(a(b(b(x1))))) -> b#(b(b(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))))))) a(a(a(x1))) -> a(a(x1)) b(b(x1)) -> a(b(a(x1))) graph: Qed