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