WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: g(x,s(y)) -> g(f(x,y),0()) g(0(),f(x,x)) -> x g(f(x,y),0()) -> f(g(x,0()),g(y,0())) g(s(x),y) -> g(f(x,y),0()) - Signature: {g/2} / {0/0,f/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {g} and constructors {0,f,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: g(x,s(y)) -> g(f(x,y),0()) g(0(),f(x,x)) -> x g(f(x,y),0()) -> f(g(x,0()),g(y,0())) g(s(x),y) -> g(f(x,y),0()) - Signature: {g/2} / {0/0,f/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {g} and constructors {0,f,s} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: g(x,0()){x -> f(x,y)} = g(f(x,y),0()) ->^+ f(g(x,0()),g(y,0())) = C[g(x,0()) = g(x,0()){}] ** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: g(x,s(y)) -> g(f(x,y),0()) g(0(),f(x,x)) -> x g(f(x,y),0()) -> f(g(x,0()),g(y,0())) g(s(x),y) -> g(f(x,y),0()) - Signature: {g/2} / {0/0,f/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {g} and constructors {0,f,s} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(f) = {1,2} Following symbols are considered usable: {g} TcT has computed the following interpretation: p(0) = 0 p(f) = x1 + x2 p(g) = x2 p(s) = 14 Following rules are strictly oriented: g(x,s(y)) = 14 > 0 = g(f(x,y),0()) Following rules are (at-least) weakly oriented: g(0(),f(x,x)) = 2*x >= x = x g(f(x,y),0()) = 0 >= 0 = f(g(x,0()),g(y,0())) g(s(x),y) = y >= 0 = g(f(x,y),0()) ** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: g(0(),f(x,x)) -> x g(f(x,y),0()) -> f(g(x,0()),g(y,0())) g(s(x),y) -> g(f(x,y),0()) - Weak TRS: g(x,s(y)) -> g(f(x,y),0()) - Signature: {g/2} / {0/0,f/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {g} and constructors {0,f,s} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(f) = {1,2} Following symbols are considered usable: {g} TcT has computed the following interpretation: p(0) = 1 p(f) = 7 + x1 + x2 p(g) = 2*x1 + 2*x2 p(s) = 9 + x1 Following rules are strictly oriented: g(0(),f(x,x)) = 16 + 4*x > x = x g(f(x,y),0()) = 16 + 2*x + 2*y > 11 + 2*x + 2*y = f(g(x,0()),g(y,0())) g(s(x),y) = 18 + 2*x + 2*y > 16 + 2*x + 2*y = g(f(x,y),0()) Following rules are (at-least) weakly oriented: g(x,s(y)) = 18 + 2*x + 2*y >= 16 + 2*x + 2*y = g(f(x,y),0()) ** Step 1.b:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: g(x,s(y)) -> g(f(x,y),0()) g(0(),f(x,x)) -> x g(f(x,y),0()) -> f(g(x,0()),g(y,0())) g(s(x),y) -> g(f(x,y),0()) - Signature: {g/2} / {0/0,f/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {g} and constructors {0,f,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))