* 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: MI 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: MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 1, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)): 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] x_2 + [0] p(Nil) = [0] p(duplicate) = [0] p(goal) = [8] Following rules are strictly oriented: goal(x) = [8] > [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: WeightGap 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Cons) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(Cons) = [1] x2 + [0] p(Nil) = [0] p(duplicate) = [5] p(goal) = [5] Following rules are strictly oriented: duplicate(Nil()) = [5] > [0] = Nil() Following rules are (at-least) weakly oriented: duplicate(Cons(x,xs)) = [5] >= [5] = Cons(x,Cons(x,duplicate(xs))) goal(x) = [5] >= [5] = duplicate(x) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 1.b:3: WeightGap 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Cons) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(Cons) = [1] x2 + [1] p(Nil) = [10] p(duplicate) = [3] x1 + [0] p(goal) = [9] x1 + [0] Following rules are strictly oriented: duplicate(Cons(x,xs)) = [3] xs + [3] > [3] xs + [2] = Cons(x,Cons(x,duplicate(xs))) Following rules are (at-least) weakly oriented: duplicate(Nil()) = [30] >= [10] = Nil() goal(x) = [9] x + [0] >= [3] x + [0] = duplicate(x) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** 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))