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