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