WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: bits(0()) -> 0() bits(s(x)) -> s(bits(half(s(x)))) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) - Signature: {bits/1,half/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {bits,half} 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: bits(0()) -> 0() bits(s(x)) -> s(bits(half(s(x)))) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) - Signature: {bits/1,half/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {bits,half} 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: bits(0()) -> 0() bits(s(x)) -> s(bits(half(s(x)))) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) - Signature: {bits/1,half/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {bits,half} 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(bits) = {1}, uargs(s) = {1} Following symbols are considered usable: {bits,half} TcT has computed the following interpretation: p(0) = 4 p(bits) = 4 + x1 p(half) = x1 p(s) = x1 Following rules are strictly oriented: bits(0()) = 8 > 4 = 0() Following rules are (at-least) weakly oriented: bits(s(x)) = 4 + x >= 4 + x = s(bits(half(s(x)))) half(0()) = 4 >= 4 = 0() half(s(0())) = 4 >= 4 = 0() half(s(s(x))) = x >= x = s(half(x)) ** Step 1.b:2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: bits(s(x)) -> s(bits(half(s(x)))) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) - Weak TRS: bits(0()) -> 0() - Signature: {bits/1,half/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {bits,half} and constructors {0,s} + Applied Processor: Ara {araHeuristics = Heuristics, minDegree = 1, maxDegree = 1, araTimeout = 3, araRuleShifting = Nothing} + Details: Signatures used: ---------------- 0 :: [] -(0)-> "A"(3) 0 :: [] -(0)-> "A"(5) 0 :: [] -(0)-> "A"(0) bits :: ["A"(5)] -(0)-> "A"(0) half :: ["A"(3)] -(1)-> "A"(5) s :: ["A"(5)] -(5)-> "A"(5) s :: ["A"(3)] -(3)-> "A"(3) s :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- WORST_CASE(Omega(n^1),O(n^1))