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