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