WORST_CASE(?,O(n^1)) * Step 1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: append(l1,l2) -> ifappend(l1,l2,l1) hd(cons(x,l)) -> x ifappend(l1,l2,cons(x,l)) -> cons(x,append(l,l2)) ifappend(l1,l2,nil()) -> l2 is_empty(cons(x,l)) -> false() is_empty(nil()) -> true() tl(cons(x,l)) -> l - Signature: {append/2,hd/1,ifappend/3,is_empty/1,tl/1} / {cons/2,false/0,nil/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,hd,ifappend,is_empty,tl} and constructors {cons ,false,nil,true} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3} + Details: Signatures used: ---------------- append :: [A(15) x A(15)] -(9)-> A(3) cons :: [A(5) x A(5)] -(5)-> A(5) cons :: [A(15) x A(15)] -(15)-> A(15) cons :: [A(9) x A(9)] -(9)-> A(9) cons :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(3) x A(3)] -(3)-> A(3) false :: [] -(0)-> A(0) hd :: [A(5)] -(6)-> A(0) ifappend :: [A(0) x A(15) x A(15)] -(8)-> A(3) is_empty :: [A(9)] -(10)-> A(0) nil :: [] -(0)-> A(15) nil :: [] -(0)-> A(9) tl :: [A(0)] -(15)-> A(0) true :: [] -(0)-> A(0) Cost-free Signatures used: -------------------------- append :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) ifappend :: [A_cf(0) x A_cf(0) x A_cf(0)] -(0)-> A_cf(0) nil :: [] -(0)-> A_cf(0) 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) * Step 2: Open MAYBE - Strict TRS: append(l1,l2) -> ifappend(l1,l2,l1) hd(cons(x,l)) -> x ifappend(l1,l2,cons(x,l)) -> cons(x,append(l,l2)) ifappend(l1,l2,nil()) -> l2 is_empty(cons(x,l)) -> false() is_empty(nil()) -> true() tl(cons(x,l)) -> l - Signature: {append/2,hd/1,ifappend/3,is_empty/1,tl/1} / {cons/2,false/0,nil/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,hd,ifappend,is_empty,tl} and constructors {cons ,false,nil,true} Following problems could not be solved: - Strict TRS: append(l1,l2) -> ifappend(l1,l2,l1) hd(cons(x,l)) -> x ifappend(l1,l2,cons(x,l)) -> cons(x,append(l,l2)) ifappend(l1,l2,nil()) -> l2 is_empty(cons(x,l)) -> false() is_empty(nil()) -> true() tl(cons(x,l)) -> l - Signature: {append/2,hd/1,ifappend/3,is_empty/1,tl/1} / {cons/2,false/0,nil/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,hd,ifappend,is_empty,tl} and constructors {cons ,false,nil,true} WORST_CASE(?,O(n^1))