WORST_CASE(?,O(n^1)) * Step 1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: a__eq(X,Y) -> false() a__eq(X1,X2) -> eq(X1,X2) a__eq(0(),0()) -> true() a__eq(s(X),s(Y)) -> a__eq(X,Y) a__inf(X) -> cons(X,inf(s(X))) a__inf(X) -> inf(X) a__length(X) -> length(X) a__length(cons(X,L)) -> s(length(L)) a__length(nil()) -> 0() a__take(X1,X2) -> take(X1,X2) a__take(0(),X) -> nil() a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L)) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(X1,X2) mark(eq(X1,X2)) -> a__eq(X1,X2) mark(false()) -> false() mark(inf(X)) -> a__inf(mark(X)) mark(length(X)) -> a__length(mark(X)) mark(nil()) -> nil() mark(s(X)) -> s(X) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(true()) -> true() - Signature: {a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1} / {0/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__eq,a__inf,a__length,a__take,mark} and constructors {0 ,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(1) 0 :: [] -(0)-> A(5) 0 :: [] -(0)-> A(0) 0 :: [] -(0)-> A(15) 0 :: [] -(0)-> A(7) a__eq :: [A(1) x A(5)] -(8)-> A(0) a__inf :: [A(0)] -(4)-> A(0) a__length :: [A(0)] -(9)-> A(0) a__take :: [A(0) x A(0)] -(6)-> A(0) cons :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(0) x A(15)] -(15)-> A(15) eq :: [A(15) x A(15)] -(15)-> A(15) eq :: [A(0) x A(0)] -(0)-> A(0) false :: [] -(0)-> A(15) false :: [] -(0)-> A(7) inf :: [A(15)] -(15)-> A(15) inf :: [A(0)] -(0)-> A(0) length :: [A(15)] -(15)-> A(15) length :: [A(0)] -(0)-> A(0) mark :: [A(15)] -(8)-> A(0) nil :: [] -(0)-> A(0) nil :: [] -(0)-> A(15) nil :: [] -(0)-> A(7) s :: [A(1)] -(1)-> A(1) s :: [A(5)] -(5)-> A(5) s :: [A(0)] -(0)-> A(0) s :: [A(15)] -(15)-> A(15) take :: [A(15) x A(15)] -(15)-> A(15) take :: [A(0) x A(0)] -(0)-> A(0) true :: [] -(0)-> A(15) true :: [] -(0)-> A(7) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) a__eq :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) a__inf :: [A_cf(0)] -(0)-> A_cf(0) a__length :: [A_cf(0)] -(0)-> A_cf(0) a__take :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) eq :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) false :: [] -(0)-> A_cf(0) inf :: [A_cf(0)] -(0)-> A_cf(0) length :: [A_cf(0)] -(0)-> A_cf(0) mark :: [A_cf(0)] -(0)-> A_cf(0) nil :: [] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) take :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) true :: [] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(1)-> A(1) eq_A :: [A(1) x A(1)] -(1)-> A(1) false_A :: [] -(0)-> A(1) inf_A :: [A(1)] -(1)-> A(1) length_A :: [A(1)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) s_A :: [A(1)] -(1)-> A(1) take_A :: [A(1) x A(1)] -(1)-> A(1) true_A :: [] -(0)-> A(1) * Step 2: Open MAYBE - Strict TRS: a__eq(X,Y) -> false() a__eq(X1,X2) -> eq(X1,X2) a__eq(0(),0()) -> true() a__eq(s(X),s(Y)) -> a__eq(X,Y) a__inf(X) -> cons(X,inf(s(X))) a__inf(X) -> inf(X) a__length(X) -> length(X) a__length(cons(X,L)) -> s(length(L)) a__length(nil()) -> 0() a__take(X1,X2) -> take(X1,X2) a__take(0(),X) -> nil() a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L)) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(X1,X2) mark(eq(X1,X2)) -> a__eq(X1,X2) mark(false()) -> false() mark(inf(X)) -> a__inf(mark(X)) mark(length(X)) -> a__length(mark(X)) mark(nil()) -> nil() mark(s(X)) -> s(X) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(true()) -> true() - Signature: {a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1} / {0/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__eq,a__inf,a__length,a__take,mark} and constructors {0 ,cons,eq,false,inf,length,nil,s,take,true} Following problems could not be solved: - Strict TRS: a__eq(X,Y) -> false() a__eq(X1,X2) -> eq(X1,X2) a__eq(0(),0()) -> true() a__eq(s(X),s(Y)) -> a__eq(X,Y) a__inf(X) -> cons(X,inf(s(X))) a__inf(X) -> inf(X) a__length(X) -> length(X) a__length(cons(X,L)) -> s(length(L)) a__length(nil()) -> 0() a__take(X1,X2) -> take(X1,X2) a__take(0(),X) -> nil() a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L)) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(X1,X2) mark(eq(X1,X2)) -> a__eq(X1,X2) mark(false()) -> false() mark(inf(X)) -> a__inf(mark(X)) mark(length(X)) -> a__length(mark(X)) mark(nil()) -> nil() mark(s(X)) -> s(X) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(true()) -> true() - Signature: {a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1} / {0/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__eq,a__inf,a__length,a__take,mark} and constructors {0 ,cons,eq,false,inf,length,nil,s,take,true} WORST_CASE(?,O(n^1))