WORST_CASE(?,O(n^1)) * Step 1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: fold(a,xs) -> Cons(foldl(a,xs),Cons(foldr(a,xs),Nil())) foldl(a,Nil()) -> a foldl(x,Cons(S(0()),xs)) -> foldl(S(x),xs) foldl(S(0()),Cons(x,xs)) -> foldl(S(x),xs) foldr(a,Cons(x,xs)) -> op(x,foldr(a,xs)) foldr(a,Nil()) -> a notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() op(x,S(0())) -> S(x) op(S(0()),y) -> S(y) - Signature: {fold/2,foldl/2,foldr/2,notEmpty/1,op/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {fold,foldl,foldr,notEmpty,op} and constructors {0,Cons ,False,Nil,S,True} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(0) Cons :: [A(2) x A(2)] -(2)-> A(2) Cons :: [A(13) x A(13)] -(13)-> A(13) Cons :: [A(7) x A(7)] -(7)-> A(7) Cons :: [A(0) x A(0)] -(0)-> A(0) False :: [] -(0)-> A(14) Nil :: [] -(0)-> A(2) Nil :: [] -(0)-> A(13) Nil :: [] -(0)-> A(7) Nil :: [] -(0)-> A(5) S :: [A(0)] -(2)-> A(2) S :: [A(0)] -(1)-> A(1) S :: [A(0)] -(11)-> A(11) S :: [A(0)] -(12)-> A(12) S :: [A(0)] -(13)-> A(13) True :: [] -(0)-> A(14) fold :: [A(15) x A(15)] -(15)-> A(0) foldl :: [A(1) x A(2)] -(8)-> A(0) foldr :: [A(13) x A(13)] -(3)-> A(11) notEmpty :: [A(7)] -(9)-> A(0) op :: [A(12) x A(11)] -(3)-> A(12) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) Cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) Nil :: [] -(0)-> A_cf(0) S :: [A_cf(0)] -(0)-> A_cf(0) foldl :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) foldr :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) op :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) Cons_A :: [A(1) x A(1)] -(1)-> A(1) False_A :: [] -(0)-> A(1) Nil_A :: [] -(0)-> A(1) S_A :: [A(0)] -(1)-> A(1) True_A :: [] -(0)-> A(1) * Step 2: Open MAYBE - Strict TRS: fold(a,xs) -> Cons(foldl(a,xs),Cons(foldr(a,xs),Nil())) foldl(a,Nil()) -> a foldl(x,Cons(S(0()),xs)) -> foldl(S(x),xs) foldl(S(0()),Cons(x,xs)) -> foldl(S(x),xs) foldr(a,Cons(x,xs)) -> op(x,foldr(a,xs)) foldr(a,Nil()) -> a notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() op(x,S(0())) -> S(x) op(S(0()),y) -> S(y) - Signature: {fold/2,foldl/2,foldr/2,notEmpty/1,op/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {fold,foldl,foldr,notEmpty,op} and constructors {0,Cons ,False,Nil,S,True} Following problems could not be solved: - Strict TRS: fold(a,xs) -> Cons(foldl(a,xs),Cons(foldr(a,xs),Nil())) foldl(a,Nil()) -> a foldl(x,Cons(S(0()),xs)) -> foldl(S(x),xs) foldl(S(0()),Cons(x,xs)) -> foldl(S(x),xs) foldr(a,Cons(x,xs)) -> op(x,foldr(a,xs)) foldr(a,Nil()) -> a notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() op(x,S(0())) -> S(x) op(S(0()),y) -> S(y) - Signature: {fold/2,foldl/2,foldr/2,notEmpty/1,op/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {fold,foldl,foldr,notEmpty,op} and constructors {0,Cons ,False,Nil,S,True} WORST_CASE(?,O(n^1))