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