WORST_CASE(?,O(n^1)) * Step 1: WeightGap 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: 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: all TcT has computed the following interpretation: p(Cons) = [1] x1 + [1] x2 + [1] p(Nil) = [6] p(One) = [0] p(Zero) = [4] p(add#2) = [1] x1 + [4] x2 + [0] p(inc#1) = [1] x1 + [0] p(main) = [1] x1 + [4] x2 + [2] Following rules are strictly oriented: add#2(x2,Nil()) = [1] x2 + [24] > [1] x2 + [0] = x2 add#2(Cons(x6,x4),Cons(Zero(),x2)) = [4] x2 + [1] x4 + [1] x6 + [21] > [4] x2 + [1] x4 + [1] x6 + [1] = Cons(x6,add#2(x4,x2)) add#2(Cons(Zero(),x4),Cons(One(),x2)) = [4] x2 + [1] x4 + [9] > [4] x2 + [1] x4 + [1] = Cons(One(),add#2(x4,x2)) add#2(Nil(),Cons(x4,x2)) = [4] x2 + [4] x4 + [10] > [1] x2 + [1] x4 + [1] = Cons(x4,x2) inc#1(Cons(Zero(),x8)) = [1] x8 + [5] > [1] x8 + [1] = Cons(One(),x8) main(x2,x1) = [4] x1 + [1] x2 + [2] > [4] x1 + [1] x2 + [0] = add#2(x2,x1) Following rules are (at-least) weakly oriented: add#2(Cons(One(),x4),Cons(One(),x2)) = [4] x2 + [1] x4 + [5] >= [4] x2 + [1] x4 + [5] = Cons(Zero(),inc#1(add#2(x4,x2))) inc#1(Cons(One(),x8)) = [1] x8 + [1] >= [1] x8 + [5] = Cons(Zero(),inc#1(x8)) inc#1(Nil()) = [6] >= [7] = Cons(One(),Nil()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: add#2(Cons(One(),x4),Cons(One(),x2)) -> Cons(Zero(),inc#1(add#2(x4,x2))) 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(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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: 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: all TcT has computed the following interpretation: p(Cons) = [1] x1 + [1] x2 + [0] p(Nil) = [0] p(One) = [0] p(Zero) = [2] p(add#2) = [2] x1 + [2] x2 + [4] p(inc#1) = [1] x1 + [1] p(main) = [2] x1 + [4] x2 + [4] Following rules are strictly oriented: inc#1(Nil()) = [1] > [0] = Cons(One(),Nil()) Following rules are (at-least) weakly oriented: add#2(x2,Nil()) = [2] x2 + [4] >= [1] x2 + [0] = x2 add#2(Cons(x6,x4),Cons(Zero(),x2)) = [2] x2 + [2] x4 + [2] x6 + [8] >= [2] x2 + [2] x4 + [1] x6 + [4] = Cons(x6,add#2(x4,x2)) add#2(Cons(One(),x4),Cons(One(),x2)) = [2] x2 + [2] x4 + [4] >= [2] x2 + [2] x4 + [7] = Cons(Zero(),inc#1(add#2(x4,x2))) add#2(Cons(Zero(),x4),Cons(One(),x2)) = [2] x2 + [2] x4 + [8] >= [2] x2 + [2] x4 + [4] = Cons(One(),add#2(x4,x2)) add#2(Nil(),Cons(x4,x2)) = [2] x2 + [2] x4 + [4] >= [1] x2 + [1] x4 + [0] = Cons(x4,x2) inc#1(Cons(One(),x8)) = [1] x8 + [1] >= [1] x8 + [3] = Cons(Zero(),inc#1(x8)) inc#1(Cons(Zero(),x8)) = [1] x8 + [3] >= [1] x8 + [0] = Cons(One(),x8) main(x2,x1) = [4] x1 + [2] x2 + [4] >= [2] x1 + [2] x2 + [4] = add#2(x2,x1) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: add#2(Cons(One(),x4),Cons(One(),x2)) -> Cons(Zero(),inc#1(add#2(x4,x2))) inc#1(Cons(One(),x8)) -> Cons(Zero(),inc#1(x8)) - Weak TRS: add#2(x2,Nil()) -> x2 add#2(Cons(x6,x4),Cons(Zero(),x2)) -> Cons(x6,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) 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: 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: all TcT has computed the following interpretation: p(Cons) = [1] x2 + [2] p(Nil) = [0] p(One) = [0] p(Zero) = [0] p(add#2) = [4] x1 + [1] x2 + [0] p(inc#1) = [1] x1 + [2] p(main) = [4] x1 + [1] x2 + [0] Following rules are strictly oriented: add#2(Cons(One(),x4),Cons(One(),x2)) = [1] x2 + [4] x4 + [10] > [1] x2 + [4] x4 + [4] = Cons(Zero(),inc#1(add#2(x4,x2))) Following rules are (at-least) weakly oriented: add#2(x2,Nil()) = [4] x2 + [0] >= [1] x2 + [0] = x2 add#2(Cons(x6,x4),Cons(Zero(),x2)) = [1] x2 + [4] x4 + [10] >= [1] x2 + [4] x4 + [2] = Cons(x6,add#2(x4,x2)) add#2(Cons(Zero(),x4),Cons(One(),x2)) = [1] x2 + [4] x4 + [10] >= [1] x2 + [4] x4 + [2] = Cons(One(),add#2(x4,x2)) add#2(Nil(),Cons(x4,x2)) = [1] x2 + [2] >= [1] x2 + [2] = Cons(x4,x2) inc#1(Cons(One(),x8)) = [1] x8 + [4] >= [1] x8 + [4] = Cons(Zero(),inc#1(x8)) inc#1(Cons(Zero(),x8)) = [1] x8 + [4] >= [1] x8 + [2] = Cons(One(),x8) inc#1(Nil()) = [2] >= [2] = Cons(One(),Nil()) main(x2,x1) = [1] x1 + [4] x2 + [0] >= [1] x1 + [4] x2 + [0] = add#2(x2,x1) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: inc#1(Cons(One(),x8)) -> Cons(Zero(),inc#1(x8)) - 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) 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: 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: all TcT has computed the following interpretation: p(Cons) = [1] x1 + [1] x2 + [0] p(Nil) = [0] p(One) = [1] p(Zero) = [0] p(add#2) = [6] x1 + [1] x2 + [0] p(inc#1) = [1] x1 + [4] p(main) = [7] x1 + [5] x2 + [0] Following rules are strictly oriented: inc#1(Cons(One(),x8)) = [1] x8 + [5] > [1] x8 + [4] = Cons(Zero(),inc#1(x8)) Following rules are (at-least) weakly oriented: add#2(x2,Nil()) = [6] x2 + [0] >= [1] x2 + [0] = x2 add#2(Cons(x6,x4),Cons(Zero(),x2)) = [1] x2 + [6] x4 + [6] x6 + [0] >= [1] x2 + [6] x4 + [1] x6 + [0] = Cons(x6,add#2(x4,x2)) add#2(Cons(One(),x4),Cons(One(),x2)) = [1] x2 + [6] x4 + [7] >= [1] x2 + [6] x4 + [4] = Cons(Zero(),inc#1(add#2(x4,x2))) add#2(Cons(Zero(),x4),Cons(One(),x2)) = [1] x2 + [6] x4 + [1] >= [1] x2 + [6] x4 + [1] = Cons(One(),add#2(x4,x2)) add#2(Nil(),Cons(x4,x2)) = [1] x2 + [1] x4 + [0] >= [1] x2 + [1] x4 + [0] = Cons(x4,x2) inc#1(Cons(Zero(),x8)) = [1] x8 + [4] >= [1] x8 + [1] = Cons(One(),x8) inc#1(Nil()) = [4] >= [1] = Cons(One(),Nil()) main(x2,x1) = [5] x1 + [7] x2 + [0] >= [1] x1 + [6] x2 + [0] = add#2(x2,x1) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: 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))