WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: app_xs#1(Cons(x7,x8),x10) -> Cons(x7,app_xs#1(x8,x10)) app_xs#1(Nil(),x6) -> x6 main(x4,x2) -> app_xs#1(x4,app_xs#1(x4,x2)) - Signature: {app_xs#1/2,main/2} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {app_xs#1,main} 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: uargs(Cons) = {2}, uargs(app_xs#1) = {2} Following symbols are considered usable: {app_xs#1,main} TcT has computed the following interpretation: p(Cons) = [1] x1 + [1] x2 + [1] p(Nil) = [4] p(app_xs#1) = [2] x1 + [2] x2 + [4] p(main) = [7] x1 + [4] x2 + [12] Following rules are strictly oriented: app_xs#1(Cons(x7,x8),x10) = [2] x10 + [2] x7 + [2] x8 + [6] > [2] x10 + [1] x7 + [2] x8 + [5] = Cons(x7,app_xs#1(x8,x10)) app_xs#1(Nil(),x6) = [2] x6 + [12] > [1] x6 + [0] = x6 Following rules are (at-least) weakly oriented: main(x4,x2) = [4] x2 + [7] x4 + [12] >= [4] x2 + [6] x4 + [12] = app_xs#1(x4,app_xs#1(x4,x2)) * Step 2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: main(x4,x2) -> app_xs#1(x4,app_xs#1(x4,x2)) - Weak TRS: app_xs#1(Cons(x7,x8),x10) -> Cons(x7,app_xs#1(x8,x10)) app_xs#1(Nil(),x6) -> x6 - Signature: {app_xs#1/2,main/2} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {app_xs#1,main} 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}, uargs(app_xs#1) = {2} Following symbols are considered usable: {app_xs#1,main} TcT has computed the following interpretation: p(Cons) = 4 + x1 + x2 p(Nil) = 12 p(app_xs#1) = 4 + 2*x1 + 2*x2 p(main) = 15 + 7*x1 + 6*x2 Following rules are strictly oriented: main(x4,x2) = 15 + 6*x2 + 7*x4 > 12 + 4*x2 + 6*x4 = app_xs#1(x4,app_xs#1(x4,x2)) Following rules are (at-least) weakly oriented: app_xs#1(Cons(x7,x8),x10) = 12 + 2*x10 + 2*x7 + 2*x8 >= 8 + 2*x10 + x7 + 2*x8 = Cons(x7,app_xs#1(x8,x10)) app_xs#1(Nil(),x6) = 28 + 2*x6 >= x6 = x6 * Step 3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: app_xs#1(Cons(x7,x8),x10) -> Cons(x7,app_xs#1(x8,x10)) app_xs#1(Nil(),x6) -> x6 main(x4,x2) -> app_xs#1(x4,app_xs#1(x4,x2)) - Signature: {app_xs#1/2,main/2} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {app_xs#1,main} and constructors {Cons,Nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))