WORST_CASE(?,O(n^2)) * Step 1: Sum WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: fac(0()) -> s(0()) fac(s(x)) -> times(s(x),fac(p(s(x)))) p(s(x)) -> x - Signature: {fac/1,p/1} / {0/0,s/1,times/2} - Obligation: innermost runtime complexity wrt. defined symbols {fac,p} and constructors {0,s,times} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: fac(0()) -> s(0()) fac(s(x)) -> times(s(x),fac(p(s(x)))) p(s(x)) -> x - Signature: {fac/1,p/1} / {0/0,s/1,times/2} - Obligation: innermost runtime complexity wrt. defined symbols {fac,p} and constructors {0,s,times} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(fac) = {1}, uargs(times) = {2} Following symbols are considered usable: {fac,p} TcT has computed the following interpretation: p(0) = 4 p(fac) = 4*x1 p(p) = x1 p(s) = x1 p(times) = x2 Following rules are strictly oriented: fac(0()) = 16 > 4 = s(0()) Following rules are (at-least) weakly oriented: fac(s(x)) = 4*x >= 4*x = times(s(x),fac(p(s(x)))) p(s(x)) = x >= x = x * Step 3: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: fac(s(x)) -> times(s(x),fac(p(s(x)))) p(s(x)) -> x - Weak TRS: fac(0()) -> s(0()) - Signature: {fac/1,p/1} / {0/0,s/1,times/2} - Obligation: innermost runtime complexity wrt. defined symbols {fac,p} and constructors {0,s,times} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(fac) = {1}, uargs(times) = {2} Following symbols are considered usable: {fac,p} TcT has computed the following interpretation: p(0) = 3 p(fac) = 4*x1 p(p) = x1 p(s) = 2 + x1 p(times) = x2 Following rules are strictly oriented: p(s(x)) = 2 + x > x = x Following rules are (at-least) weakly oriented: fac(0()) = 12 >= 5 = s(0()) fac(s(x)) = 8 + 4*x >= 8 + 4*x = times(s(x),fac(p(s(x)))) * Step 4: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: fac(s(x)) -> times(s(x),fac(p(s(x)))) - Weak TRS: fac(0()) -> s(0()) p(s(x)) -> x - Signature: {fac/1,p/1} / {0/0,s/1,times/2} - Obligation: innermost runtime complexity wrt. defined symbols {fac,p} and constructors {0,s,times} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 5, araRuleShifting = Nothing} + Details: Signatures used: ---------------- 0 :: [] -(0)-> "A"(2, 2) 0 :: [] -(0)-> "A"(0, 0) fac :: ["A"(2, 2)] -(0)-> "A"(0, 0) p :: ["A"(0, 2)] -(0)-> "A"(2, 2) s :: ["A"(4, 2)] -(2)-> "A"(2, 2) s :: ["A"(2, 2)] -(0)-> "A"(0, 2) s :: ["A"(1, 0)] -(1)-> "A"(1, 0) s :: ["A"(0, 0)] -(0)-> "A"(0, 0) times :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- WORST_CASE(?,O(n^2))