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