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