YES Problem: f(f(x)) -> f(g(f(x),x)) f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y h(x,x) -> g(x,0()) Proof: DP Processor: DPs: f#(f(x)) -> g#(f(x),x) f#(f(x)) -> f#(g(f(x),x)) f#(f(x)) -> h#(f(x),f(x)) f#(f(x)) -> f#(h(f(x),f(x))) h#(x,x) -> g#(x,0()) TRS: f(f(x)) -> f(g(f(x),x)) f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y h(x,x) -> g(x,0()) TDG Processor: DPs: f#(f(x)) -> g#(f(x),x) f#(f(x)) -> f#(g(f(x),x)) f#(f(x)) -> h#(f(x),f(x)) f#(f(x)) -> f#(h(f(x),f(x))) h#(x,x) -> g#(x,0()) TRS: f(f(x)) -> f(g(f(x),x)) f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y h(x,x) -> g(x,0()) graph: f#(f(x)) -> h#(f(x),f(x)) -> h#(x,x) -> g#(x,0()) f#(f(x)) -> f#(h(f(x),f(x))) -> f#(f(x)) -> f#(h(f(x),f(x))) f#(f(x)) -> f#(h(f(x),f(x))) -> f#(f(x)) -> h#(f(x),f(x)) f#(f(x)) -> f#(h(f(x),f(x))) -> f#(f(x)) -> f#(g(f(x),x)) f#(f(x)) -> f#(h(f(x),f(x))) -> f#(f(x)) -> g#(f(x),x) f#(f(x)) -> f#(g(f(x),x)) -> f#(f(x)) -> f#(h(f(x),f(x))) f#(f(x)) -> f#(g(f(x),x)) -> f#(f(x)) -> h#(f(x),f(x)) f#(f(x)) -> f#(g(f(x),x)) -> f#(f(x)) -> f#(g(f(x),x)) f#(f(x)) -> f#(g(f(x),x)) -> f#(f(x)) -> g#(f(x),x) SCC Processor: #sccs: 1 #rules: 2 #arcs: 9/25 DPs: f#(f(x)) -> f#(h(f(x),f(x))) f#(f(x)) -> f#(g(f(x),x)) TRS: f(f(x)) -> f(g(f(x),x)) f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y h(x,x) -> g(x,0()) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0) = x0 + -16, [0] = 0, [h](x0, x1) = -7x0 + -2x1 + 0, [g](x0, x1) = -2x0 + x1 + -16, [f](x0) = x0 + 1 orientation: f#(f(x)) = x + 1 >= -2x + 0 = f#(h(f(x),f(x))) f#(f(x)) = x + 1 >= x + -1 = f#(g(f(x),x)) f(f(x)) = x + 1 >= x + 1 = f(g(f(x),x)) f(f(x)) = x + 1 >= -2x + 1 = f(h(f(x),f(x))) g(x,y) = -2x + y + -16 >= y = y h(x,x) = -2x + 0 >= -2x + 0 = g(x,0()) problem: DPs: f#(f(x)) -> f#(g(f(x),x)) TRS: f(f(x)) -> f(g(f(x),x)) f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y h(x,x) -> g(x,0()) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0) = 1x0 + -6, [0] = 0, [h](x0, x1) = x0 + -1x1 + 1, [g](x0, x1) = -9x0 + 1x1, [f](x0) = 2x0 + 1 orientation: f#(f(x)) = 3x + 2 >= 2x + -6 = f#(g(f(x),x)) f(f(x)) = 4x + 3 >= 3x + 1 = f(g(f(x),x)) f(f(x)) = 4x + 3 >= 4x + 3 = f(h(f(x),f(x))) g(x,y) = -9x + 1y >= y = y h(x,x) = x + 1 >= -9x + 1 = g(x,0()) problem: DPs: TRS: f(f(x)) -> f(g(f(x),x)) f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y h(x,x) -> g(x,0()) Qed