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