MAYBE Problem: f(c(s(x),y)) -> f(c(x,s(y))) f(c(s(x),s(y))) -> g(c(x,y)) g(c(x,s(y))) -> g(c(s(x),y)) g(c(s(x),s(y))) -> f(c(x,y)) Proof: Complexity Transformation Processor: strict: f(c(s(x),y)) -> f(c(x,s(y))) f(c(s(x),s(y))) -> g(c(x,y)) g(c(x,s(y))) -> g(c(s(x),y)) g(c(s(x),s(y))) -> f(c(x,y)) weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [g](x0) = x0 + 1, [f](x0) = x0, [c](x0, x1) = x0 + x1, [s](x0) = x0 orientation: f(c(s(x),y)) = x + y >= x + y = f(c(x,s(y))) f(c(s(x),s(y))) = x + y >= x + y + 1 = g(c(x,y)) g(c(x,s(y))) = x + y + 1 >= x + y + 1 = g(c(s(x),y)) g(c(s(x),s(y))) = x + y + 1 >= x + y = f(c(x,y)) problem: strict: f(c(s(x),y)) -> f(c(x,s(y))) f(c(s(x),s(y))) -> g(c(x,y)) g(c(x,s(y))) -> g(c(s(x),y)) weak: g(c(s(x),s(y))) -> f(c(x,y)) Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [g](x0) = x0, [f](x0) = x0, [c](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1 orientation: f(c(s(x),y)) = x + y + 2 >= x + y + 2 = f(c(x,s(y))) f(c(s(x),s(y))) = x + y + 3 >= x + y + 1 = g(c(x,y)) g(c(x,s(y))) = x + y + 2 >= x + y + 2 = g(c(s(x),y)) g(c(s(x),s(y))) = x + y + 3 >= x + y + 1 = f(c(x,y)) problem: strict: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) weak: f(c(s(x),s(y))) -> g(c(x,y)) g(c(s(x),s(y))) -> f(c(x,y)) Open