WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: decrease(Cons(x,xs)) -> decrease(xs) decrease(Nil()) -> number42(Nil()) goal(x) -> decrease(x) number42(x) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {decrease/1,goal/1,number42/1} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {decrease,goal,number42} and constructors {Cons,Nil} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: decrease(Cons(x,xs)) -> decrease(xs) decrease(Nil()) -> number42(Nil()) goal(x) -> decrease(x) number42(x) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {decrease/1,goal/1,number42/1} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {decrease,goal,number42} and constructors {Cons,Nil} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: decrease(y){y -> Cons(x,y)} = decrease(Cons(x,y)) ->^+ decrease(y) = C[decrease(y) = decrease(y){}] ** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: decrease(Cons(x,xs)) -> decrease(xs) decrease(Nil()) -> number42(Nil()) goal(x) -> decrease(x) number42(x) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {decrease/1,goal/1,number42/1} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {decrease,goal,number42} and constructors {Cons,Nil} + 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: none Following symbols are considered usable: {decrease,goal,number42} TcT has computed the following interpretation: p(Cons) = 0 p(Nil) = 0 p(decrease) = 2 p(goal) = 6 p(number42) = 2 Following rules are strictly oriented: goal(x) = 6 > 2 = decrease(x) number42(x) = 2 > 0 = Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) Following rules are (at-least) weakly oriented: decrease(Cons(x,xs)) = 2 >= 2 = decrease(xs) decrease(Nil()) = 2 >= 2 = number42(Nil()) ** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: decrease(Cons(x,xs)) -> decrease(xs) decrease(Nil()) -> number42(Nil()) - Weak TRS: goal(x) -> decrease(x) number42(x) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {decrease/1,goal/1,number42/1} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {decrease,goal,number42} and constructors {Cons,Nil} + 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: none Following symbols are considered usable: {decrease,goal,number42} TcT has computed the following interpretation: p(Cons) = x1 p(Nil) = 0 p(decrease) = 2 p(goal) = 5 p(number42) = x1 Following rules are strictly oriented: decrease(Nil()) = 2 > 0 = number42(Nil()) Following rules are (at-least) weakly oriented: decrease(Cons(x,xs)) = 2 >= 2 = decrease(xs) goal(x) = 5 >= 2 = decrease(x) number42(x) = x >= 0 = Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) ** Step 1.b:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: decrease(Cons(x,xs)) -> decrease(xs) - Weak TRS: decrease(Nil()) -> number42(Nil()) goal(x) -> decrease(x) number42(x) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {decrease/1,goal/1,number42/1} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {decrease,goal,number42} and constructors {Cons,Nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- Cons :: ["A"(7) x "A"(7)] -(7)-> "A"(7) Cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0) Cons :: ["A"(1) x "A"(1)] -(1)-> "A"(1) Nil :: [] -(0)-> "A"(7) Nil :: [] -(0)-> "A"(14) Nil :: [] -(0)-> "A"(12) Nil :: [] -(0)-> "A"(4) Nil :: [] -(0)-> "A"(0) Nil :: [] -(0)-> "A"(10) Nil :: [] -(0)-> "A"(8) Nil :: [] -(0)-> "A"(15) Nil :: [] -(0)-> "A"(9) decrease :: ["A"(7)] -(15)-> "A"(0) goal :: ["A"(15)] -(15)-> "A"(0) number42 :: ["A"(3)] -(15)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "Cons_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "Nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: decrease(Cons(x,xs)) -> decrease(xs) 2. Weak: WORST_CASE(Omega(n^1),O(n^1))