YES Problem: f(f(x,y,z),u,f(x,y,v)) -> f(x,y,f(z,u,v)) f(x,y,y) -> y f(x,y,g(y)) -> x f(x,x,y) -> x f(g(x),x,y) -> y Proof: DP Processor: DPs: f#(f(x,y,z),u,f(x,y,v)) -> f#(z,u,v) f#(f(x,y,z),u,f(x,y,v)) -> f#(x,y,f(z,u,v)) TRS: f(f(x,y,z),u,f(x,y,v)) -> f(x,y,f(z,u,v)) f(x,y,y) -> y f(x,y,g(y)) -> x f(x,x,y) -> x f(g(x),x,y) -> y Restore Modifier: DPs: f#(f(x,y,z),u,f(x,y,v)) -> f#(z,u,v) f#(f(x,y,z),u,f(x,y,v)) -> f#(x,y,f(z,u,v)) TRS: f(f(x,y,z),u,f(x,y,v)) -> f(x,y,f(z,u,v)) f(x,y,y) -> y f(x,y,g(y)) -> x f(x,x,y) -> x f(g(x),x,y) -> y SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 DPs: f#(f(x,y,z),u,f(x,y,v)) -> f#(z,u,v) f#(f(x,y,z),u,f(x,y,v)) -> f#(x,y,f(z,u,v)) TRS: f(f(x,y,z),u,f(x,y,v)) -> f(x,y,f(z,u,v)) f(x,y,y) -> y f(x,y,g(y)) -> x f(x,x,y) -> x f(g(x),x,y) -> y Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1, x2) = x0 + 1, [g](x0) = 0, [f](x0, x1, x2) = x0 + x2 + 1 orientation: f#(f(x,y,z),u,f(x,y,v)) = x + z + 2 >= z + 1 = f#(z,u,v) f#(f(x,y,z),u,f(x,y,v)) = x + z + 2 >= x + 1 = f#(x,y,f(z,u,v)) f(f(x,y,z),u,f(x,y,v)) = v + 2x + z + 3 >= v + x + z + 2 = f(x,y,f(z,u,v)) f(x,y,y) = x + y + 1 >= y = y f(x,y,g(y)) = x + 1 >= x = x f(x,x,y) = x + y + 1 >= x = x f(g(x),x,y) = y + 1 >= y = y problem: DPs: TRS: f(f(x,y,z),u,f(x,y,v)) -> f(x,y,f(z,u,v)) f(x,y,y) -> y f(x,y,g(y)) -> x f(x,x,y) -> x f(g(x),x,y) -> y Qed