WORST_CASE(?,O(n^1)) * Step 1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: a(c(d(x))) -> c(x) u(b(d(d(x)))) -> b(x) v(a(a(x))) -> u(v(x)) v(a(c(x))) -> u(b(d(x))) v(c(x)) -> b(x) w(a(a(x))) -> u(w(x)) w(a(c(x))) -> u(b(d(x))) w(c(x)) -> b(x) - Signature: {a/1,u/1,v/1,w/1} / {b/1,c/1,d/1} - Obligation: innermost runtime complexity wrt. defined symbols {a,u,v,w} and constructors {b,c,d} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3} + Details: Signatures used: ---------------- a :: [A(7)] -(7)-> A(7) b :: [A(5)] -(5)-> A(5) b :: [A(6)] -(6)-> A(6) c :: [A(7)] -(7)-> A(7) d :: [A(7)] -(7)-> A(7) d :: [A(5)] -(5)-> A(5) u :: [A(5)] -(7)-> A(5) v :: [A(7)] -(15)-> A(5) w :: [A(7)] -(12)-> A(5) Cost-free Signatures used: -------------------------- a :: [A_cf(0)] -(0)-> A_cf(0) b :: [A_cf(0)] -(0)-> A_cf(0) c :: [A_cf(0)] -(0)-> A_cf(0) d :: [A_cf(0)] -(0)-> A_cf(0) u :: [A_cf(0)] -(0)-> A_cf(0) v :: [A_cf(0)] -(0)-> A_cf(0) w :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- b_A :: [A(1)] -(1)-> A(1) c_A :: [A(1)] -(1)-> A(1) d_A :: [A(1)] -(1)-> A(1) * Step 2: Open MAYBE - Strict TRS: a(c(d(x))) -> c(x) u(b(d(d(x)))) -> b(x) v(a(a(x))) -> u(v(x)) v(a(c(x))) -> u(b(d(x))) v(c(x)) -> b(x) w(a(a(x))) -> u(w(x)) w(a(c(x))) -> u(b(d(x))) w(c(x)) -> b(x) - Signature: {a/1,u/1,v/1,w/1} / {b/1,c/1,d/1} - Obligation: innermost runtime complexity wrt. defined symbols {a,u,v,w} and constructors {b,c,d} Following problems could not be solved: - Strict TRS: a(c(d(x))) -> c(x) u(b(d(d(x)))) -> b(x) v(a(a(x))) -> u(v(x)) v(a(c(x))) -> u(b(d(x))) v(c(x)) -> b(x) w(a(a(x))) -> u(w(x)) w(a(c(x))) -> u(b(d(x))) w(c(x)) -> b(x) - Signature: {a/1,u/1,v/1,w/1} / {b/1,c/1,d/1} - Obligation: innermost runtime complexity wrt. defined symbols {a,u,v,w} and constructors {b,c,d} WORST_CASE(?,O(n^1))