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