MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: a() -> c() a() -> d() ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() ifsum(false(),b,xs,y) -> ifsum2(b,xs,y) ifsum(true(),b,xs,y) -> y ifsum2(false(),xs,y) -> sum2(cons(p(head(xs)),tail(xs)),s(y)) ifsum2(true(),xs,y) -> sum2(tail(xs),y) isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) sum(xs) -> sum2(xs,0()) sum2(xs,y) -> ifsum(isNil(xs),isZero(head(xs)),xs,y) tail(cons(x,xs)) -> xs tail(nil()) -> nil() times(x,y) -> sum(generate(x,y)) - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1 ,times/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {a,ge,gen,generate,head,if,ifsum,ifsum2,isNil,isZero,p,sum ,sum2,tail,times} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a#() -> c_1() a#() -> c_2() ge#(x,0()) -> c_3() ge#(0(),s(y)) -> c_4() ge#(s(x),s(y)) -> c_5(ge#(x,y)) gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) head#(cons(x,xs)) -> c_8() head#(nil()) -> c_9() if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) if#(true(),x,y,z) -> c_11() ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum#(true(),b,xs,y) -> c_13() ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs)),head#(xs),tail#(xs)) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y),tail#(xs)) isNil#(cons(x,xs)) -> c_16() isNil#(nil()) -> c_17() isZero#(0()) -> c_18() isZero#(s(0())) -> c_19() isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(0()) -> c_21() p#(s(0())) -> c_22() p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isNil#(xs),isZero#(head(xs)),head#(xs)) tail#(cons(x,xs)) -> c_26() tail#(nil()) -> c_27() times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: a#() -> c_1() a#() -> c_2() ge#(x,0()) -> c_3() ge#(0(),s(y)) -> c_4() ge#(s(x),s(y)) -> c_5(ge#(x,y)) gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) head#(cons(x,xs)) -> c_8() head#(nil()) -> c_9() if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) if#(true(),x,y,z) -> c_11() ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum#(true(),b,xs,y) -> c_13() ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs)),head#(xs),tail#(xs)) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y),tail#(xs)) isNil#(cons(x,xs)) -> c_16() isNil#(nil()) -> c_17() isZero#(0()) -> c_18() isZero#(s(0())) -> c_19() isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(0()) -> c_21() p#(s(0())) -> c_22() p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isNil#(xs),isZero#(head(xs)),head#(xs)) tail#(cons(x,xs)) -> c_26() tail#(nil()) -> c_27() times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak TRS: a() -> c() a() -> d() ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() ifsum(false(),b,xs,y) -> ifsum2(b,xs,y) ifsum(true(),b,xs,y) -> y ifsum2(false(),xs,y) -> sum2(cons(p(head(xs)),tail(xs)),s(y)) ifsum2(true(),xs,y) -> sum2(tail(xs),y) isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) sum(xs) -> sum2(xs,0()) sum2(xs,y) -> ifsum(isNil(xs),isZero(head(xs)),xs,y) tail(cons(x,xs)) -> xs tail(nil()) -> nil() times(x,y) -> sum(generate(x,y)) - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/2,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/4,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/4,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() a#() -> c_1() a#() -> c_2() ge#(x,0()) -> c_3() ge#(0(),s(y)) -> c_4() ge#(s(x),s(y)) -> c_5(ge#(x,y)) gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) head#(cons(x,xs)) -> c_8() head#(nil()) -> c_9() if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) if#(true(),x,y,z) -> c_11() ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum#(true(),b,xs,y) -> c_13() ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs)),head#(xs),tail#(xs)) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y),tail#(xs)) isNil#(cons(x,xs)) -> c_16() isNil#(nil()) -> c_17() isZero#(0()) -> c_18() isZero#(s(0())) -> c_19() isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(0()) -> c_21() p#(s(0())) -> c_22() p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isNil#(xs),isZero#(head(xs)),head#(xs)) tail#(cons(x,xs)) -> c_26() tail#(nil()) -> c_27() times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a#() -> c_1() a#() -> c_2() ge#(x,0()) -> c_3() ge#(0(),s(y)) -> c_4() ge#(s(x),s(y)) -> c_5(ge#(x,y)) gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) head#(cons(x,xs)) -> c_8() head#(nil()) -> c_9() if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) if#(true(),x,y,z) -> c_11() ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum#(true(),b,xs,y) -> c_13() ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs)),head#(xs),tail#(xs)) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y),tail#(xs)) isNil#(cons(x,xs)) -> c_16() isNil#(nil()) -> c_17() isZero#(0()) -> c_18() isZero#(s(0())) -> c_19() isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(0()) -> c_21() p#(s(0())) -> c_22() p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isNil#(xs),isZero#(head(xs)),head#(xs)) tail#(cons(x,xs)) -> c_26() tail#(nil()) -> c_27() times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/2,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/4,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/4,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,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,8,9,11,13,16,17,18,19,21,22,26,27} by application of Pre({1,2,3,4,8,9,11,13,16,17,18,19,21,22,26,27}) = {5,6,14,15,20,23,25}. Here rules are labelled as follows: 1: a#() -> c_1() 2: a#() -> c_2() 3: ge#(x,0()) -> c_3() 4: ge#(0(),s(y)) -> c_4() 5: ge#(s(x),s(y)) -> c_5(ge#(x,y)) 6: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) 7: generate#(x,y) -> c_7(gen#(x,y,0())) 8: head#(cons(x,xs)) -> c_8() 9: head#(nil()) -> c_9() 10: if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) 11: if#(true(),x,y,z) -> c_11() 12: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) 13: ifsum#(true(),b,xs,y) -> c_13() 14: ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs)),head#(xs),tail#(xs)) 15: ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y),tail#(xs)) 16: isNil#(cons(x,xs)) -> c_16() 17: isNil#(nil()) -> c_17() 18: isZero#(0()) -> c_18() 19: isZero#(s(0())) -> c_19() 20: isZero#(s(s(x))) -> c_20(isZero#(s(x))) 21: p#(0()) -> c_21() 22: p#(s(0())) -> c_22() 23: p#(s(s(x))) -> c_23(p#(s(x))) 24: sum#(xs) -> c_24(sum2#(xs,0())) 25: sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isNil#(xs),isZero#(head(xs)),head#(xs)) 26: tail#(cons(x,xs)) -> c_26() 27: tail#(nil()) -> c_27() 28: times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs)),head#(xs),tail#(xs)) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y),tail#(xs)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isNil#(xs),isZero#(head(xs)),head#(xs)) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak DPs: a#() -> c_1() a#() -> c_2() ge#(x,0()) -> c_3() ge#(0(),s(y)) -> c_4() head#(cons(x,xs)) -> c_8() head#(nil()) -> c_9() if#(true(),x,y,z) -> c_11() ifsum#(true(),b,xs,y) -> c_13() isNil#(cons(x,xs)) -> c_16() isNil#(nil()) -> c_17() isZero#(0()) -> c_18() isZero#(s(0())) -> c_19() p#(0()) -> c_21() p#(s(0())) -> c_22() tail#(cons(x,xs)) -> c_26() tail#(nil()) -> c_27() - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/2,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/4,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/4,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:ge#(s(x),s(y)) -> c_5(ge#(x,y)) -->_1 ge#(0(),s(y)) -> c_4():16 -->_1 ge#(x,0()) -> c_3():15 -->_1 ge#(s(x),s(y)) -> c_5(ge#(x,y)):1 2:S:gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) -->_1 if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))):4 -->_1 if#(true(),x,y,z) -> c_11():19 -->_2 ge#(0(),s(y)) -> c_4():16 -->_2 ge#(x,0()) -> c_3():15 -->_2 ge#(s(x),s(y)) -> c_5(ge#(x,y)):1 3:S:generate#(x,y) -> c_7(gen#(x,y,0())) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)):2 4:S:if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)):2 5:S:ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) -->_1 ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y),tail#(xs)):7 -->_1 ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)) ,p#(head(xs)) ,head#(xs) ,tail#(xs)):6 6:S:ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs)),head#(xs),tail#(xs)) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y) ,isNil#(xs) ,isZero#(head(xs)) ,head#(xs)):11 -->_2 p#(s(s(x))) -> c_23(p#(s(x))):9 -->_4 tail#(nil()) -> c_27():28 -->_4 tail#(cons(x,xs)) -> c_26():27 -->_2 p#(s(0())) -> c_22():26 -->_2 p#(0()) -> c_21():25 -->_3 head#(nil()) -> c_9():18 -->_3 head#(cons(x,xs)) -> c_8():17 7:S:ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y),tail#(xs)) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y) ,isNil#(xs) ,isZero#(head(xs)) ,head#(xs)):11 -->_2 tail#(nil()) -> c_27():28 -->_2 tail#(cons(x,xs)) -> c_26():27 8:S:isZero#(s(s(x))) -> c_20(isZero#(s(x))) -->_1 isZero#(s(0())) -> c_19():24 -->_1 isZero#(s(s(x))) -> c_20(isZero#(s(x))):8 9:S:p#(s(s(x))) -> c_23(p#(s(x))) -->_1 p#(s(0())) -> c_22():26 -->_1 p#(s(s(x))) -> c_23(p#(s(x))):9 10:S:sum#(xs) -> c_24(sum2#(xs,0())) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y) ,isNil#(xs) ,isZero#(head(xs)) ,head#(xs)):11 11:S:sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isNil#(xs),isZero#(head(xs)),head#(xs)) -->_3 isZero#(s(0())) -> c_19():24 -->_3 isZero#(0()) -> c_18():23 -->_2 isNil#(nil()) -> c_17():22 -->_2 isNil#(cons(x,xs)) -> c_16():21 -->_1 ifsum#(true(),b,xs,y) -> c_13():20 -->_4 head#(nil()) -> c_9():18 -->_4 head#(cons(x,xs)) -> c_8():17 -->_3 isZero#(s(s(x))) -> c_20(isZero#(s(x))):8 -->_1 ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)):5 12:S:times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) -->_1 sum#(xs) -> c_24(sum2#(xs,0())):10 -->_2 generate#(x,y) -> c_7(gen#(x,y,0())):3 13:W:a#() -> c_1() 14:W:a#() -> c_2() 15:W:ge#(x,0()) -> c_3() 16:W:ge#(0(),s(y)) -> c_4() 17:W:head#(cons(x,xs)) -> c_8() 18:W:head#(nil()) -> c_9() 19:W:if#(true(),x,y,z) -> c_11() 20:W:ifsum#(true(),b,xs,y) -> c_13() 21:W:isNil#(cons(x,xs)) -> c_16() 22:W:isNil#(nil()) -> c_17() 23:W:isZero#(0()) -> c_18() 24:W:isZero#(s(0())) -> c_19() 25:W:p#(0()) -> c_21() 26:W:p#(s(0())) -> c_22() 27:W:tail#(cons(x,xs)) -> c_26() 28:W:tail#(nil()) -> c_27() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 14: a#() -> c_2() 13: a#() -> c_1() 25: p#(0()) -> c_21() 26: p#(s(0())) -> c_22() 27: tail#(cons(x,xs)) -> c_26() 28: tail#(nil()) -> c_27() 17: head#(cons(x,xs)) -> c_8() 18: head#(nil()) -> c_9() 20: ifsum#(true(),b,xs,y) -> c_13() 21: isNil#(cons(x,xs)) -> c_16() 22: isNil#(nil()) -> c_17() 23: isZero#(0()) -> c_18() 24: isZero#(s(0())) -> c_19() 19: if#(true(),x,y,z) -> c_11() 15: ge#(x,0()) -> c_3() 16: ge#(0(),s(y)) -> c_4() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs)),head#(xs),tail#(xs)) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y),tail#(xs)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isNil#(xs),isZero#(head(xs)),head#(xs)) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/2,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/4,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/4,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:ge#(s(x),s(y)) -> c_5(ge#(x,y)) -->_1 ge#(s(x),s(y)) -> c_5(ge#(x,y)):1 2:S:gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) -->_1 if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))):4 -->_2 ge#(s(x),s(y)) -> c_5(ge#(x,y)):1 3:S:generate#(x,y) -> c_7(gen#(x,y,0())) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)):2 4:S:if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)):2 5:S:ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) -->_1 ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y),tail#(xs)):7 -->_1 ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)) ,p#(head(xs)) ,head#(xs) ,tail#(xs)):6 6:S:ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs)),head#(xs),tail#(xs)) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y) ,isNil#(xs) ,isZero#(head(xs)) ,head#(xs)):11 -->_2 p#(s(s(x))) -> c_23(p#(s(x))):9 7:S:ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y),tail#(xs)) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y) ,isNil#(xs) ,isZero#(head(xs)) ,head#(xs)):11 8:S:isZero#(s(s(x))) -> c_20(isZero#(s(x))) -->_1 isZero#(s(s(x))) -> c_20(isZero#(s(x))):8 9:S:p#(s(s(x))) -> c_23(p#(s(x))) -->_1 p#(s(s(x))) -> c_23(p#(s(x))):9 10:S:sum#(xs) -> c_24(sum2#(xs,0())) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y) ,isNil#(xs) ,isZero#(head(xs)) ,head#(xs)):11 11:S:sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isNil#(xs),isZero#(head(xs)),head#(xs)) -->_3 isZero#(s(s(x))) -> c_20(isZero#(s(x))):8 -->_1 ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)):5 12:S:times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) -->_1 sum#(xs) -> c_24(sum2#(xs,0())):10 -->_2 generate#(x,y) -> c_7(gen#(x,y,0())):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) * Step 6: Decompose MAYBE + Considered Problem: - Strict DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/2,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + 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: ge#(s(x),s(y)) -> c_5(ge#(x,y)) - Weak DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/2,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1 ,c_21/0,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} Problem (S) - Strict DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/2,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1 ,c_21/0,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} ** Step 6.a:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) - Weak DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/2,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:ge#(s(x),s(y)) -> c_5(ge#(x,y)) -->_1 ge#(s(x),s(y)) -> c_5(ge#(x,y)):1 2:W:gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) -->_2 ge#(s(x),s(y)) -> c_5(ge#(x,y)):1 -->_1 if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))):4 3:W:generate#(x,y) -> c_7(gen#(x,y,0())) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)):2 4:W:if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)):2 5:W:ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) -->_1 ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)):7 -->_1 ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))):6 6:W:ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):11 -->_2 p#(s(s(x))) -> c_23(p#(s(x))):9 7:W:ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):11 8:W:isZero#(s(s(x))) -> c_20(isZero#(s(x))) -->_1 isZero#(s(s(x))) -> c_20(isZero#(s(x))):8 9:W:p#(s(s(x))) -> c_23(p#(s(x))) -->_1 p#(s(s(x))) -> c_23(p#(s(x))):9 10:W:sum#(xs) -> c_24(sum2#(xs,0())) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):11 11:W:sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) -->_1 ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)):5 -->_2 isZero#(s(s(x))) -> c_20(isZero#(s(x))):8 12:W:times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) -->_2 generate#(x,y) -> c_7(gen#(x,y,0())):3 -->_1 sum#(xs) -> c_24(sum2#(xs,0())):10 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: sum#(xs) -> c_24(sum2#(xs,0())) 5: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) 11: sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) 7: ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) 6: ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) 9: p#(s(s(x))) -> c_23(p#(s(x))) 8: isZero#(s(s(x))) -> c_20(isZero#(s(x))) ** Step 6.a:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) - Weak DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/2,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:ge#(s(x),s(y)) -> c_5(ge#(x,y)) -->_1 ge#(s(x),s(y)) -> c_5(ge#(x,y)):1 2:W:gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) -->_2 ge#(s(x),s(y)) -> c_5(ge#(x,y)):1 -->_1 if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))):4 3:W:generate#(x,y) -> c_7(gen#(x,y,0())) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)):2 4:W:if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)):2 12:W:times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) -->_2 generate#(x,y) -> c_7(gen#(x,y,0())):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: times#(x,y) -> c_28(generate#(x,y)) ** Step 6.a:3: UsableRules MAYBE + Considered Problem: - Strict DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) - Weak DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) times#(x,y) -> c_28(generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/2,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) ge#(s(x),s(y)) -> c_5(ge#(x,y)) gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) times#(x,y) -> c_28(generate#(x,y)) ** Step 6.a:4: Failure MAYBE + Considered Problem: - Strict DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) - Weak DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) times#(x,y) -> c_28(generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/2,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. ** Step 6.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/2,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) -->_2 ge#(s(x),s(y)) -> c_5(ge#(x,y)):12 -->_1 if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))):3 2:S:generate#(x,y) -> c_7(gen#(x,y,0())) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)):1 3:S:if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)):1 4:S:ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) -->_1 ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)):6 -->_1 ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))):5 5:S:ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):10 -->_2 p#(s(s(x))) -> c_23(p#(s(x))):8 6:S:ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):10 7:S:isZero#(s(s(x))) -> c_20(isZero#(s(x))) -->_1 isZero#(s(s(x))) -> c_20(isZero#(s(x))):7 8:S:p#(s(s(x))) -> c_23(p#(s(x))) -->_1 p#(s(s(x))) -> c_23(p#(s(x))):8 9:S:sum#(xs) -> c_24(sum2#(xs,0())) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):10 10:S:sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) -->_2 isZero#(s(s(x))) -> c_20(isZero#(s(x))):7 -->_1 ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)):4 11:S:times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) -->_1 sum#(xs) -> c_24(sum2#(xs,0())):9 -->_2 generate#(x,y) -> c_7(gen#(x,y,0())):2 12:W:ge#(s(x),s(y)) -> c_5(ge#(x,y)) -->_1 ge#(s(x),s(y)) -> c_5(ge#(x,y)):12 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 12: ge#(s(x),s(y)) -> c_5(ge#(x,y)) ** Step 6.b:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/2,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)) -->_1 if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))):3 2:S:generate#(x,y) -> c_7(gen#(x,y,0())) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)):1 3:S:if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z),ge#(z,x)):1 4:S:ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) -->_1 ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)):6 -->_1 ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))):5 5:S:ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):10 -->_2 p#(s(s(x))) -> c_23(p#(s(x))):8 6:S:ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):10 7:S:isZero#(s(s(x))) -> c_20(isZero#(s(x))) -->_1 isZero#(s(s(x))) -> c_20(isZero#(s(x))):7 8:S:p#(s(s(x))) -> c_23(p#(s(x))) -->_1 p#(s(s(x))) -> c_23(p#(s(x))):8 9:S:sum#(xs) -> c_24(sum2#(xs,0())) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):10 10:S:sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) -->_2 isZero#(s(s(x))) -> c_20(isZero#(s(x))):7 -->_1 ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)):4 11:S:times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) -->_1 sum#(xs) -> c_24(sum2#(xs,0())):9 -->_2 generate#(x,y) -> c_7(gen#(x,y,0())):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) ** Step 6.b:3: Decompose MAYBE + Considered Problem: - Strict DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + 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: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) - Weak DPs: generate#(x,y) -> c_7(gen#(x,y,0())) ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1 ,c_21/0,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} Problem (S) - Strict DPs: generate#(x,y) -> c_7(gen#(x,y,0())) ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1 ,c_21/0,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} *** Step 6.b:3.a:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) - Weak DPs: generate#(x,y) -> c_7(gen#(x,y,0())) ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) -->_1 if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))):3 2:W:generate#(x,y) -> c_7(gen#(x,y,0())) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)):1 3:S:if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)):1 4:W:ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) -->_1 ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)):6 -->_1 ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))):5 5:W:ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):10 -->_2 p#(s(s(x))) -> c_23(p#(s(x))):8 6:W:ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):10 7:W:isZero#(s(s(x))) -> c_20(isZero#(s(x))) -->_1 isZero#(s(s(x))) -> c_20(isZero#(s(x))):7 8:W:p#(s(s(x))) -> c_23(p#(s(x))) -->_1 p#(s(s(x))) -> c_23(p#(s(x))):8 9:W:sum#(xs) -> c_24(sum2#(xs,0())) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):10 10:W:sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) -->_1 ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)):4 -->_2 isZero#(s(s(x))) -> c_20(isZero#(s(x))):7 11:W:times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) -->_2 generate#(x,y) -> c_7(gen#(x,y,0())):2 -->_1 sum#(xs) -> c_24(sum2#(xs,0())):9 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 9: sum#(xs) -> c_24(sum2#(xs,0())) 4: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) 10: sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) 6: ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) 5: ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) 8: p#(s(s(x))) -> c_23(p#(s(x))) 7: isZero#(s(s(x))) -> c_20(isZero#(s(x))) *** Step 6.b:3.a:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) - Weak DPs: generate#(x,y) -> c_7(gen#(x,y,0())) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) -->_1 if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))):3 2:W:generate#(x,y) -> c_7(gen#(x,y,0())) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)):1 3:S:if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)):1 11:W:times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) -->_2 generate#(x,y) -> c_7(gen#(x,y,0())):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: times#(x,y) -> c_28(generate#(x,y)) *** Step 6.b:3.a:3: UsableRules MAYBE + Considered Problem: - Strict DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) - Weak DPs: generate#(x,y) -> c_7(gen#(x,y,0())) times#(x,y) -> c_28(generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) times#(x,y) -> c_28(generate#(x,y)) *** Step 6.b:3.a:4: Failure MAYBE + Considered Problem: - Strict DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) - Weak DPs: generate#(x,y) -> c_7(gen#(x,y,0())) times#(x,y) -> c_28(generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. *** Step 6.b:3.b:1: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: generate#(x,y) -> c_7(gen#(x,y,0())) ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {9}. Here rules are labelled as follows: 1: generate#(x,y) -> c_7(gen#(x,y,0())) 2: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) 3: ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) 4: ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) 5: isZero#(s(s(x))) -> c_20(isZero#(s(x))) 6: p#(s(s(x))) -> c_23(p#(s(x))) 7: sum#(xs) -> c_24(sum2#(xs,0())) 8: sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) 9: times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) 10: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) 11: if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) *** Step 6.b:3.b:2: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak DPs: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) generate#(x,y) -> c_7(gen#(x,y,0())) if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) -->_1 ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)):3 -->_1 ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))):2 2:S:ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):7 -->_2 p#(s(s(x))) -> c_23(p#(s(x))):5 3:S:ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):7 4:S:isZero#(s(s(x))) -> c_20(isZero#(s(x))) -->_1 isZero#(s(s(x))) -> c_20(isZero#(s(x))):4 5:S:p#(s(s(x))) -> c_23(p#(s(x))) -->_1 p#(s(s(x))) -> c_23(p#(s(x))):5 6:S:sum#(xs) -> c_24(sum2#(xs,0())) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):7 7:S:sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) -->_2 isZero#(s(s(x))) -> c_20(isZero#(s(x))):4 -->_1 ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)):1 8:S:times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) -->_2 generate#(x,y) -> c_7(gen#(x,y,0())):10 -->_1 sum#(xs) -> c_24(sum2#(xs,0())):6 9:W:gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) -->_1 if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))):11 10:W:generate#(x,y) -> c_7(gen#(x,y,0())) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)):9 11:W:if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) -->_1 gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)):9 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: generate#(x,y) -> c_7(gen#(x,y,0())) 9: gen#(x,y,z) -> c_6(if#(ge(z,x),x,y,z)) 11: if#(false(),x,y,z) -> c_10(gen#(x,y,s(z))) *** Step 6.b:3.b:3: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) -->_1 ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)):3 -->_1 ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))):2 2:S:ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):7 -->_2 p#(s(s(x))) -> c_23(p#(s(x))):5 3:S:ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):7 4:S:isZero#(s(s(x))) -> c_20(isZero#(s(x))) -->_1 isZero#(s(s(x))) -> c_20(isZero#(s(x))):4 5:S:p#(s(s(x))) -> c_23(p#(s(x))) -->_1 p#(s(s(x))) -> c_23(p#(s(x))):5 6:S:sum#(xs) -> c_24(sum2#(xs,0())) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):7 7:S:sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) -->_2 isZero#(s(s(x))) -> c_20(isZero#(s(x))):4 -->_1 ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)):1 8:S:times#(x,y) -> c_28(sum#(generate(x,y)),generate#(x,y)) -->_1 sum#(xs) -> c_24(sum2#(xs,0())):6 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: times#(x,y) -> c_28(sum#(generate(x,y))) *** Step 6.b:3.b:4: Decompose MAYBE + Considered Problem: - Strict DPs: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y))) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + 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: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) - Weak DPs: sum#(xs) -> c_24(sum2#(xs,0())) times#(x,y) -> c_28(sum#(generate(x,y))) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1 ,c_21/0,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} Problem (S) - Strict DPs: sum#(xs) -> c_24(sum2#(xs,0())) times#(x,y) -> c_28(sum#(generate(x,y))) - Weak DPs: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1 ,c_21/0,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} **** Step 6.b:3.b:4.a:1: Failure MAYBE + Considered Problem: - Strict DPs: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) - Weak DPs: sum#(xs) -> c_24(sum2#(xs,0())) times#(x,y) -> c_28(sum#(generate(x,y))) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. **** Step 6.b:3.b:4.b:1: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: sum#(xs) -> c_24(sum2#(xs,0())) times#(x,y) -> c_28(sum#(generate(x,y))) - Weak DPs: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {2}. Here rules are labelled as follows: 1: sum#(xs) -> c_24(sum2#(xs,0())) 2: times#(x,y) -> c_28(sum#(generate(x,y))) 3: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) 4: ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) 5: ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) 6: isZero#(s(s(x))) -> c_20(isZero#(s(x))) 7: p#(s(s(x))) -> c_23(p#(s(x))) 8: sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) **** Step 6.b:3.b:4.b:2: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: times#(x,y) -> c_28(sum#(generate(x,y))) - Weak DPs: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {}. Here rules are labelled as follows: 1: times#(x,y) -> c_28(sum#(generate(x,y))) 2: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) 3: ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) 4: ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) 5: isZero#(s(s(x))) -> c_20(isZero#(s(x))) 6: p#(s(s(x))) -> c_23(p#(s(x))) 7: sum#(xs) -> c_24(sum2#(xs,0())) 8: sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) **** Step 6.b:3.b:4.b:3: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) -> c_20(isZero#(s(x))) p#(s(s(x))) -> c_23(p#(s(x))) sum#(xs) -> c_24(sum2#(xs,0())) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) -> c_28(sum#(generate(x,y))) - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) -->_1 ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)):3 -->_1 ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))):2 2:W:ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):7 -->_2 p#(s(s(x))) -> c_23(p#(s(x))):5 3:W:ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):7 4:W:isZero#(s(s(x))) -> c_20(isZero#(s(x))) -->_1 isZero#(s(s(x))) -> c_20(isZero#(s(x))):4 5:W:p#(s(s(x))) -> c_23(p#(s(x))) -->_1 p#(s(s(x))) -> c_23(p#(s(x))):5 6:W:sum#(xs) -> c_24(sum2#(xs,0())) -->_1 sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))):7 7:W:sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) -->_2 isZero#(s(s(x))) -> c_20(isZero#(s(x))):4 -->_1 ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)):1 8:W:times#(x,y) -> c_28(sum#(generate(x,y))) -->_1 sum#(xs) -> c_24(sum2#(xs,0())):6 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 8: times#(x,y) -> c_28(sum#(generate(x,y))) 6: sum#(xs) -> c_24(sum2#(xs,0())) 1: ifsum#(false(),b,xs,y) -> c_12(ifsum2#(b,xs,y)) 7: sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) 3: ifsum2#(true(),xs,y) -> c_15(sum2#(tail(xs),y)) 2: ifsum2#(false(),xs,y) -> c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) 5: p#(s(s(x))) -> c_23(p#(s(x))) 4: isZero#(s(s(x))) -> c_20(isZero#(s(x))) **** Step 6.b:3.b:4.b:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) gen(x,y,z) -> if(ge(z,x),x,y,z) generate(x,y) -> gen(x,y,0()) head(cons(x,xs)) -> x head(nil()) -> error() if(false(),x,y,z) -> cons(y,gen(x,y,s(z))) if(true(),x,y,z) -> nil() isNil(cons(x,xs)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(x))) -> isZero(s(x)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(x))) -> s(p(s(x))) tail(cons(x,xs)) -> xs tail(nil()) -> nil() - Signature: {a/0,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2 ,a#/0,ge#/2,gen#/3,generate#/2,head#/1,if#/4,ifsum#/4,ifsum2#/3,isNil#/1,isZero#/1,p#/1,sum#/1,sum2#/2 ,tail#/1,times#/2} / {0/0,c/0,cons/2,d/0,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1 ,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil# ,isZero#,p#,sum#,sum2#,tail#,times#} and constructors {0,c,cons,d,error,false,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). MAYBE