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 = MiniSMT} + Details: Signatures used: ---------------- append :: [A(8) x A(3)] -(9)-> A(0) cons :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(0) x A(8)] -(8)-> A(8) cons :: [A(0) x A(2)] -(2)-> A(2) false :: [] -(0)-> A(10) hd :: [A(0)] -(8)-> A(0) ifappend :: [A(0) x A(3) x A(8)] -(8)-> A(0) is_empty :: [A(2)] -(13)-> A(0) nil :: [] -(0)-> A(8) nil :: [] -(0)-> A(2) tl :: [A(0)] -(8)-> 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(0) x A(1)] -(1)-> A(1) false_A :: [] -(0)-> A(1) nil_A :: [] -(0)-> A(1) true_A :: [] -(1)-> 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))