YES(?,O(n^2)) Problem: g(0(),f(x,x)) -> x g(x,s(y)) -> g(f(x,y),0()) g(s(x),y) -> g(f(x,y),0()) g(f(x,y),0()) -> f(g(x,0()),g(y,0())) Proof: Complexity Transformation Processor: strict: g(0(),f(x,x)) -> x g(x,s(y)) -> g(f(x,y),0()) g(s(x),y) -> g(f(x,y),0()) g(f(x,y),0()) -> f(g(x,0()),g(y,0())) weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [s](x0) = x0, [g](x0, x1) = x0 + x1, [f](x0, x1) = x0 + x1, [0] = 1 orientation: g(0(),f(x,x)) = 2x + 1 >= x = x g(x,s(y)) = x + y >= x + y + 1 = g(f(x,y),0()) g(s(x),y) = x + y >= x + y + 1 = g(f(x,y),0()) g(f(x,y),0()) = x + y + 1 >= x + y + 2 = f(g(x,0()),g(y,0())) problem: strict: g(x,s(y)) -> g(f(x,y),0()) g(s(x),y) -> g(f(x,y),0()) g(f(x,y),0()) -> f(g(x,0()),g(y,0())) weak: g(0(),f(x,x)) -> x Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [s](x0) = x0 + 1, [g](x0, x1) = x0 + x1, [f](x0, x1) = x0 + x1, [0] = 0 orientation: g(x,s(y)) = x + y + 1 >= x + y = g(f(x,y),0()) g(s(x),y) = x + y + 1 >= x + y = g(f(x,y),0()) g(f(x,y),0()) = x + y >= x + y = f(g(x,0()),g(y,0())) g(0(),f(x,x)) = 2x >= x = x problem: strict: g(f(x,y),0()) -> f(g(x,0()),g(y,0())) weak: g(x,s(y)) -> g(f(x,y),0()) g(s(x),y) -> g(f(x,y),0()) g(0(),f(x,x)) -> x Matrix Interpretation Processor: dimension: 2 max_matrix: [1 1] [0 1] interpretation: [0] [s](x0) = x0 + [1], [1 1] [1 1] [g](x0, x1) = [0 1]x0 + [0 1]x1, [0] [f](x0, x1) = x0 + x1 + [1], [0] [0] = [0] orientation: [1 1] [1 1] [1] [1 1] [1 1] [0] g(f(x,y),0()) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = f(g(x,0()),g(y,0())) [1 1] [1 1] [1] [1 1] [1 1] [1] g(x,s(y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = g(f(x,y),0()) [1 1] [1 1] [1] [1 1] [1 1] [1] g(s(x),y) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = g(f(x,y),0()) [2 2] [1] g(0(),f(x,x)) = [0 2]x + [1] >= x = x problem: strict: weak: g(f(x,y),0()) -> f(g(x,0()),g(y,0())) g(x,s(y)) -> g(f(x,y),0()) g(s(x),y) -> g(f(x,y),0()) g(0(),f(x,x)) -> x Qed