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