WORST_CASE(?,O(n^1)) * Step 1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: comp_f_g#1(comp_f_g(x7,x9),walk_xs_3(x8),x12) -> comp_f_g#1(x7,x9,Cons(x8,x12)) comp_f_g#1(walk_xs(),walk_xs_3(x8),x12) -> Cons(x8,x12) main(Cons(x4,x5)) -> comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil()) main(Nil()) -> Nil() walk#1(Cons(x4,x3)) -> comp_f_g(walk#1(x3),walk_xs_3(x4)) walk#1(Nil()) -> walk_xs() - Signature: {comp_f_g#1/3,main/1,walk#1/1} / {Cons/2,Nil/0,comp_f_g/2,walk_xs/0,walk_xs_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {comp_f_g#1,main,walk#1} and constructors {Cons,Nil ,comp_f_g,walk_xs,walk_xs_3} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3} + Details: Signatures used: ---------------- Cons :: [A(9) x A(9)] -(9)-> A(9) Cons :: [A(0) x A(0)] -(0)-> A(0) Nil :: [] -(0)-> A(9) Nil :: [] -(0)-> A(7) comp_f_g :: [A(4) x A(4)] -(4)-> A(4) comp_f_g#1 :: [A(4) x A(2) x A(0)] -(10)-> A(0) main :: [A(9)] -(15)-> A(0) walk#1 :: [A(9)] -(3)-> A(4) walk_xs :: [] -(0)-> A(4) walk_xs :: [] -(0)-> A(10) walk_xs_3 :: [A(2)] -(0)-> A(2) walk_xs_3 :: [A(3)] -(0)-> A(3) walk_xs_3 :: [A(8)] -(0)-> A(8) Cost-free Signatures used: -------------------------- Cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) Nil :: [] -(0)-> A_cf(0) comp_f_g :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) comp_f_g#1 :: [A_cf(0) x A_cf(0) x A_cf(0)] -(0)-> A_cf(0) walk#1 :: [A_cf(0)] -(0)-> A_cf(0) walk_xs :: [] -(0)-> A_cf(0) walk_xs_3 :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- Cons_A :: [A(1) x A(1)] -(1)-> A(1) Nil_A :: [] -(0)-> A(1) comp_f_g_A :: [A(0) x A(0)] -(1)-> A(1) walk_xs_3_A :: [A(0)] -(0)-> A(1) walk_xs_A :: [] -(0)-> A(1) * Step 2: Open MAYBE - Strict TRS: comp_f_g#1(comp_f_g(x7,x9),walk_xs_3(x8),x12) -> comp_f_g#1(x7,x9,Cons(x8,x12)) comp_f_g#1(walk_xs(),walk_xs_3(x8),x12) -> Cons(x8,x12) main(Cons(x4,x5)) -> comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil()) main(Nil()) -> Nil() walk#1(Cons(x4,x3)) -> comp_f_g(walk#1(x3),walk_xs_3(x4)) walk#1(Nil()) -> walk_xs() - Signature: {comp_f_g#1/3,main/1,walk#1/1} / {Cons/2,Nil/0,comp_f_g/2,walk_xs/0,walk_xs_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {comp_f_g#1,main,walk#1} and constructors {Cons,Nil ,comp_f_g,walk_xs,walk_xs_3} Following problems could not be solved: - Strict TRS: comp_f_g#1(comp_f_g(x7,x9),walk_xs_3(x8),x12) -> comp_f_g#1(x7,x9,Cons(x8,x12)) comp_f_g#1(walk_xs(),walk_xs_3(x8),x12) -> Cons(x8,x12) main(Cons(x4,x5)) -> comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil()) main(Nil()) -> Nil() walk#1(Cons(x4,x3)) -> comp_f_g(walk#1(x3),walk_xs_3(x4)) walk#1(Nil()) -> walk_xs() - Signature: {comp_f_g#1/3,main/1,walk#1/1} / {Cons/2,Nil/0,comp_f_g/2,walk_xs/0,walk_xs_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {comp_f_g#1,main,walk#1} and constructors {Cons,Nil ,comp_f_g,walk_xs,walk_xs_3} WORST_CASE(?,O(n^1))