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