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