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 usable rules: a(a(a(b(b(x1))))) -> b(b(b(x1))) b(a(a(a(b(x1))))) -> a(a(a(b(a(a(a(x1))))))) interpretation: [b#](x0) = 4x0 + 0, [a#](x0) = 2x0 + 0, [a](x0) = 1x0 + 0, [b](x0) = 3x0 + 3 orientation: a#(a(a(b(b(x1))))) = 10x1 + 10 >= 10x1 + 10 = b#(b(b(x1))) b#(a(a(a(b(x1))))) = 10x1 + 10 >= 2x1 + 0 = a#(x1) b#(a(a(a(b(x1))))) = 10x1 + 10 >= 3x1 + 2 = a#(a(x1)) b#(a(a(a(b(x1))))) = 10x1 + 10 >= 4x1 + 3 = a#(a(a(x1))) b#(a(a(a(b(x1))))) = 10x1 + 10 >= 7x1 + 6 = b#(a(a(a(x1)))) b#(a(a(a(b(x1))))) = 10x1 + 10 >= 8x1 + 7 = a#(b(a(a(a(x1))))) b#(a(a(a(b(x1))))) = 10x1 + 10 >= 9x1 + 8 = a#(a(b(a(a(a(x1)))))) b#(a(a(a(b(x1))))) = 10x1 + 10 >= 10x1 + 9 = a#(a(a(b(a(a(a(x1))))))) a(a(a(b(b(x1))))) = 9x1 + 9 >= 9x1 + 9 = b(b(b(x1))) b(a(a(a(b(x1))))) = 9x1 + 9 >= 9x1 + 8 = 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))))))) Restore Modifier: 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 usable rules: a(a(a(b(b(x1))))) -> b(b(b(x1))) b(a(a(a(b(x1))))) -> a(a(a(b(a(a(a(x1))))))) interpretation: [b#](x0) = [1 -& 0 -&]x0 + [0], [a#](x0) = [0 0 0 -&]x0 + [0], [-& -& 0 0 ] [0] [-& -& -& 0 ] [0] [a](x0) = [-& 0 -& 0 ]x0 + [0] [-& 0 -& 0 ] [0], [0 -& -& 0 ] [-&] [-& 0 0 0 ] [0 ] [b](x0) = [1 0 0 1 ]x0 + [1 ] [-& -& -& 0 ] [-&] orientation: a#(a(a(b(b(x1))))) = [1 0 0 1]x1 + [1] >= [1 0 0 1]x1 + [1] = b#(b(b(x1))) b#(a(a(a(b(x1))))) = [-& 1 1 1 ]x1 + [1] >= [-& 0 -& 0 ]x1 + [0] = a#(a(a(b(a(a(a(x1))))))) [1 0 0 1] [1] [0 -& -& 0 ] [-&] [1 0 0 1] [1] [1 0 0 1 ] [1 ] a(a(a(b(b(x1))))) = [1 0 0 1]x1 + [1] >= [1 0 0 1 ]x1 + [1 ] = b(b(b(x1))) [1 0 0 1] [1] [-& -& -& 0 ] [-&] [-& 0 0 0 ] [0] [-& 0 -& 0 ] [0] [-& 0 0 0 ] [0] [-& 0 -& 0 ] [0] b(a(a(a(b(x1))))) = [-& 1 1 1 ]x1 + [1] >= [-& 0 -& 0 ]x1 + [0] = a(a(a(b(a(a(a(x1))))))) [-& 0 0 0 ] [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))))))) Restore Modifier: 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))))))) 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))))))) graph: Qed