WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__f(X)) -> f(activate(X)) activate(n__s(X)) -> s(activate(X)) f(X) -> n__f(X) f(0()) -> cons(0(),n__f(n__s(n__0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() s(X) -> n__s(X) - Signature: {0/0,activate/1,f/1,p/1,s/1} / {cons/2,n__0/0,n__f/1,n__s/1} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,f,p,s} and constructors {cons,n__0,n__f,n__s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__f(X)) -> f(activate(X)) activate(n__s(X)) -> s(activate(X)) f(X) -> n__f(X) f(0()) -> cons(0(),n__f(n__s(n__0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() s(X) -> n__s(X) - Signature: {0/0,activate/1,f/1,p/1,s/1} / {cons/2,n__0/0,n__f/1,n__s/1} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,f,p,s} and constructors {cons,n__0,n__f,n__s} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: activate(x){x -> n__f(x)} = activate(n__f(x)) ->^+ f(activate(x)) = C[activate(x) = activate(x){}] ** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__f(X)) -> f(activate(X)) activate(n__s(X)) -> s(activate(X)) f(X) -> n__f(X) f(0()) -> cons(0(),n__f(n__s(n__0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() s(X) -> n__s(X) - Signature: {0/0,activate/1,f/1,p/1,s/1} / {cons/2,n__0/0,n__f/1,n__s/1} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,f,p,s} and constructors {cons,n__0,n__f,n__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(f) = {1}, uargs(s) = {1} Following symbols are considered usable: {0,activate,f,p,s} TcT has computed the following interpretation: p(0) = 2 p(activate) = 2 + 2*x1 p(cons) = 9 + x1 p(f) = 14 + x1 p(n__0) = 2 p(n__f) = 7 + x1 p(n__s) = 11 + x1 p(p) = x1 p(s) = 15 + x1 Following rules are strictly oriented: activate(X) = 2 + 2*X > X = X activate(n__0()) = 6 > 2 = 0() activate(n__s(X)) = 24 + 2*X > 17 + 2*X = s(activate(X)) f(X) = 14 + X > 7 + X = n__f(X) f(0()) = 16 > 11 = cons(0(),n__f(n__s(n__0()))) p(s(0())) = 17 > 2 = 0() s(X) = 15 + X > 11 + X = n__s(X) Following rules are (at-least) weakly oriented: 0() = 2 >= 2 = n__0() activate(n__f(X)) = 16 + 2*X >= 16 + 2*X = f(activate(X)) f(s(0())) = 31 >= 31 = f(p(s(0()))) ** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: 0() -> n__0() activate(n__f(X)) -> f(activate(X)) f(s(0())) -> f(p(s(0()))) - Weak TRS: activate(X) -> X activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) f(X) -> n__f(X) f(0()) -> cons(0(),n__f(n__s(n__0()))) p(s(0())) -> 0() s(X) -> n__s(X) - Signature: {0/0,activate/1,f/1,p/1,s/1} / {cons/2,n__0/0,n__f/1,n__s/1} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,f,p,s} and constructors {cons,n__0,n__f,n__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(f) = {1}, uargs(s) = {1} Following symbols are considered usable: {0,activate,f,p,s} TcT has computed the following interpretation: p(0) = 0 p(activate) = 6 + 8*x1 p(cons) = 6 p(f) = 12 + x1 p(n__0) = 0 p(n__f) = 3 + x1 p(n__s) = 1 + x1 p(p) = 1 p(s) = 4 + x1 Following rules are strictly oriented: activate(n__f(X)) = 30 + 8*X > 18 + 8*X = f(activate(X)) f(s(0())) = 16 > 13 = f(p(s(0()))) Following rules are (at-least) weakly oriented: 0() = 0 >= 0 = n__0() activate(X) = 6 + 8*X >= X = X activate(n__0()) = 6 >= 0 = 0() activate(n__s(X)) = 14 + 8*X >= 10 + 8*X = s(activate(X)) f(X) = 12 + X >= 3 + X = n__f(X) f(0()) = 12 >= 6 = cons(0(),n__f(n__s(n__0()))) p(s(0())) = 1 >= 0 = 0() s(X) = 4 + X >= 1 + X = n__s(X) ** Step 1.b:3: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: 0() -> n__0() - Weak TRS: activate(X) -> X activate(n__0()) -> 0() activate(n__f(X)) -> f(activate(X)) activate(n__s(X)) -> s(activate(X)) f(X) -> n__f(X) f(0()) -> cons(0(),n__f(n__s(n__0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() s(X) -> n__s(X) - Signature: {0/0,activate/1,f/1,p/1,s/1} / {cons/2,n__0/0,n__f/1,n__s/1} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,f,p,s} and constructors {cons,n__0,n__f,n__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(f) = {1}, uargs(s) = {1} Following symbols are considered usable: {0,activate,f,p,s} TcT has computed the following interpretation: p(0) = 1 p(activate) = 6 + 2*x1 p(cons) = x1 p(f) = x1 p(n__0) = 0 p(n__f) = x1 p(n__s) = 9 + x1 p(p) = 1 p(s) = 9 + x1 Following rules are strictly oriented: 0() = 1 > 0 = n__0() Following rules are (at-least) weakly oriented: activate(X) = 6 + 2*X >= X = X activate(n__0()) = 6 >= 1 = 0() activate(n__f(X)) = 6 + 2*X >= 6 + 2*X = f(activate(X)) activate(n__s(X)) = 24 + 2*X >= 15 + 2*X = s(activate(X)) f(X) = X >= X = n__f(X) f(0()) = 1 >= 1 = cons(0(),n__f(n__s(n__0()))) f(s(0())) = 10 >= 1 = f(p(s(0()))) p(s(0())) = 1 >= 1 = 0() s(X) = 9 + X >= 9 + X = n__s(X) ** Step 1.b:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__f(X)) -> f(activate(X)) activate(n__s(X)) -> s(activate(X)) f(X) -> n__f(X) f(0()) -> cons(0(),n__f(n__s(n__0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() s(X) -> n__s(X) - Signature: {0/0,activate/1,f/1,p/1,s/1} / {cons/2,n__0/0,n__f/1,n__s/1} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,f,p,s} and constructors {cons,n__0,n__f,n__s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))