WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: sum(0()) -> 0() sum(s(x)) -> +(sum(x),s(x)) sum1(0()) -> 0() sum1(s(x)) -> s(+(sum1(x),+(x,x))) - Signature: {sum/1,sum1/1} / {+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sum,sum1} 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: sum(0()) -> 0() sum(s(x)) -> +(sum(x),s(x)) sum1(0()) -> 0() sum1(s(x)) -> s(+(sum1(x),+(x,x))) - Signature: {sum/1,sum1/1} / {+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sum,sum1} and constructors {+,0,s} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: sum(x){x -> s(x)} = sum(s(x)) ->^+ +(sum(x),s(x)) = C[sum(x) = sum(x){}] ** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: sum(0()) -> 0() sum(s(x)) -> +(sum(x),s(x)) sum1(0()) -> 0() sum1(s(x)) -> s(+(sum1(x),+(x,x))) - Signature: {sum/1,sum1/1} / {+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sum,sum1} 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(+) = {1}, uargs(s) = {1} Following symbols are considered usable: {sum,sum1} TcT has computed the following interpretation: p(+) = x1 p(0) = 3 p(s) = x1 p(sum) = 5 + 4*x1 p(sum1) = 1 + 4*x1 Following rules are strictly oriented: sum(0()) = 17 > 3 = 0() sum1(0()) = 13 > 3 = 0() Following rules are (at-least) weakly oriented: sum(s(x)) = 5 + 4*x >= 5 + 4*x = +(sum(x),s(x)) sum1(s(x)) = 1 + 4*x >= 1 + 4*x = s(+(sum1(x),+(x,x))) ** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: sum(s(x)) -> +(sum(x),s(x)) sum1(s(x)) -> s(+(sum1(x),+(x,x))) - Weak TRS: sum(0()) -> 0() sum1(0()) -> 0() - Signature: {sum/1,sum1/1} / {+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sum,sum1} 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(+) = {1}, uargs(s) = {1} Following symbols are considered usable: {sum,sum1} TcT has computed the following interpretation: p(+) = 8 + x1 p(0) = 4 p(s) = 8 + x1 p(sum) = 2*x1 p(sum1) = 15 + 2*x1 Following rules are strictly oriented: sum(s(x)) = 16 + 2*x > 8 + 2*x = +(sum(x),s(x)) Following rules are (at-least) weakly oriented: sum(0()) = 8 >= 4 = 0() sum1(0()) = 23 >= 4 = 0() sum1(s(x)) = 31 + 2*x >= 31 + 2*x = s(+(sum1(x),+(x,x))) ** Step 1.b:3: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: sum1(s(x)) -> s(+(sum1(x),+(x,x))) - Weak TRS: sum(0()) -> 0() sum(s(x)) -> +(sum(x),s(x)) sum1(0()) -> 0() - Signature: {sum/1,sum1/1} / {+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sum,sum1} 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(+) = {1}, uargs(s) = {1} Following symbols are considered usable: {sum,sum1} TcT has computed the following interpretation: p(+) = 4 + x1 p(0) = 8 p(s) = 8 + x1 p(sum) = 2*x1 p(sum1) = 2*x1 Following rules are strictly oriented: sum1(s(x)) = 16 + 2*x > 12 + 2*x = s(+(sum1(x),+(x,x))) Following rules are (at-least) weakly oriented: sum(0()) = 16 >= 8 = 0() sum(s(x)) = 16 + 2*x >= 4 + 2*x = +(sum(x),s(x)) sum1(0()) = 16 >= 8 = 0() ** Step 1.b:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: sum(0()) -> 0() sum(s(x)) -> +(sum(x),s(x)) sum1(0()) -> 0() sum1(s(x)) -> s(+(sum1(x),+(x,x))) - Signature: {sum/1,sum1/1} / {+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sum,sum1} 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))