WORST_CASE(?,O(n^1)) * Step 1: Sum WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: dec(Cons(Cons(x,xs),Nil())) -> dec(Nil()) dec(Cons(Cons(x',xs'),Cons(x,xs))) -> dec(Cons(x,xs)) dec(Cons(Nil(),Cons(x,xs))) -> dec(Cons(x,xs)) dec(Cons(Nil(),Nil())) -> Nil() goal(x) -> nestdec(x) isNilNil(Cons(Cons(x,xs),Nil())) -> False() isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) -> False() isNilNil(Cons(Nil(),Cons(x,xs))) -> False() isNilNil(Cons(Nil(),Nil())) -> True() nestdec(Cons(x,xs)) -> nestdec(dec(Cons(x,xs))) nestdec(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()))))))))))))))))) number17(n) -> 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: {dec/1,goal/1,isNilNil/1,nestdec/1,number17/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {dec,goal,isNilNil,nestdec ,number17} and constructors {Cons,False,Nil,True} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: dec(Cons(Cons(x,xs),Nil())) -> dec(Nil()) dec(Cons(Cons(x',xs'),Cons(x,xs))) -> dec(Cons(x,xs)) dec(Cons(Nil(),Cons(x,xs))) -> dec(Cons(x,xs)) dec(Cons(Nil(),Nil())) -> Nil() goal(x) -> nestdec(x) isNilNil(Cons(Cons(x,xs),Nil())) -> False() isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) -> False() isNilNil(Cons(Nil(),Cons(x,xs))) -> False() isNilNil(Cons(Nil(),Nil())) -> True() nestdec(Cons(x,xs)) -> nestdec(dec(Cons(x,xs))) nestdec(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()))))))))))))))))) number17(n) -> 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: {dec/1,goal/1,isNilNil/1,nestdec/1,number17/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {dec,goal,isNilNil,nestdec ,number17} and constructors {Cons,False,Nil,True} + 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(nestdec) = {1} Following symbols are considered usable: {dec,goal,isNilNil,nestdec,number17} TcT has computed the following interpretation: p(Cons) = 2 + x1 p(False) = 7 p(Nil) = 0 p(True) = 0 p(dec) = 0 p(goal) = 3 + 4*x1 p(isNilNil) = 7 p(nestdec) = 2 + 4*x1 p(number17) = 2 Following rules are strictly oriented: goal(x) = 3 + 4*x > 2 + 4*x = nestdec(x) isNilNil(Cons(Nil(),Nil())) = 7 > 0 = True() nestdec(Cons(x,xs)) = 10 + 4*x > 2 = nestdec(dec(Cons(x,xs))) Following rules are (at-least) weakly oriented: dec(Cons(Cons(x,xs),Nil())) = 0 >= 0 = dec(Nil()) dec(Cons(Cons(x',xs'),Cons(x,xs))) = 0 >= 0 = dec(Cons(x,xs)) dec(Cons(Nil(),Cons(x,xs))) = 0 >= 0 = dec(Cons(x,xs)) dec(Cons(Nil(),Nil())) = 0 >= 0 = Nil() isNilNil(Cons(Cons(x,xs),Nil())) = 7 >= 7 = False() isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) = 7 >= 7 = False() isNilNil(Cons(Nil(),Cons(x,xs))) = 7 >= 7 = False() nestdec(Nil()) = 2 >= 2 = 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()))))))))))))))))) number17(n) = 2 >= 2 = 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 3: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: dec(Cons(Cons(x,xs),Nil())) -> dec(Nil()) dec(Cons(Cons(x',xs'),Cons(x,xs))) -> dec(Cons(x,xs)) dec(Cons(Nil(),Cons(x,xs))) -> dec(Cons(x,xs)) dec(Cons(Nil(),Nil())) -> Nil() isNilNil(Cons(Cons(x,xs),Nil())) -> False() isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) -> False() isNilNil(Cons(Nil(),Cons(x,xs))) -> False() nestdec(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()))))))))))))))))) number17(n) -> 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()))))))))))))))))) - Weak TRS: goal(x) -> nestdec(x) isNilNil(Cons(Nil(),Nil())) -> True() nestdec(Cons(x,xs)) -> nestdec(dec(Cons(x,xs))) - Signature: {dec/1,goal/1,isNilNil/1,nestdec/1,number17/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {dec,goal,isNilNil,nestdec ,number17} and constructors {Cons,False,Nil,True} + 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(nestdec) = {1} Following symbols are considered usable: {dec,goal,isNilNil,nestdec,number17} TcT has computed the following interpretation: p(Cons) = 0 p(False) = 0 p(Nil) = 0 p(True) = 4 p(dec) = 0 p(goal) = 6 + 4*x1 p(isNilNil) = 4 p(nestdec) = 6 + 4*x1 p(number17) = x1 Following rules are strictly oriented: isNilNil(Cons(Cons(x,xs),Nil())) = 4 > 0 = False() isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) = 4 > 0 = False() isNilNil(Cons(Nil(),Cons(x,xs))) = 4 > 0 = False() nestdec(Nil()) = 6 > 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(),Nil()))))))))))))))))) Following rules are (at-least) weakly oriented: dec(Cons(Cons(x,xs),Nil())) = 0 >= 0 = dec(Nil()) dec(Cons(Cons(x',xs'),Cons(x,xs))) = 0 >= 0 = dec(Cons(x,xs)) dec(Cons(Nil(),Cons(x,xs))) = 0 >= 0 = dec(Cons(x,xs)) dec(Cons(Nil(),Nil())) = 0 >= 0 = Nil() goal(x) = 6 + 4*x >= 6 + 4*x = nestdec(x) isNilNil(Cons(Nil(),Nil())) = 4 >= 4 = True() nestdec(Cons(x,xs)) = 6 >= 6 = nestdec(dec(Cons(x,xs))) number17(n) = n >= 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(),Nil()))))))))))))))))) * Step 4: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: dec(Cons(Cons(x,xs),Nil())) -> dec(Nil()) dec(Cons(Cons(x',xs'),Cons(x,xs))) -> dec(Cons(x,xs)) dec(Cons(Nil(),Cons(x,xs))) -> dec(Cons(x,xs)) dec(Cons(Nil(),Nil())) -> Nil() number17(n) -> 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()))))))))))))))))) - Weak TRS: goal(x) -> nestdec(x) isNilNil(Cons(Cons(x,xs),Nil())) -> False() isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) -> False() isNilNil(Cons(Nil(),Cons(x,xs))) -> False() isNilNil(Cons(Nil(),Nil())) -> True() nestdec(Cons(x,xs)) -> nestdec(dec(Cons(x,xs))) nestdec(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: {dec/1,goal/1,isNilNil/1,nestdec/1,number17/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {dec,goal,isNilNil,nestdec ,number17} and constructors {Cons,False,Nil,True} + 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(nestdec) = {1} Following symbols are considered usable: {dec,goal,isNilNil,nestdec,number17} TcT has computed the following interpretation: p(Cons) = 0 p(False) = 0 p(Nil) = 0 p(True) = 0 p(dec) = 0 p(goal) = 2 + 4*x1 p(isNilNil) = 1 + x1 p(nestdec) = 2*x1 p(number17) = 3 + x1 Following rules are strictly oriented: number17(n) = 3 + n > 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(),Nil()))))))))))))))))) Following rules are (at-least) weakly oriented: dec(Cons(Cons(x,xs),Nil())) = 0 >= 0 = dec(Nil()) dec(Cons(Cons(x',xs'),Cons(x,xs))) = 0 >= 0 = dec(Cons(x,xs)) dec(Cons(Nil(),Cons(x,xs))) = 0 >= 0 = dec(Cons(x,xs)) dec(Cons(Nil(),Nil())) = 0 >= 0 = Nil() goal(x) = 2 + 4*x >= 2*x = nestdec(x) isNilNil(Cons(Cons(x,xs),Nil())) = 1 >= 0 = False() isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) = 1 >= 0 = False() isNilNil(Cons(Nil(),Cons(x,xs))) = 1 >= 0 = False() isNilNil(Cons(Nil(),Nil())) = 1 >= 0 = True() nestdec(Cons(x,xs)) = 0 >= 0 = nestdec(dec(Cons(x,xs))) nestdec(Nil()) = 0 >= 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(),Nil()))))))))))))))))) * Step 5: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: dec(Cons(Cons(x,xs),Nil())) -> dec(Nil()) dec(Cons(Cons(x',xs'),Cons(x,xs))) -> dec(Cons(x,xs)) dec(Cons(Nil(),Cons(x,xs))) -> dec(Cons(x,xs)) dec(Cons(Nil(),Nil())) -> Nil() - Weak TRS: goal(x) -> nestdec(x) isNilNil(Cons(Cons(x,xs),Nil())) -> False() isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) -> False() isNilNil(Cons(Nil(),Cons(x,xs))) -> False() isNilNil(Cons(Nil(),Nil())) -> True() nestdec(Cons(x,xs)) -> nestdec(dec(Cons(x,xs))) nestdec(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()))))))))))))))))) number17(n) -> 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: {dec/1,goal/1,isNilNil/1,nestdec/1,number17/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {dec,goal,isNilNil,nestdec ,number17} and constructors {Cons,False,Nil,True} + 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(nestdec) = {1} Following symbols are considered usable: {dec,goal,isNilNil,nestdec,number17} TcT has computed the following interpretation: p(Cons) = 4 p(False) = 0 p(Nil) = 2 p(True) = 0 p(dec) = x1 p(goal) = 4 + x1 p(isNilNil) = 0 p(nestdec) = 4 + x1 p(number17) = 4 Following rules are strictly oriented: dec(Cons(Cons(x,xs),Nil())) = 4 > 2 = dec(Nil()) dec(Cons(Nil(),Nil())) = 4 > 2 = Nil() Following rules are (at-least) weakly oriented: dec(Cons(Cons(x',xs'),Cons(x,xs))) = 4 >= 4 = dec(Cons(x,xs)) dec(Cons(Nil(),Cons(x,xs))) = 4 >= 4 = dec(Cons(x,xs)) goal(x) = 4 + x >= 4 + x = nestdec(x) isNilNil(Cons(Cons(x,xs),Nil())) = 0 >= 0 = False() isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) = 0 >= 0 = False() isNilNil(Cons(Nil(),Cons(x,xs))) = 0 >= 0 = False() isNilNil(Cons(Nil(),Nil())) = 0 >= 0 = True() nestdec(Cons(x,xs)) = 8 >= 8 = nestdec(dec(Cons(x,xs))) nestdec(Nil()) = 6 >= 4 = 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()))))))))))))))))) number17(n) = 4 >= 4 = 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 6: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: dec(Cons(Cons(x',xs'),Cons(x,xs))) -> dec(Cons(x,xs)) dec(Cons(Nil(),Cons(x,xs))) -> dec(Cons(x,xs)) - Weak TRS: dec(Cons(Cons(x,xs),Nil())) -> dec(Nil()) dec(Cons(Nil(),Nil())) -> Nil() goal(x) -> nestdec(x) isNilNil(Cons(Cons(x,xs),Nil())) -> False() isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) -> False() isNilNil(Cons(Nil(),Cons(x,xs))) -> False() isNilNil(Cons(Nil(),Nil())) -> True() nestdec(Cons(x,xs)) -> nestdec(dec(Cons(x,xs))) nestdec(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()))))))))))))))))) number17(n) -> 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: {dec/1,goal/1,isNilNil/1,nestdec/1,number17/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {dec,goal,isNilNil,nestdec ,number17} and constructors {Cons,False,Nil,True} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 5, araRuleShifting = Nothing} + Details: Signatures used: ---------------- Cons :: ["A"(1) x "A"(1)] -(1)-> "A"(1) Cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0) Cons :: ["A"(15) x "A"(15)] -(15)-> "A"(15) False :: [] -(0)-> "A"(0) Nil :: [] -(0)-> "A"(1) Nil :: [] -(0)-> "A"(0) Nil :: [] -(0)-> "A"(15) Nil :: [] -(0)-> "A"(10) Nil :: [] -(0)-> "A"(8) True :: [] -(0)-> "A"(0) dec :: ["A"(1)] -(14)-> "A"(15) goal :: ["A"(15)] -(15)-> "A"(0) isNilNil :: ["A"(0)] -(0)-> "A"(0) nestdec :: ["A"(15)] -(1)-> "A"(0) number17 :: ["A"(0)] -(14)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "Cons_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "False_A" :: [] -(0)-> "A"(1) "Nil_A" :: [] -(0)-> "A"(1) "True_A" :: [] -(0)-> "A"(1) WORST_CASE(?,O(n^1))