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