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