WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: b(r(x)) -> r(b(x)) b(w(x)) -> w(b(x)) w(r(x)) -> r(w(x)) - Signature: {b/1,w/1} / {r/1} - Obligation: innermost runtime complexity wrt. defined symbols {b,w} and constructors {r} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: b(r(x)) -> r(b(x)) b(w(x)) -> w(b(x)) w(r(x)) -> r(w(x)) - Signature: {b/1,w/1} / {r/1} - Obligation: innermost runtime complexity wrt. defined symbols {b,w} and constructors {r} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: b(x){x -> r(x)} = b(r(x)) ->^+ r(b(x)) = C[b(x) = b(x){}] ** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: b(r(x)) -> r(b(x)) b(w(x)) -> w(b(x)) w(r(x)) -> r(w(x)) - Signature: {b/1,w/1} / {r/1} - Obligation: innermost runtime complexity wrt. defined symbols {b,w} and constructors {r} + 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(r) = {1}, uargs(w) = {1} Following symbols are considered usable: {b,w} TcT has computed the following interpretation: p(b) = 8 + 5*x1 p(r) = x1 p(w) = 4 + 2*x1 Following rules are strictly oriented: b(w(x)) = 28 + 10*x > 20 + 10*x = w(b(x)) Following rules are (at-least) weakly oriented: b(r(x)) = 8 + 5*x >= 8 + 5*x = r(b(x)) w(r(x)) = 4 + 2*x >= 4 + 2*x = r(w(x)) ** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: b(r(x)) -> r(b(x)) w(r(x)) -> r(w(x)) - Weak TRS: b(w(x)) -> w(b(x)) - Signature: {b/1,w/1} / {r/1} - Obligation: innermost runtime complexity wrt. defined symbols {b,w} and constructors {r} + 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(r) = {1}, uargs(w) = {1} Following symbols are considered usable: {b,w} TcT has computed the following interpretation: p(b) = 8 + 5*x1 p(r) = 3 + x1 p(w) = 2 + 2*x1 Following rules are strictly oriented: b(r(x)) = 23 + 5*x > 11 + 5*x = r(b(x)) w(r(x)) = 8 + 2*x > 5 + 2*x = r(w(x)) Following rules are (at-least) weakly oriented: b(w(x)) = 18 + 10*x >= 18 + 10*x = w(b(x)) ** Step 1.b:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: b(r(x)) -> r(b(x)) b(w(x)) -> w(b(x)) w(r(x)) -> r(w(x)) - Signature: {b/1,w/1} / {r/1} - Obligation: innermost runtime complexity wrt. defined symbols {b,w} and constructors {r} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))