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