WORST_CASE(?,O(n^1)) * Step 1: Sum WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(0()) -> s(0()) f(s(x)) -> s(s(g(x))) g(0()) -> 0() g(s(x)) -> f(x) - Signature: {f/1,g/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {0,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(0()) -> s(0()) f(s(x)) -> s(s(g(x))) g(0()) -> 0() g(s(x)) -> f(x) - Signature: {f/1,g/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {0,s} + 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(s) = {1} Following symbols are considered usable: {f,g} TcT has computed the following interpretation: p(0) = 0 p(f) = 3 + 5*x1 p(g) = 2 + 5*x1 p(s) = 2 + x1 Following rules are strictly oriented: f(0()) = 3 > 2 = s(0()) f(s(x)) = 13 + 5*x > 6 + 5*x = s(s(g(x))) g(0()) = 2 > 0 = 0() g(s(x)) = 12 + 5*x > 3 + 5*x = f(x) Following rules are (at-least) weakly oriented: * Step 3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: f(0()) -> s(0()) f(s(x)) -> s(s(g(x))) g(0()) -> 0() g(s(x)) -> f(x) - Signature: {f/1,g/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {0,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))