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