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: NaturalMI 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: 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 + [0] p(Nil) = [6] p(app_xs#1) = [1] x1 + [1] x2 + [0] p(main) = [8] x1 + [1] x2 + [9] Following rules are strictly oriented: main(x4,x2) = [1] x2 + [8] x4 + [9] > [1] x2 + [2] x4 + [0] = app_xs#1(x4,app_xs#1(x4,x2)) Following rules are (at-least) weakly oriented: app_xs#1(Cons(x7,x8),x10) = [1] x10 + [1] x7 + [1] x8 + [0] >= [1] x10 + [1] x7 + [1] x8 + [0] = Cons(x7,app_xs#1(x8,x10)) app_xs#1(Nil(),x6) = [1] x6 + [6] >= [1] x6 + [0] = 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))