WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),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: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(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: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: foldr#3(y){y -> Cons(x,y)} = foldr#3(Cons(x,y)) ->^+ step_x_f(rev_l(),x,foldr#3(y)) = C[foldr#3(y) = foldr#3(y){}] ** Step 1.b:1: NaturalPI 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: 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) = 3 + x2 p(Nil) = 2 p(fleft_op_e_xs_1) = 2 p(foldr#3) = x1 p(main) = 1 + 10*x1 p(rev_l) = 1 p(rev_l#2) = 6 + x1 p(step_x_f) = 2 + x1 + x3 p(step_x_f#1) = 1 + 10*x1 + 10*x3 + 4*x4 Following rules are strictly oriented: main(Cons(x8,x9)) = 31 + 10*x9 > 19 + 10*x9 = step_x_f#1(rev_l(),x8,foldr#3(x9),Nil()) main(Nil()) = 21 > 2 = Nil() rev_l#2(x8,x10) = 6 + x8 > 3 + x8 = Cons(x10,x8) step_x_f#1(rev_l(),x5,fleft_op_e_xs_1(),x3) = 31 + 4*x3 > 6 + x3 = rev_l#2(x3,x5) step_x_f#1(rev_l(),x5,step_x_f(x2,x3,x4),x1) = 31 + 4*x1 + 10*x2 + 10*x4 > 25 + 4*x1 + 10*x2 + 10*x4 = step_x_f#1(x2,x3,x4,rev_l#2(x1,x5)) Following rules are (at-least) weakly oriented: foldr#3(Cons(x16,x6)) = 3 + x6 >= 3 + x6 = step_x_f(rev_l(),x16,foldr#3(x6)) foldr#3(Nil()) = 2 >= 2 = fleft_op_e_xs_1() ** Step 1.b: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)) foldr#3(Nil()) -> fleft_op_e_xs_1() - Weak TRS: 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: 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) = x2 p(Nil) = 8 p(fleft_op_e_xs_1) = 13 p(foldr#3) = 2*x1 p(main) = 12 + 2*x1 p(rev_l) = 0 p(rev_l#2) = x1 p(step_x_f) = x3 p(step_x_f#1) = 4 + x3 + x4 Following rules are strictly oriented: foldr#3(Nil()) = 16 > 13 = fleft_op_e_xs_1() Following rules are (at-least) weakly oriented: foldr#3(Cons(x16,x6)) = 2*x6 >= 2*x6 = step_x_f(rev_l(),x16,foldr#3(x6)) main(Cons(x8,x9)) = 12 + 2*x9 >= 12 + 2*x9 = step_x_f#1(rev_l(),x8,foldr#3(x9),Nil()) main(Nil()) = 28 >= 8 = Nil() rev_l#2(x8,x10) = x8 >= x8 = Cons(x10,x8) step_x_f#1(rev_l(),x5,fleft_op_e_xs_1(),x3) = 17 + x3 >= x3 = rev_l#2(x3,x5) step_x_f#1(rev_l(),x5,step_x_f(x2,x3,x4),x1) = 4 + x1 + x4 >= 4 + x1 + x4 = step_x_f#1(x2,x3,x4,rev_l#2(x1,x5)) ** Step 1.b:3: NaturalPI 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: 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) = 3 + x2 p(Nil) = 3 p(fleft_op_e_xs_1) = 0 p(foldr#3) = x1 p(main) = 2 + 8*x1 p(rev_l) = 2 p(rev_l#2) = 10 + x1 p(step_x_f) = x1 + x3 p(step_x_f#1) = 7 + 8*x1 + 8*x3 + x4 Following rules are strictly oriented: foldr#3(Cons(x16,x6)) = 3 + x6 > 2 + x6 = step_x_f(rev_l(),x16,foldr#3(x6)) Following rules are (at-least) weakly oriented: foldr#3(Nil()) = 3 >= 0 = fleft_op_e_xs_1() main(Cons(x8,x9)) = 26 + 8*x9 >= 26 + 8*x9 = step_x_f#1(rev_l(),x8,foldr#3(x9),Nil()) main(Nil()) = 26 >= 3 = Nil() rev_l#2(x8,x10) = 10 + x8 >= 3 + x8 = Cons(x10,x8) step_x_f#1(rev_l(),x5,fleft_op_e_xs_1(),x3) = 23 + x3 >= 10 + x3 = rev_l#2(x3,x5) step_x_f#1(rev_l(),x5,step_x_f(x2,x3,x4),x1) = 23 + x1 + 8*x2 + 8*x4 >= 17 + x1 + 8*x2 + 8*x4 = step_x_f#1(x2,x3,x4,rev_l#2(x1,x5)) ** Step 1.b: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(Omega(n^1),O(n^1))