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