WORST_CASE(?,O(n^1)) * Step 1: Ara 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: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT} + Details: Signatures used: ---------------- Cons :: [A(0) x A(2)] -(2)-> A(2) Cons :: [A(0) x A(0)] -(0)-> A(0) Cons :: [A(0) x A(4)] -(4)-> A(4) False :: [] -(0)-> A(0) False :: [] -(0)-> A(1) Nil :: [] -(0)-> A(2) Nil :: [] -(0)-> A(0) Nil :: [] -(0)-> A(4) Nil :: [] -(0)-> A(6) Nil :: [] -(0)-> A(1) Nil :: [] -(0)-> A(5) True :: [] -(0)-> A(0) dec :: [A(2)] -(0)-> A(6) goal :: [A(4)] -(6)-> A(0) isNilNil :: [A(0)] -(7)-> A(0) nestdec :: [A(4)] -(4)-> A(0) number17 :: [A(0)] -(7)-> A(0) Cost-free Signatures used: -------------------------- Cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) Nil :: [] -(0)-> A_cf(0) dec :: [A_cf(0)] -(0)-> A_cf(0) nestdec :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- Cons_A :: [A(0) x A(1)] -(1)-> A(1) False_A :: [] -(0)-> A(1) Nil_A :: [] -(0)-> A(1) True_A :: [] -(0)-> A(1) * Step 2: Open MAYBE - 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} Following problems could not be solved: - 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} WORST_CASE(?,O(n^1))