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