WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: anchored(Cons(x,xs),y) -> anchored(xs,Cons(Cons(Nil(),Nil()),y)) anchored(Nil(),y) -> y goal(x,y) -> anchored(x,y) - Signature: {anchored/2,goal/2} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {anchored,goal} and constructors {Cons,Nil} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: none Following symbols are considered usable: {anchored,goal} TcT has computed the following interpretation: p(Cons) = [0] p(Nil) = [8] p(anchored) = [8] x2 + [11] p(goal) = [12] x2 + [11] Following rules are strictly oriented: anchored(Nil(),y) = [8] y + [11] > [1] y + [0] = y Following rules are (at-least) weakly oriented: anchored(Cons(x,xs),y) = [8] y + [11] >= [11] = anchored(xs,Cons(Cons(Nil(),Nil()),y)) goal(x,y) = [12] y + [11] >= [8] y + [11] = anchored(x,y) * Step 2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: anchored(Cons(x,xs),y) -> anchored(xs,Cons(Cons(Nil(),Nil()),y)) goal(x,y) -> anchored(x,y) - Weak TRS: anchored(Nil(),y) -> y - Signature: {anchored/2,goal/2} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {anchored,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: none Following symbols are considered usable: {anchored,goal} TcT has computed the following interpretation: p(Cons) = x2 p(Nil) = 4 p(anchored) = 8*x2 p(goal) = 8 + 8*x2 Following rules are strictly oriented: goal(x,y) = 8 + 8*y > 8*y = anchored(x,y) Following rules are (at-least) weakly oriented: anchored(Cons(x,xs),y) = 8*y >= 8*y = anchored(xs,Cons(Cons(Nil(),Nil()),y)) anchored(Nil(),y) = 8*y >= y = y * Step 3: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: anchored(Cons(x,xs),y) -> anchored(xs,Cons(Cons(Nil(),Nil()),y)) - Weak TRS: anchored(Nil(),y) -> y goal(x,y) -> anchored(x,y) - Signature: {anchored/2,goal/2} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {anchored,goal} and constructors {Cons,Nil} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: none Following symbols are considered usable: {anchored,goal} TcT has computed the following interpretation: p(Cons) = [1] x2 + [2] p(Nil) = [0] p(anchored) = [4] x1 + [3] x2 + [2] p(goal) = [6] x1 + [3] x2 + [3] Following rules are strictly oriented: anchored(Cons(x,xs),y) = [4] xs + [3] y + [10] > [4] xs + [3] y + [8] = anchored(xs,Cons(Cons(Nil(),Nil()),y)) Following rules are (at-least) weakly oriented: anchored(Nil(),y) = [3] y + [2] >= [1] y + [0] = y goal(x,y) = [6] x + [3] y + [3] >= [4] x + [3] y + [2] = anchored(x,y) * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: anchored(Cons(x,xs),y) -> anchored(xs,Cons(Cons(Nil(),Nil()),y)) anchored(Nil(),y) -> y goal(x,y) -> anchored(x,y) - Signature: {anchored/2,goal/2} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {anchored,goal} and constructors {Cons,Nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))