WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: f(0(),y) -> 0() f(s(x),y) -> f(f(x,y),y) - Signature: {f/2} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f} and constructors {0,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: f(0(),y) -> 0() f(s(x),y) -> f(f(x,y),y) - Signature: {f/2} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f} and constructors {0,s} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: f(x,y){x -> s(x)} = f(s(x),y) ->^+ f(f(x,y),y) = C[f(x,y) = f(x,y){}] ** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(0(),y) -> 0() f(s(x),y) -> f(f(x,y),y) - Signature: {f/2} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f} and constructors {0,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} Following symbols are considered usable: {f} TcT has computed the following interpretation: p(0) = 1 p(f) = 1 + x1 p(s) = 7 + x1 Following rules are strictly oriented: f(0(),y) = 2 > 1 = 0() f(s(x),y) = 8 + x > 2 + x = f(f(x,y),y) Following rules are (at-least) weakly oriented: ** Step 1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: f(0(),y) -> 0() f(s(x),y) -> f(f(x,y),y) - Signature: {f/2} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f} and constructors {0,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))