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