MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) app(cons(x,l1),l2) -> cons(x,app(l1,l2)) app(nil(),l) -> l prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1} / {0/0,cons/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,+,app,prod,sum} and constructors {0,cons,nil,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs *#(x,0()) -> c_1() *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(0(),x) -> c_3() *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(x,0()) -> c_5() +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(0(),x) -> c_7() +#(s(x),s(y)) -> c_8(+#(x,y)) app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) app#(nil(),l) -> c_10() prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) prod#(nil()) -> c_13() sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) sum#(nil()) -> c_16() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: *#(x,0()) -> c_1() *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(0(),x) -> c_3() *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(x,0()) -> c_5() +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(0(),x) -> c_7() +#(s(x),s(y)) -> c_8(+#(x,y)) app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) app#(nil(),l) -> c_10() prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) prod#(nil()) -> c_13() sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) sum#(nil()) -> c_16() - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) app(cons(x,l1),l2) -> cons(x,app(l1,l2)) app(nil(),l) -> l prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() *#(x,0()) -> c_1() *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(0(),x) -> c_3() *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(x,0()) -> c_5() +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(0(),x) -> c_7() +#(s(x),s(y)) -> c_8(+#(x,y)) app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) app#(nil(),l) -> c_10() prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) prod#(nil()) -> c_13() sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) sum#(nil()) -> c_16() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: *#(x,0()) -> c_1() *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(0(),x) -> c_3() *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(x,0()) -> c_5() +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(0(),x) -> c_7() +#(s(x),s(y)) -> c_8(+#(x,y)) app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) app#(nil(),l) -> c_10() prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) prod#(nil()) -> c_13() sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) sum#(nil()) -> c_16() - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,5,7,10,13,16} by application of Pre({1,3,5,7,10,13,16}) = {2,4,6,8,9,11,12,14,15}. Here rules are labelled as follows: 1: *#(x,0()) -> c_1() 2: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) 3: *#(0(),x) -> c_3() 4: *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) 5: +#(x,0()) -> c_5() 6: +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) 7: +#(0(),x) -> c_7() 8: +#(s(x),s(y)) -> c_8(+#(x,y)) 9: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) 10: app#(nil(),l) -> c_10() 11: prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) 12: prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) 13: prod#(nil()) -> c_13() 14: sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) 15: sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) 16: sum#(nil()) -> c_16() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) - Weak DPs: *#(x,0()) -> c_1() *#(0(),x) -> c_3() +#(x,0()) -> c_5() +#(0(),x) -> c_7() app#(nil(),l) -> c_10() prod#(nil()) -> c_13() sum#(nil()) -> c_16() - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) -->_2 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_2 *#(0(),x) -> c_3():11 -->_1 *#(0(),x) -> c_3():11 -->_2 *#(x,0()) -> c_1():10 -->_1 *#(x,0()) -> c_1():10 -->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 2:S:*#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) -->_3 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_3 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 -->_3 +#(0(),x) -> c_7():13 -->_1 +#(0(),x) -> c_7():13 -->_3 +#(x,0()) -> c_5():12 -->_1 +#(x,0()) -> c_5():12 -->_2 *#(0(),x) -> c_3():11 -->_2 *#(x,0()) -> c_1():10 -->_2 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 3:S:+#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) -->_2 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_2 +#(0(),x) -> c_7():13 -->_1 +#(0(),x) -> c_7():13 -->_2 +#(x,0()) -> c_5():12 -->_1 +#(x,0()) -> c_5():12 -->_2 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 4:S:+#(s(x),s(y)) -> c_8(+#(x,y)) -->_1 +#(0(),x) -> c_7():13 -->_1 +#(x,0()) -> c_5():12 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 5:S:app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) -->_1 app#(nil(),l) -> c_10():14 -->_1 app#(cons(x,l1),l2) -> c_9(app#(l1,l2)):5 6:S:prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) -->_3 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):7 -->_2 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):7 -->_3 prod#(nil()) -> c_13():15 -->_2 prod#(nil()) -> c_13():15 -->_1 *#(0(),x) -> c_3():11 -->_1 *#(x,0()) -> c_1():10 -->_3 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):6 -->_2 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):6 -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 7:S:prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) -->_2 prod#(nil()) -> c_13():15 -->_1 *#(0(),x) -> c_3():11 -->_1 *#(x,0()) -> c_1():10 -->_2 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):7 -->_2 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):6 -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 8:S:sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) -->_3 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):9 -->_2 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):9 -->_3 sum#(nil()) -> c_16():16 -->_2 sum#(nil()) -> c_16():16 -->_1 +#(0(),x) -> c_7():13 -->_1 +#(x,0()) -> c_5():12 -->_3 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):8 -->_2 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):8 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 9:S:sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) -->_2 sum#(nil()) -> c_16():16 -->_1 +#(0(),x) -> c_7():13 -->_1 +#(x,0()) -> c_5():12 -->_2 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):9 -->_2 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):8 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 10:W:*#(x,0()) -> c_1() 11:W:*#(0(),x) -> c_3() 12:W:+#(x,0()) -> c_5() 13:W:+#(0(),x) -> c_7() 14:W:app#(nil(),l) -> c_10() 15:W:prod#(nil()) -> c_13() 16:W:sum#(nil()) -> c_16() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 16: sum#(nil()) -> c_16() 15: prod#(nil()) -> c_13() 14: app#(nil(),l) -> c_10() 10: *#(x,0()) -> c_1() 11: *#(0(),x) -> c_3() 12: +#(x,0()) -> c_5() 13: +#(0(),x) -> c_7() * Step 5: Decompose MAYBE + Considered Problem: - Strict DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) - Weak DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0 ,c_4/3,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} Problem (S) - Strict DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) - Weak DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0 ,c_4/3,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} ** Step 5.a:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) - Weak DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) -->_2 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 2:S:*#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) -->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 -->_3 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_3 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 -->_2 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 3:S:+#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) -->_2 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_2 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 4:S:+#(s(x),s(y)) -> c_8(+#(x,y)) -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 5:W:app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) -->_1 app#(cons(x,l1),l2) -> c_9(app#(l1,l2)):5 6:W:prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_3 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):7 -->_2 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):7 -->_3 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):6 -->_2 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):6 7:W:prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):2 -->_2 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):6 -->_2 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):7 8:W:sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_3 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):9 -->_2 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):9 -->_3 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):8 -->_2 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):8 9:W:sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):3 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):4 -->_2 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):8 -->_2 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):9 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) ** Step 5.a:2: DecomposeDG MAYBE + Considered Problem: - Strict DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) - Weak DPs: prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) and a lower component *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) Further, following extension rules are added to the lower component. prod#(app(l1,l2)) -> *#(prod(l1),prod(l2)) prod#(app(l1,l2)) -> prod#(l1) prod#(app(l1,l2)) -> prod#(l2) prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(app(l1,l2)) -> +#(sum(l1),sum(l2)) sum#(app(l1,l2)) -> sum#(l1) sum#(app(l1,l2)) -> sum#(l2) sum#(cons(x,l)) -> +#(x,sum(l)) sum#(cons(x,l)) -> sum#(l) *** Step 5.a:2.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 3: sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) 4: sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) The strictly oriented rules are moved into the weak component. **** Step 5.a:2.a:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_11) = {1,2,3}, uargs(c_12) = {1,2}, uargs(c_14) = {1,2,3}, uargs(c_15) = {1,2} Following symbols are considered usable: {*#,+#,app#,prod#,sum#} TcT has computed the following interpretation: p(*) = [0] p(+) = [0] p(0) = [0] p(app) = [4] x1 + [1] x2 + [5] p(cons) = [1] x1 + [1] x2 + [5] p(nil) = [0] p(prod) = [0] p(s) = [0] p(sum) = [1] x1 + [0] p(*#) = [5] p(+#) = [1] p(app#) = [0] p(prod#) = [1] x1 + [0] p(sum#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [1] x1 + [4] x2 + [1] x3 + [0] p(c_12) = [1] x1 + [1] x2 + [0] p(c_13) = [0] p(c_14) = [4] x1 + [4] x2 + [1] x3 + [0] p(c_15) = [1] x1 + [1] x2 + [0] p(c_16) = [0] Following rules are strictly oriented: sum#(app(l1,l2)) = [4] l1 + [1] l2 + [5] > [4] l1 + [1] l2 + [4] = c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) = [1] l + [1] x + [5] > [1] l + [1] = c_15(+#(x,sum(l)),sum#(l)) Following rules are (at-least) weakly oriented: prod#(app(l1,l2)) = [4] l1 + [1] l2 + [5] >= [4] l1 + [1] l2 + [5] = c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) = [1] l + [1] x + [5] >= [1] l + [5] = c_12(*#(x,prod(l)),prod#(l)) **** Step 5.a:2.a:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) - Weak DPs: sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 5.a:2.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) - Weak DPs: sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) -->_3 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):2 -->_2 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):2 -->_3 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):1 -->_2 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):1 2:S:prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) -->_2 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):2 -->_2 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):1 3:W:sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) -->_3 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):4 -->_2 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):4 -->_3 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):3 -->_2 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):3 4:W:sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) -->_2 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):4 -->_2 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) 4: sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) **** Step 5.a:2.a:1.b:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) -->_3 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):2 -->_2 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):2 -->_3 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):1 -->_2 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):1 2:S:prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) -->_2 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):2 -->_2 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) **** Step 5.a:2.a:1.b:3: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) **** Step 5.a:2.a:1.b:4: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) 2: prod#(cons(x,l)) -> c_12(prod#(l)) The strictly oriented rules are moved into the weak component. ***** Step 5.a:2.a:1.b:4.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_11) = {1,2}, uargs(c_12) = {1} Following symbols are considered usable: {*#,+#,app#,prod#,sum#} TcT has computed the following interpretation: p(*) = [2] x2 + [0] p(+) = [1] x1 + [2] x2 + [1] p(0) = [4] p(app) = [7] x1 + [2] x2 + [5] p(cons) = [1] x2 + [4] p(nil) = [4] p(prod) = [0] p(s) = [0] p(sum) = [1] p(*#) = [1] x1 + [2] p(+#) = [1] x2 + [0] p(app#) = [1] p(prod#) = [4] x1 + [0] p(sum#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [4] x1 + [2] x2 + [9] p(c_12) = [1] x1 + [3] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] Following rules are strictly oriented: prod#(app(l1,l2)) = [28] l1 + [8] l2 + [20] > [16] l1 + [8] l2 + [9] = c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) = [4] l + [16] > [4] l + [3] = c_12(prod#(l)) Following rules are (at-least) weakly oriented: ***** Step 5.a:2.a:1.b:4.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 5.a:2.a:1.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) -->_2 prod#(cons(x,l)) -> c_12(prod#(l)):2 -->_1 prod#(cons(x,l)) -> c_12(prod#(l)):2 -->_2 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):1 -->_1 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):1 2:W:prod#(cons(x,l)) -> c_12(prod#(l)) -->_1 prod#(cons(x,l)) -> c_12(prod#(l)):2 -->_1 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) 2: prod#(cons(x,l)) -> c_12(prod#(l)) ***** Step 5.a:2.a:1.b:4.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 5.a:2.b:1: Failure MAYBE + Considered Problem: - Strict DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) - Weak DPs: prod#(app(l1,l2)) -> *#(prod(l1),prod(l2)) prod#(app(l1,l2)) -> prod#(l1) prod#(app(l1,l2)) -> prod#(l2) prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) sum#(app(l1,l2)) -> +#(sum(l1),sum(l2)) sum#(app(l1,l2)) -> sum#(l1) sum#(app(l1,l2)) -> sum#(l2) sum#(cons(x,l)) -> +#(x,sum(l)) sum#(cons(x,l)) -> sum#(l) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. ** Step 5.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) - Weak DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) +#(s(x),s(y)) -> c_8(+#(x,y)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) -->_1 app#(cons(x,l1),l2) -> c_9(app#(l1,l2)):1 2:S:prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):7 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):6 -->_3 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):3 -->_2 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):3 -->_3 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):2 -->_2 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):2 3:S:prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):7 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):6 -->_2 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):3 -->_2 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):2 4:S:sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):9 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):8 -->_3 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):5 -->_2 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):5 -->_3 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):4 -->_2 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):4 5:S:sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):9 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):8 -->_2 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):5 -->_2 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):4 6:W:*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) -->_2 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):7 -->_1 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):7 -->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):6 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):6 7:W:*#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) -->_3 +#(s(x),s(y)) -> c_8(+#(x,y)):9 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):9 -->_3 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):8 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):8 -->_2 *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)):7 -->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):6 8:W:+#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) -->_2 +#(s(x),s(y)) -> c_8(+#(x,y)):9 -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):9 -->_2 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):8 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):8 9:W:+#(s(x),s(y)) -> c_8(+#(x,y)) -->_1 +#(s(x),s(y)) -> c_8(+#(x,y)):9 -->_1 +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)):8 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 7: *#(s(x),s(y)) -> c_4(+#(*(x,y),+(x,y)),*#(x,y),+#(x,y)) 6: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) 9: +#(s(x),s(y)) -> c_8(+#(x,y)) 8: +#(+(x,y),z) -> c_6(+#(x,+(y,z)),+#(y,z)) ** Step 5.b:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/2,c_13/0,c_14/3,c_15/2,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) -->_1 app#(cons(x,l1),l2) -> c_9(app#(l1,l2)):1 2:S:prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) -->_3 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):3 -->_2 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):3 -->_3 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):2 -->_2 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):2 3:S:prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)) -->_2 prod#(cons(x,l)) -> c_12(*#(x,prod(l)),prod#(l)):3 -->_2 prod#(app(l1,l2)) -> c_11(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):2 4:S:sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) -->_3 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):5 -->_2 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):5 -->_3 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):4 -->_2 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):4 5:S:sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)) -->_2 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):5 -->_2 sum#(app(l1,l2)) -> c_14(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) ** Step 5.b:3: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> s(0()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0() - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) ** Step 5.b:4: Decompose WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) - Weak DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0 ,c_4/3,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} Problem (S) - Strict DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Weak DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0 ,c_4/3,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} *** Step 5.b:4.a:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) - Weak DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) -->_1 app#(cons(x,l1),l2) -> c_9(app#(l1,l2)):1 2:W:prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) -->_2 prod#(cons(x,l)) -> c_12(prod#(l)):3 -->_1 prod#(cons(x,l)) -> c_12(prod#(l)):3 -->_2 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):2 -->_1 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):2 3:W:prod#(cons(x,l)) -> c_12(prod#(l)) -->_1 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):2 -->_1 prod#(cons(x,l)) -> c_12(prod#(l)):3 4:W:sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) -->_2 sum#(cons(x,l)) -> c_15(sum#(l)):5 -->_1 sum#(cons(x,l)) -> c_15(sum#(l)):5 -->_2 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):4 -->_1 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):4 5:W:sum#(cons(x,l)) -> c_15(sum#(l)) -->_1 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):4 -->_1 sum#(cons(x,l)) -> c_15(sum#(l)):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) 5: sum#(cons(x,l)) -> c_15(sum#(l)) 2: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) 3: prod#(cons(x,l)) -> c_12(prod#(l)) *** Step 5.b:4.a:2: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) The strictly oriented rules are moved into the weak component. **** Step 5.b:4.a:2.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_9) = {1} Following symbols are considered usable: {*#,+#,app#,prod#,sum#} TcT has computed the following interpretation: p(*) = [0] p(+) = [0] p(0) = [0] p(app) = [0] p(cons) = [1] x2 + [2] p(nil) = [0] p(prod) = [0] p(s) = [1] x1 + [0] p(sum) = [0] p(*#) = [0] p(+#) = [0] p(app#) = [1] x1 + [1] p(prod#) = [0] p(sum#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [1] x1 + [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] Following rules are strictly oriented: app#(cons(x,l1),l2) = [1] l1 + [3] > [1] l1 + [1] = c_9(app#(l1,l2)) Following rules are (at-least) weakly oriented: **** Step 5.b:4.a:2.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 5.b:4.a:2.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) -->_1 app#(cons(x,l1),l2) -> c_9(app#(l1,l2)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) **** Step 5.b:4.a:2.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 5.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Weak DPs: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) -->_2 prod#(cons(x,l)) -> c_12(prod#(l)):2 -->_1 prod#(cons(x,l)) -> c_12(prod#(l)):2 -->_2 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):1 -->_1 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):1 2:S:prod#(cons(x,l)) -> c_12(prod#(l)) -->_1 prod#(cons(x,l)) -> c_12(prod#(l)):2 -->_1 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):1 3:S:sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) -->_2 sum#(cons(x,l)) -> c_15(sum#(l)):4 -->_1 sum#(cons(x,l)) -> c_15(sum#(l)):4 -->_2 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):3 -->_1 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):3 4:S:sum#(cons(x,l)) -> c_15(sum#(l)) -->_1 sum#(cons(x,l)) -> c_15(sum#(l)):4 -->_1 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):3 5:W:app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) -->_1 app#(cons(x,l1),l2) -> c_9(app#(l1,l2)):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: app#(cons(x,l1),l2) -> c_9(app#(l1,l2)) *** Step 5.b:4.b:2: Decompose WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) - Weak DPs: sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0 ,c_4/3,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} Problem (S) - Strict DPs: sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Weak DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0 ,c_4/3,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} **** Step 5.b:4.b:2.a:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) - Weak DPs: sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) -->_2 prod#(cons(x,l)) -> c_12(prod#(l)):2 -->_1 prod#(cons(x,l)) -> c_12(prod#(l)):2 -->_2 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):1 -->_1 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):1 2:S:prod#(cons(x,l)) -> c_12(prod#(l)) -->_1 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):1 -->_1 prod#(cons(x,l)) -> c_12(prod#(l)):2 3:W:sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) -->_2 sum#(cons(x,l)) -> c_15(sum#(l)):4 -->_1 sum#(cons(x,l)) -> c_15(sum#(l)):4 -->_2 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):3 -->_1 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):3 4:W:sum#(cons(x,l)) -> c_15(sum#(l)) -->_1 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):3 -->_1 sum#(cons(x,l)) -> c_15(sum#(l)):4 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) 4: sum#(cons(x,l)) -> c_15(sum#(l)) **** Step 5.b:4.b:2.a:2: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: prod#(cons(x,l)) -> c_12(prod#(l)) The strictly oriented rules are moved into the weak component. ***** Step 5.b:4.b:2.a:2.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_11) = {1,2}, uargs(c_12) = {1} Following symbols are considered usable: {*#,+#,app#,prod#,sum#} TcT has computed the following interpretation: p(*) = [1] p(+) = [1] x1 + [4] x2 + [2] p(0) = [0] p(app) = [10] x1 + [10] x2 + [0] p(cons) = [1] x2 + [8] p(nil) = [0] p(prod) = [2] x1 + [1] p(s) = [1] x1 + [0] p(sum) = [0] p(*#) = [1] x2 + [0] p(+#) = [1] p(app#) = [1] x2 + [2] p(prod#) = [1] x1 + [0] p(sum#) = [0] p(c_1) = [1] p(c_2) = [2] p(c_3) = [0] p(c_4) = [1] x1 + [1] x3 + [0] p(c_5) = [2] p(c_6) = [1] x1 + [1] x2 + [0] p(c_7) = [1] p(c_8) = [0] p(c_9) = [2] x1 + [8] p(c_10) = [0] p(c_11) = [1] x1 + [1] x2 + [0] p(c_12) = [1] x1 + [4] p(c_13) = [2] p(c_14) = [1] x2 + [0] p(c_15) = [0] p(c_16) = [2] Following rules are strictly oriented: prod#(cons(x,l)) = [1] l + [8] > [1] l + [4] = c_12(prod#(l)) Following rules are (at-least) weakly oriented: prod#(app(l1,l2)) = [10] l1 + [10] l2 + [0] >= [1] l1 + [1] l2 + [0] = c_11(prod#(l1),prod#(l2)) ***** Step 5.b:4.b:2.a:2.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) - Weak DPs: prod#(cons(x,l)) -> c_12(prod#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 5.b:4.b:2.a:2.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) - Weak DPs: prod#(cons(x,l)) -> c_12(prod#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) The strictly oriented rules are moved into the weak component. ****** Step 5.b:4.b:2.a:2.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) - Weak DPs: prod#(cons(x,l)) -> c_12(prod#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_11) = {1,2}, uargs(c_12) = {1} Following symbols are considered usable: {*#,+#,app#,prod#,sum#} TcT has computed the following interpretation: p(*) = [0] p(+) = [0] p(0) = [0] p(app) = [4] x1 + [1] x2 + [4] p(cons) = [1] x1 + [1] x2 + [1] p(nil) = [0] p(prod) = [1] x1 + [0] p(s) = [0] p(sum) = [0] p(*#) = [8] x1 + [8] x2 + [0] p(+#) = [1] x2 + [0] p(app#) = [2] x1 + [0] p(prod#) = [4] x1 + [0] p(sum#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [1] x1 + [2] x2 + [0] p(c_3) = [0] p(c_4) = [1] x1 + [1] x3 + [0] p(c_5) = [0] p(c_6) = [2] x2 + [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [1] x1 + [1] p(c_10) = [1] p(c_11) = [1] x1 + [1] x2 + [8] p(c_12) = [1] x1 + [4] p(c_13) = [2] p(c_14) = [4] x2 + [0] p(c_15) = [1] x1 + [0] p(c_16) = [0] Following rules are strictly oriented: prod#(app(l1,l2)) = [16] l1 + [4] l2 + [16] > [4] l1 + [4] l2 + [8] = c_11(prod#(l1),prod#(l2)) Following rules are (at-least) weakly oriented: prod#(cons(x,l)) = [4] l + [4] x + [4] >= [4] l + [4] = c_12(prod#(l)) ****** Step 5.b:4.b:2.a:2.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ****** Step 5.b:4.b:2.a:2.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) -->_2 prod#(cons(x,l)) -> c_12(prod#(l)):2 -->_1 prod#(cons(x,l)) -> c_12(prod#(l)):2 -->_2 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):1 -->_1 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):1 2:W:prod#(cons(x,l)) -> c_12(prod#(l)) -->_1 prod#(cons(x,l)) -> c_12(prod#(l)):2 -->_1 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) 2: prod#(cons(x,l)) -> c_12(prod#(l)) ****** Step 5.b:4.b:2.a:2.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). **** Step 5.b:4.b:2.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Weak DPs: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_12(prod#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) -->_2 sum#(cons(x,l)) -> c_15(sum#(l)):2 -->_1 sum#(cons(x,l)) -> c_15(sum#(l)):2 -->_2 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):1 -->_1 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):1 2:S:sum#(cons(x,l)) -> c_15(sum#(l)) -->_1 sum#(cons(x,l)) -> c_15(sum#(l)):2 -->_1 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):1 3:W:prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) -->_2 prod#(cons(x,l)) -> c_12(prod#(l)):4 -->_1 prod#(cons(x,l)) -> c_12(prod#(l)):4 -->_2 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):3 -->_1 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):3 4:W:prod#(cons(x,l)) -> c_12(prod#(l)) -->_1 prod#(cons(x,l)) -> c_12(prod#(l)):4 -->_1 prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: prod#(app(l1,l2)) -> c_11(prod#(l1),prod#(l2)) 4: prod#(cons(x,l)) -> c_12(prod#(l)) **** Step 5.b:4.b:2.b:2: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) 2: sum#(cons(x,l)) -> c_15(sum#(l)) The strictly oriented rules are moved into the weak component. ***** Step 5.b:4.b:2.b:2.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_14) = {1,2}, uargs(c_15) = {1} Following symbols are considered usable: {*#,+#,app#,prod#,sum#} TcT has computed the following interpretation: p(*) = [2] x2 + [1] p(+) = [1] x2 + [1] p(0) = [2] p(app) = [6] x1 + [2] x2 + [4] p(cons) = [1] x2 + [8] p(nil) = [0] p(prod) = [8] p(s) = [0] p(sum) = [0] p(*#) = [2] x1 + [1] x2 + [4] p(+#) = [1] x1 + [0] p(app#) = [2] x1 + [4] x2 + [0] p(prod#) = [2] x1 + [1] p(sum#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [8] p(c_4) = [2] x1 + [2] p(c_5) = [0] p(c_6) = [2] x1 + [1] x2 + [0] p(c_7) = [4] p(c_8) = [1] x1 + [0] p(c_9) = [8] p(c_10) = [1] p(c_11) = [8] x1 + [0] p(c_12) = [1] x1 + [8] p(c_13) = [8] p(c_14) = [4] x1 + [1] x2 + [3] p(c_15) = [1] x1 + [3] p(c_16) = [2] Following rules are strictly oriented: sum#(app(l1,l2)) = [6] l1 + [2] l2 + [4] > [4] l1 + [1] l2 + [3] = c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) = [1] l + [8] > [1] l + [3] = c_15(sum#(l)) Following rules are (at-least) weakly oriented: ***** Step 5.b:4.b:2.b:2.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 5.b:4.b:2.b:2.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_15(sum#(l)) - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) -->_2 sum#(cons(x,l)) -> c_15(sum#(l)):2 -->_1 sum#(cons(x,l)) -> c_15(sum#(l)):2 -->_2 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):1 -->_1 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):1 2:W:sum#(cons(x,l)) -> c_15(sum#(l)) -->_1 sum#(cons(x,l)) -> c_15(sum#(l)):2 -->_1 sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: sum#(app(l1,l2)) -> c_14(sum#(l1),sum#(l2)) 2: sum#(cons(x,l)) -> c_15(sum#(l)) ***** Step 5.b:4.b:2.b:2.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {*/2,+/2,app/2,prod/1,sum/1,*#/2,+#/2,app#/2,prod#/1,sum#/1} / {0/0,cons/2,nil/0,s/1,c_1/0,c_2/2,c_3/0,c_4/3 ,c_5/0,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,app#,prod#,sum#} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). MAYBE