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