Problem: f(0()) -> 0() f(s(x)) -> f(id(x)) id(0()) -> 0() id(s(x)) -> s(id(x)) Proof: Complexity Transformation Processor: strict: f(0()) -> 0() f(s(x)) -> f(id(x)) id(0()) -> 0() id(s(x)) -> s(id(x)) weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [id](x0) = x0 + 194, [s](x0) = x0 + 82, [f](x0) = x0 + 167, [0] = 116 orientation: f(0()) = 283 >= 116 = 0() f(s(x)) = x + 249 >= x + 361 = f(id(x)) id(0()) = 310 >= 116 = 0() id(s(x)) = x + 276 >= x + 276 = s(id(x)) problem: strict: f(s(x)) -> f(id(x)) id(s(x)) -> s(id(x)) weak: f(0()) -> 0() id(0()) -> 0() Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [id](x0) = x0, [s](x0) = x0 + 1, [f](x0) = x0, [0] = 40 orientation: f(s(x)) = x + 1 >= x = f(id(x)) id(s(x)) = x + 1 >= x + 1 = s(id(x)) f(0()) = 40 >= 40 = 0() id(0()) = 40 >= 40 = 0() problem: strict: id(s(x)) -> s(id(x)) weak: f(s(x)) -> f(id(x)) f(0()) -> 0() id(0()) -> 0() Matrix Interpretation Processor: dimension: 4 max_matrix: [1 1 1 1] [0 0 0 0] [0 0 0 1] [0 0 0 1] interpretation: [1 0 1 0] [1] [0 0 0 0] [0] [id](x0) = [0 0 0 1]x0 + [0] [0 0 0 1] [0], [1 1 1 1] [1] [0 0 0 0] [0] [s](x0) = [0 0 0 1]x0 + [1] [0 0 0 1] [1], [1 0 0 1] [1] [0 0 0 0] [1] [f](x0) = [0 0 0 0]x0 + [1] [0 0 0 0] [1], [0] [0] [0] = [0] [0] orientation: [1 1 1 2] [3] [1 0 1 2] [2] [0 0 0 0] [0] [0 0 0 0] [0] id(s(x)) = [0 0 0 1]x + [1] >= [0 0 0 1]x + [1] = s(id(x)) [0 0 0 1] [1] [0 0 0 1] [1] [1 1 1 2] [3] [1 0 1 1] [2] [0 0 0 0] [1] [0 0 0 0] [1] f(s(x)) = [0 0 0 0]x + [1] >= [0 0 0 0]x + [1] = f(id(x)) [0 0 0 0] [1] [0 0 0 0] [1] [1] [0] [1] [0] f(0()) = [1] >= [0] = 0() [1] [0] [1] [0] [0] [0] id(0()) = [0] >= [0] = 0() [0] [0] problem: strict: weak: id(s(x)) -> s(id(x)) f(s(x)) -> f(id(x)) f(0()) -> 0() id(0()) -> 0() Qed