MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(#(),x) -> #() *(*(x,y),z) -> *(x,*(y,z)) *(0(x),y) -> 0(*(x,y)) *(1(x),y) -> +(0(*(x,y)),y) +(x,#()) -> x +(#(),x) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#()))) 0(#()) -> #() 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()) -> 1(#()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0(#()) - Signature: {*/2,+/2,0/1,app/2,prod/1,sum/1} / {#/0,1/1,cons/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {*,+,0,app,prod,sum} and constructors {#,1,cons,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)) *#(#(),x) -> c_2() *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)) *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)) *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)) +#(x,#()) -> c_6() +#(#(),x) -> c_7() +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)) +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)) +#(0(x),1(y)) -> c_10(+#(x,y)) +#(1(x),0(y)) -> c_11(+#(x,y)) +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)) 0#(#()) -> c_13() app#(cons(x,l1),l2) -> c_14(app#(l1,l2)) app#(nil(),l) -> c_15() prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)) prod#(nil()) -> c_18() sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)) sum#(nil()) -> c_21(0#(#())) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)) *#(#(),x) -> c_2() *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)) *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)) *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)) +#(x,#()) -> c_6() +#(#(),x) -> c_7() +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)) +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)) +#(0(x),1(y)) -> c_10(+#(x,y)) +#(1(x),0(y)) -> c_11(+#(x,y)) +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)) 0#(#()) -> c_13() app#(cons(x,l1),l2) -> c_14(app#(l1,l2)) app#(nil(),l) -> c_15() prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)) prod#(nil()) -> c_18() sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)) sum#(nil()) -> c_21(0#(#())) - Weak TRS: *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(#(),x) -> #() *(*(x,y),z) -> *(x,*(y,z)) *(0(x),y) -> 0(*(x,y)) *(1(x),y) -> +(0(*(x,y)),y) +(x,#()) -> x +(#(),x) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#()))) 0(#()) -> #() 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()) -> 1(#()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0(#()) - Signature: {*/2,+/2,0/1,app/2,prod/1,sum/1,*#/2,+#/2,0#/1,app#/2,prod#/1,sum#/1} / {#/0,1/1,cons/2,nil/0,c_1/3,c_2/0 ,c_3/2,c_4/2,c_5/3,c_6/0,c_7/0,c_8/2,c_9/2,c_10/1,c_11/1,c_12/3,c_13/0,c_14/1,c_15/0,c_16/3,c_17/2,c_18/0 ,c_19/3,c_20/2,c_21/1} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,0#,app#,prod#,sum#} and constructors {#,1,cons,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(#(),x) -> #() *(*(x,y),z) -> *(x,*(y,z)) *(0(x),y) -> 0(*(x,y)) *(1(x),y) -> +(0(*(x,y)),y) +(x,#()) -> x +(#(),x) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#()))) 0(#()) -> #() prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> 1(#()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0(#()) *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)) *#(#(),x) -> c_2() *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)) *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)) *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)) +#(x,#()) -> c_6() +#(#(),x) -> c_7() +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)) +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)) +#(0(x),1(y)) -> c_10(+#(x,y)) +#(1(x),0(y)) -> c_11(+#(x,y)) +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)) 0#(#()) -> c_13() app#(cons(x,l1),l2) -> c_14(app#(l1,l2)) app#(nil(),l) -> c_15() prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)) prod#(nil()) -> c_18() sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)) sum#(nil()) -> c_21(0#(#())) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)) *#(#(),x) -> c_2() *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)) *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)) *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)) +#(x,#()) -> c_6() +#(#(),x) -> c_7() +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)) +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)) +#(0(x),1(y)) -> c_10(+#(x,y)) +#(1(x),0(y)) -> c_11(+#(x,y)) +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)) 0#(#()) -> c_13() app#(cons(x,l1),l2) -> c_14(app#(l1,l2)) app#(nil(),l) -> c_15() prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)) prod#(nil()) -> c_18() sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)) sum#(nil()) -> c_21(0#(#())) - Weak TRS: *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(#(),x) -> #() *(*(x,y),z) -> *(x,*(y,z)) *(0(x),y) -> 0(*(x,y)) *(1(x),y) -> +(0(*(x,y)),y) +(x,#()) -> x +(#(),x) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#()))) 0(#()) -> #() prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> 1(#()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0(#()) - Signature: {*/2,+/2,0/1,app/2,prod/1,sum/1,*#/2,+#/2,0#/1,app#/2,prod#/1,sum#/1} / {#/0,1/1,cons/2,nil/0,c_1/3,c_2/0 ,c_3/2,c_4/2,c_5/3,c_6/0,c_7/0,c_8/2,c_9/2,c_10/1,c_11/1,c_12/3,c_13/0,c_14/1,c_15/0,c_16/3,c_17/2,c_18/0 ,c_19/3,c_20/2,c_21/1} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,0#,app#,prod#,sum#} and constructors {#,1,cons,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,6,7,13,15,18} by application of Pre({2,6,7,13,15,18}) = {1,3,4,5,8,9,10,11,12,14,16,17,19,20,21}. Here rules are labelled as follows: 1: *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)) 2: *#(#(),x) -> c_2() 3: *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)) 4: *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)) 5: *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)) 6: +#(x,#()) -> c_6() 7: +#(#(),x) -> c_7() 8: +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)) 9: +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)) 10: +#(0(x),1(y)) -> c_10(+#(x,y)) 11: +#(1(x),0(y)) -> c_11(+#(x,y)) 12: +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)) 13: 0#(#()) -> c_13() 14: app#(cons(x,l1),l2) -> c_14(app#(l1,l2)) 15: app#(nil(),l) -> c_15() 16: prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) 17: prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)) 18: prod#(nil()) -> c_18() 19: sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) 20: sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)) 21: sum#(nil()) -> c_21(0#(#())) * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)) *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)) *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)) *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)) +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)) +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)) +#(0(x),1(y)) -> c_10(+#(x,y)) +#(1(x),0(y)) -> c_11(+#(x,y)) +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)) app#(cons(x,l1),l2) -> c_14(app#(l1,l2)) prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)) sum#(nil()) -> c_21(0#(#())) - Weak DPs: *#(#(),x) -> c_2() +#(x,#()) -> c_6() +#(#(),x) -> c_7() 0#(#()) -> c_13() app#(nil(),l) -> c_15() prod#(nil()) -> c_18() - Weak TRS: *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(#(),x) -> #() *(*(x,y),z) -> *(x,*(y,z)) *(0(x),y) -> 0(*(x,y)) *(1(x),y) -> +(0(*(x,y)),y) +(x,#()) -> x +(#(),x) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#()))) 0(#()) -> #() prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> 1(#()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0(#()) - Signature: {*/2,+/2,0/1,app/2,prod/1,sum/1,*#/2,+#/2,0#/1,app#/2,prod#/1,sum#/1} / {#/0,1/1,cons/2,nil/0,c_1/3,c_2/0 ,c_3/2,c_4/2,c_5/3,c_6/0,c_7/0,c_8/2,c_9/2,c_10/1,c_11/1,c_12/3,c_13/0,c_14/1,c_15/0,c_16/3,c_17/2,c_18/0 ,c_19/3,c_20/2,c_21/1} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,0#,app#,prod#,sum#} and constructors {#,1,cons,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {15} by application of Pre({15}) = {13,14}. Here rules are labelled as follows: 1: *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)) 2: *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)) 3: *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)) 4: *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)) 5: +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)) 6: +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)) 7: +#(0(x),1(y)) -> c_10(+#(x,y)) 8: +#(1(x),0(y)) -> c_11(+#(x,y)) 9: +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)) 10: app#(cons(x,l1),l2) -> c_14(app#(l1,l2)) 11: prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) 12: prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)) 13: sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) 14: sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)) 15: sum#(nil()) -> c_21(0#(#())) 16: *#(#(),x) -> c_2() 17: +#(x,#()) -> c_6() 18: +#(#(),x) -> c_7() 19: 0#(#()) -> c_13() 20: app#(nil(),l) -> c_15() 21: prod#(nil()) -> c_18() * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)) *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)) *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)) *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)) +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)) +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)) +#(0(x),1(y)) -> c_10(+#(x,y)) +#(1(x),0(y)) -> c_11(+#(x,y)) +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)) app#(cons(x,l1),l2) -> c_14(app#(l1,l2)) prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)) - Weak DPs: *#(#(),x) -> c_2() +#(x,#()) -> c_6() +#(#(),x) -> c_7() 0#(#()) -> c_13() app#(nil(),l) -> c_15() prod#(nil()) -> c_18() sum#(nil()) -> c_21(0#(#())) - Weak TRS: *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(#(),x) -> #() *(*(x,y),z) -> *(x,*(y,z)) *(0(x),y) -> 0(*(x,y)) *(1(x),y) -> +(0(*(x,y)),y) +(x,#()) -> x +(#(),x) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#()))) 0(#()) -> #() prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> 1(#()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0(#()) - Signature: {*/2,+/2,0/1,app/2,prod/1,sum/1,*#/2,+#/2,0#/1,app#/2,prod#/1,sum#/1} / {#/0,1/1,cons/2,nil/0,c_1/3,c_2/0 ,c_3/2,c_4/2,c_5/3,c_6/0,c_7/0,c_8/2,c_9/2,c_10/1,c_11/1,c_12/3,c_13/0,c_14/1,c_15/0,c_16/3,c_17/2,c_18/0 ,c_19/3,c_20/2,c_21/1} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,0#,app#,prod#,sum#} and constructors {#,1,cons,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:*#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)) -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 -->_3 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_2 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_3 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_2 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_3 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_2 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_1 +#(#(),x) -> c_7():17 -->_1 +#(x,#()) -> c_6():16 -->_3 *#(#(),x) -> c_2():15 -->_2 *#(#(),x) -> c_2():15 -->_3 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 -->_2 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 2:S:*#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)) -->_2 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_1 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_2 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_1 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_2 *#(#(),x) -> c_2():15 -->_1 *#(#(),x) -> c_2():15 -->_2 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_1 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_2 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 -->_1 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 3:S:*#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)) -->_2 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_1 0#(#()) -> c_13():18 -->_2 *#(#(),x) -> c_2():15 -->_2 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_2 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_2 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 4:S:*#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)) -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 -->_2 0#(#()) -> c_13():18 -->_1 +#(#(),x) -> c_7():17 -->_1 +#(x,#()) -> c_6():16 -->_3 *#(#(),x) -> c_2():15 -->_3 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_3 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_3 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_3 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 5:S:+#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)) -->_2 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_2 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_2 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_2 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_2 +#(#(),x) -> c_7():17 -->_1 +#(#(),x) -> c_7():17 -->_2 +#(x,#()) -> c_6():16 -->_1 +#(x,#()) -> c_6():16 -->_2 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 6:S:+#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)) -->_2 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_2 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_2 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 0#(#()) -> c_13():18 -->_2 +#(#(),x) -> c_7():17 -->_2 +#(x,#()) -> c_6():16 -->_2 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_2 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 7:S:+#(0(x),1(y)) -> c_10(+#(x,y)) -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(#(),x) -> c_7():17 -->_1 +#(x,#()) -> c_6():16 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 8:S:+#(1(x),0(y)) -> c_11(+#(x,y)) -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(#(),x) -> c_7():17 -->_1 +#(x,#()) -> c_6():16 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 9:S:+#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)) -->_1 0#(#()) -> c_13():18 -->_3 +#(#(),x) -> c_7():17 -->_2 +#(#(),x) -> c_7():17 -->_3 +#(x,#()) -> c_6():16 -->_3 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_2 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_3 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_3 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_2 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_3 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_3 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 -->_2 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 10:S:app#(cons(x,l1),l2) -> c_14(app#(l1,l2)) -->_1 app#(nil(),l) -> c_15():19 -->_1 app#(cons(x,l1),l2) -> c_14(app#(l1,l2)):10 11:S:prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) -->_3 prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)):12 -->_2 prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)):12 -->_3 prod#(nil()) -> c_18():20 -->_2 prod#(nil()) -> c_18():20 -->_1 *#(#(),x) -> c_2():15 -->_3 prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):11 -->_2 prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):11 -->_1 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_1 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_1 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_1 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 12:S:prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)) -->_2 prod#(nil()) -> c_18():20 -->_1 *#(#(),x) -> c_2():15 -->_2 prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)):12 -->_2 prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):11 -->_1 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_1 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_1 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_1 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 13:S:sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) -->_3 sum#(nil()) -> c_21(0#(#())):21 -->_2 sum#(nil()) -> c_21(0#(#())):21 -->_3 sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)):14 -->_2 sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)):14 -->_1 +#(#(),x) -> c_7():17 -->_1 +#(x,#()) -> c_6():16 -->_3 sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):13 -->_2 sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):13 -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 14:S:sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)) -->_2 sum#(nil()) -> c_21(0#(#())):21 -->_1 +#(#(),x) -> c_7():17 -->_1 +#(x,#()) -> c_6():16 -->_2 sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)):14 -->_2 sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):13 -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 15:W:*#(#(),x) -> c_2() 16:W:+#(x,#()) -> c_6() 17:W:+#(#(),x) -> c_7() 18:W:0#(#()) -> c_13() 19:W:app#(nil(),l) -> c_15() 20:W:prod#(nil()) -> c_18() 21:W:sum#(nil()) -> c_21(0#(#())) -->_1 0#(#()) -> c_13():18 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 21: sum#(nil()) -> c_21(0#(#())) 20: prod#(nil()) -> c_18() 19: app#(nil(),l) -> c_15() 15: *#(#(),x) -> c_2() 16: +#(x,#()) -> c_6() 17: +#(#(),x) -> c_7() 18: 0#(#()) -> c_13() * Step 6: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)) *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)) *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)) *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)) +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)) +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)) +#(0(x),1(y)) -> c_10(+#(x,y)) +#(1(x),0(y)) -> c_11(+#(x,y)) +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)) app#(cons(x,l1),l2) -> c_14(app#(l1,l2)) prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(#(),x) -> #() *(*(x,y),z) -> *(x,*(y,z)) *(0(x),y) -> 0(*(x,y)) *(1(x),y) -> +(0(*(x,y)),y) +(x,#()) -> x +(#(),x) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#()))) 0(#()) -> #() prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> 1(#()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0(#()) - Signature: {*/2,+/2,0/1,app/2,prod/1,sum/1,*#/2,+#/2,0#/1,app#/2,prod#/1,sum#/1} / {#/0,1/1,cons/2,nil/0,c_1/3,c_2/0 ,c_3/2,c_4/2,c_5/3,c_6/0,c_7/0,c_8/2,c_9/2,c_10/1,c_11/1,c_12/3,c_13/0,c_14/1,c_15/0,c_16/3,c_17/2,c_18/0 ,c_19/3,c_20/2,c_21/1} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,0#,app#,prod#,sum#} and constructors {#,1,cons,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:*#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)) -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 -->_3 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_2 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_3 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_2 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_3 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_2 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_3 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 -->_2 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 2:S:*#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)) -->_2 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_1 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_2 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_1 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_2 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_1 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_2 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 -->_1 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 3:S:*#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)) -->_2 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_2 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_2 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_2 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 4:S:*#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)) -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 -->_3 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_3 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_3 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_3 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 5:S:+#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)) -->_2 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_2 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_2 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_2 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_2 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 6:S:+#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)) -->_2 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_2 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_2 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_2 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_2 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 7:S:+#(0(x),1(y)) -> c_10(+#(x,y)) -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 8:S:+#(1(x),0(y)) -> c_11(+#(x,y)) -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 9:S:+#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)) -->_3 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_2 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_3 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_3 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_2 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_3 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_3 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 -->_2 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 10:S:app#(cons(x,l1),l2) -> c_14(app#(l1,l2)) -->_1 app#(cons(x,l1),l2) -> c_14(app#(l1,l2)):10 11:S:prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) -->_3 prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)):12 -->_2 prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)):12 -->_3 prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):11 -->_2 prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):11 -->_1 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_1 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_1 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_1 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 12:S:prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)) -->_2 prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)):12 -->_2 prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)):11 -->_1 *#(1(x),y) -> c_5(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):4 -->_1 *#(0(x),y) -> c_4(0#(*(x,y)),*#(x,y)):3 -->_1 *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)):2 -->_1 *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)):1 13:S:sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) -->_3 sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)):14 -->_2 sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)):14 -->_3 sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):13 -->_2 sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):13 -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 14:S:sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)) -->_2 sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)):14 -->_2 sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)):13 -->_1 +#(1(x),1(y)) -> c_12(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):9 -->_1 +#(1(x),0(y)) -> c_11(+#(x,y)):8 -->_1 +#(0(x),1(y)) -> c_10(+#(x,y)):7 -->_1 +#(0(x),0(y)) -> c_9(0#(+(x,y)),+#(x,y)):6 -->_1 +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)):5 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: *#(0(x),y) -> c_4(*#(x,y)) *#(1(x),y) -> c_5(+#(0(*(x,y)),y),*#(x,y)) +#(0(x),0(y)) -> c_9(+#(x,y)) +#(1(x),1(y)) -> c_12(+#(+(x,y),1(#())),+#(x,y)) * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: *#(x,+(y,z)) -> c_1(+#(*(x,y),*(x,z)),*#(x,y),*#(x,z)) *#(*(x,y),z) -> c_3(*#(x,*(y,z)),*#(y,z)) *#(0(x),y) -> c_4(*#(x,y)) *#(1(x),y) -> c_5(+#(0(*(x,y)),y),*#(x,y)) +#(+(x,y),z) -> c_8(+#(x,+(y,z)),+#(y,z)) +#(0(x),0(y)) -> c_9(+#(x,y)) +#(0(x),1(y)) -> c_10(+#(x,y)) +#(1(x),0(y)) -> c_11(+#(x,y)) +#(1(x),1(y)) -> c_12(+#(+(x,y),1(#())),+#(x,y)) app#(cons(x,l1),l2) -> c_14(app#(l1,l2)) prod#(app(l1,l2)) -> c_16(*#(prod(l1),prod(l2)),prod#(l1),prod#(l2)) prod#(cons(x,l)) -> c_17(*#(x,prod(l)),prod#(l)) sum#(app(l1,l2)) -> c_19(+#(sum(l1),sum(l2)),sum#(l1),sum#(l2)) sum#(cons(x,l)) -> c_20(+#(x,sum(l)),sum#(l)) - Weak TRS: *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(#(),x) -> #() *(*(x,y),z) -> *(x,*(y,z)) *(0(x),y) -> 0(*(x,y)) *(1(x),y) -> +(0(*(x,y)),y) +(x,#()) -> x +(#(),x) -> x +(+(x,y),z) -> +(x,+(y,z)) +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#()))) 0(#()) -> #() prod(app(l1,l2)) -> *(prod(l1),prod(l2)) prod(cons(x,l)) -> *(x,prod(l)) prod(nil()) -> 1(#()) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) sum(cons(x,l)) -> +(x,sum(l)) sum(nil()) -> 0(#()) - Signature: {*/2,+/2,0/1,app/2,prod/1,sum/1,*#/2,+#/2,0#/1,app#/2,prod#/1,sum#/1} / {#/0,1/1,cons/2,nil/0,c_1/3,c_2/0 ,c_3/2,c_4/1,c_5/2,c_6/0,c_7/0,c_8/2,c_9/1,c_10/1,c_11/1,c_12/2,c_13/0,c_14/1,c_15/0,c_16/3,c_17/2,c_18/0 ,c_19/3,c_20/2,c_21/1} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,0#,app#,prod#,sum#} and constructors {#,1,cons,nil} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE