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