YES(?,O(n^1)) Problem: f(a(),f(b(),f(a(),x))) -> f(a(),f(b(),f(b(),f(a(),x)))) f(b(),f(b(),f(b(),x))) -> f(b(),f(b(),x)) Proof: Complexity Transformation Processor: strict: f(a(),f(b(),f(a(),x))) -> f(a(),f(b(),f(b(),f(a(),x)))) f(b(),f(b(),f(b(),x))) -> f(b(),f(b(),x)) weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [f](x0, x1) = x0 + x1, [b] = 1, [a] = 0 orientation: f(a(),f(b(),f(a(),x))) = x + 1 >= x + 2 = f(a(),f(b(),f(b(),f(a(),x)))) f(b(),f(b(),f(b(),x))) = x + 3 >= x + 2 = f(b(),f(b(),x)) problem: strict: f(a(),f(b(),f(a(),x))) -> f(a(),f(b(),f(b(),f(a(),x)))) weak: f(b(),f(b(),f(b(),x))) -> f(b(),f(b(),x)) Bounds Processor: bound: 1 enrichment: match automaton: final states: {4} transitions: f1(12,11) -> 13* f1(12,13) -> 13,14 f1(10,4) -> 11* f1(10,14) -> 11,4 f1(12,4) -> 13* a1() -> 10* b1() -> 12* f0(4,4) -> 4* a0() -> 4* b0() -> 4* problem: strict: weak: f(a(),f(b(),f(a(),x))) -> f(a(),f(b(),f(b(),f(a(),x)))) f(b(),f(b(),f(b(),x))) -> f(b(),f(b(),x)) Qed