YES Problem: a(a(x1)) -> x1 a(b(b(a(x1)))) -> a(a(b(a(b(b(x1)))))) Proof: DP Processor: DPs: a#(b(b(a(x1)))) -> a#(b(b(x1))) a#(b(b(a(x1)))) -> a#(b(a(b(b(x1))))) a#(b(b(a(x1)))) -> a#(a(b(a(b(b(x1)))))) TRS: a(a(x1)) -> x1 a(b(b(a(x1)))) -> a(a(b(a(b(b(x1)))))) Arctic Interpretation Processor: dimension: 2 interpretation: [a#](x0) = [0 -&]x0 + [0], [-& 0 ] [1] [b](x0) = [0 -&]x0 + [0], [1 0 ] [2] [a](x0) = [0 -&]x0 + [0] orientation: a#(b(b(a(x1)))) = [1 0]x1 + [2] >= [0 -&]x1 + [1] = a#(b(b(x1))) a#(b(b(a(x1)))) = [1 0]x1 + [2] >= [0 -&]x1 + [1] = a#(b(a(b(b(x1))))) a#(b(b(a(x1)))) = [1 0]x1 + [2] >= [1 0]x1 + [2] = a#(a(b(a(b(b(x1)))))) [2 1] [3] a(a(x1)) = [1 0]x1 + [2] >= x1 = x1 [2 1] [3] [2 1] [3] a(b(b(a(x1)))) = [1 0]x1 + [2] >= [1 0]x1 + [2] = a(a(b(a(b(b(x1)))))) problem: DPs: a#(b(b(a(x1)))) -> a#(a(b(a(b(b(x1)))))) TRS: a(a(x1)) -> x1 a(b(b(a(x1)))) -> a(a(b(a(b(b(x1)))))) Arctic Interpretation Processor: dimension: 3 interpretation: [a#](x0) = [-& 1 0 ]x0 + [0], [-& -& 1 ] [0] [b](x0) = [0 -& 0 ]x0 + [1] [-& -& -&] [0], [0 0 0 ] [0] [a](x0) = [-& 0 0 ]x0 + [0] [-& 0 1 ] [1] orientation: a#(b(b(a(x1)))) = [-& 2 3 ]x1 + [3] >= [-& -& 2 ]x1 + [2] = a#(a(b(a(b(b(x1)))))) [0 0 1 ] [1] a(a(x1)) = [-& 0 1 ]x1 + [1] >= x1 = x1 [-& 1 2 ] [2] [-& 1 2 ] [2] [-& -& 2 ] [2] a(b(b(a(x1)))) = [-& 1 2 ]x1 + [2] >= [-& -& 1 ]x1 + [1] = a(a(b(a(b(b(x1)))))) [-& 1 2 ] [2] [-& -& 2 ] [2] problem: DPs: TRS: a(a(x1)) -> x1 a(b(b(a(x1)))) -> a(a(b(a(b(b(x1)))))) Qed