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: NaturalMI 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: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {1}, uargs(c_10) = {1}, uargs(c_12) = {1}, uargs(c_14) = {1,2}, uargs(c_15) = {1}, uargs(c_20) = {1}, uargs(c_23) = {1}, uargs(c_24) = {1}, uargs(c_25) = {1,2}, uargs(c_28) = {1,2} Following symbols are considered usable: {gen,generate,if,isZero,a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil#,isZero#,p#,sum#,sum2#,tail# ,times#} TcT has computed the following interpretation: p(0) = [0] p(a) = [0] p(c) = [0] p(cons) = [0] p(d) = [0] p(error) = [0] p(false) = [0] p(ge) = [0] p(gen) = [1] x3 + [0] p(generate) = [0] p(head) = [2] p(if) = [1] x4 + [0] p(ifsum) = [1] x1 + [1] x3 + [4] x4 + [1] p(ifsum2) = [2] x3 + [1] p(isNil) = [0] p(isZero) = [0] p(nil) = [0] p(p) = [1] x1 + [6] p(s) = [4] p(sum) = [0] p(sum2) = [1] x2 + [0] p(tail) = [1] x1 + [0] p(times) = [1] x2 + [1] p(true) = [0] p(a#) = [2] p(ge#) = [0] p(gen#) = [0] p(generate#) = [0] p(head#) = [1] x1 + [0] p(if#) = [0] p(ifsum#) = [0] p(ifsum2#) = [0] p(isNil#) = [0] p(isZero#) = [0] p(p#) = [0] p(sum#) = [4] x1 + [0] p(sum2#) = [0] p(tail#) = [4] x1 + [1] p(times#) = [1] x1 + [5] p(c_1) = [1] p(c_2) = [1] p(c_3) = [1] p(c_4) = [1] p(c_5) = [1] x1 + [0] p(c_6) = [2] x1 + [4] x2 + [0] p(c_7) = [4] x1 + [0] p(c_8) = [1] p(c_9) = [1] p(c_10) = [4] x1 + [0] p(c_11) = [1] p(c_12) = [2] x1 + [0] p(c_13) = [4] p(c_14) = [1] x1 + [2] x2 + [0] p(c_15) = [2] x1 + [0] p(c_16) = [1] p(c_17) = [0] p(c_18) = [4] p(c_19) = [1] p(c_20) = [1] x1 + [0] p(c_21) = [0] p(c_22) = [2] p(c_23) = [1] x1 + [0] p(c_24) = [1] x1 + [0] p(c_25) = [1] x1 + [1] x2 + [0] p(c_26) = [0] p(c_27) = [1] p(c_28) = [4] x1 + [1] x2 + [3] Following rules are strictly oriented: times#(x,y) = [1] x + [5] > [3] = c_28(sum#(generate(x,y)),generate#(x,y)) Following rules are (at-least) weakly oriented: ge#(s(x),s(y)) = [0] >= [0] = c_5(ge#(x,y)) gen#(x,y,z) = [0] >= [0] = c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) = [0] >= [0] = c_7(gen#(x,y,0())) if#(false(),x,y,z) = [0] >= [0] = c_10(gen#(x,y,s(z))) ifsum#(false(),b,xs,y) = [0] >= [0] = c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) = [0] >= [0] = c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) = [0] >= [0] = c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) = [0] >= [0] = c_20(isZero#(s(x))) p#(s(s(x))) = [0] >= [0] = c_23(p#(s(x))) sum#(xs) = [4] xs + [0] >= [0] = c_24(sum2#(xs,0())) sum2#(xs,y) = [0] >= [0] = c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) gen(x,y,z) = [1] z + [0] >= [1] z + [0] = if(ge(z,x),x,y,z) generate(x,y) = [0] >= [0] = gen(x,y,0()) if(false(),x,y,z) = [1] z + [0] >= [0] = cons(y,gen(x,y,s(z))) if(true(),x,y,z) = [1] z + [0] >= [0] = nil() isZero(0()) = [0] >= [0] = true() isZero(s(0())) = [0] >= [0] = false() isZero(s(s(x))) = [0] >= [0] = isZero(s(x)) * Step 7: NaturalMI 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))) - Weak DPs: 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: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {1}, uargs(c_10) = {1}, uargs(c_12) = {1}, uargs(c_14) = {1,2}, uargs(c_15) = {1}, uargs(c_20) = {1}, uargs(c_23) = {1}, uargs(c_24) = {1}, uargs(c_25) = {1,2}, uargs(c_28) = {1,2} Following symbols are considered usable: {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil#,isZero#,p#,sum#,sum2#,tail#,times#} TcT has computed the following interpretation: p(0) = [0] p(a) = [0] p(c) = [1] p(cons) = [0] p(d) = [4] p(error) = [1] p(false) = [0] p(ge) = [0] p(gen) = [4] x1 + [1] x2 + [2] x3 + [4] p(generate) = [1] x1 + [4] x2 + [0] p(head) = [2] x1 + [4] p(if) = [2] x3 + [4] x4 + [5] p(ifsum) = [4] x3 + [4] p(ifsum2) = [2] p(isNil) = [1] x1 + [4] p(isZero) = [0] p(nil) = [4] p(p) = [0] p(s) = [0] p(sum) = [0] p(sum2) = [1] p(tail) = [1] x1 + [5] p(times) = [1] p(true) = [0] p(a#) = [1] p(ge#) = [0] p(gen#) = [4] x1 + [1] x3 + [2] p(generate#) = [4] x1 + [4] p(head#) = [4] p(if#) = [4] x2 + [2] p(ifsum#) = [0] p(ifsum2#) = [0] p(isNil#) = [0] p(isZero#) = [0] p(p#) = [0] p(sum#) = [0] p(sum2#) = [0] p(tail#) = [2] p(times#) = [4] x1 + [6] p(c_1) = [0] p(c_2) = [1] p(c_3) = [1] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [4] x2 + [0] p(c_7) = [1] x1 + [1] p(c_8) = [0] p(c_9) = [1] p(c_10) = [1] x1 + [0] p(c_11) = [1] p(c_12) = [4] x1 + [0] p(c_13) = [4] p(c_14) = [2] x1 + [1] x2 + [0] p(c_15) = [2] x1 + [0] p(c_16) = [1] p(c_17) = [0] p(c_18) = [4] p(c_19) = [0] p(c_20) = [2] x1 + [0] p(c_21) = [1] p(c_22) = [4] p(c_23) = [1] x1 + [0] p(c_24) = [4] x1 + [0] p(c_25) = [4] x1 + [1] x2 + [0] p(c_26) = [2] p(c_27) = [0] p(c_28) = [2] x1 + [1] x2 + [0] Following rules are strictly oriented: generate#(x,y) = [4] x + [4] > [4] x + [3] = c_7(gen#(x,y,0())) Following rules are (at-least) weakly oriented: ge#(s(x),s(y)) = [0] >= [0] = c_5(ge#(x,y)) gen#(x,y,z) = [4] x + [1] z + [2] >= [4] x + [2] = c_6(if#(ge(z,x),x,y,z),ge#(z,x)) if#(false(),x,y,z) = [4] x + [2] >= [4] x + [2] = c_10(gen#(x,y,s(z))) ifsum#(false(),b,xs,y) = [0] >= [0] = c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) = [0] >= [0] = c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) = [0] >= [0] = c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) = [0] >= [0] = c_20(isZero#(s(x))) p#(s(s(x))) = [0] >= [0] = c_23(p#(s(x))) sum#(xs) = [0] >= [0] = c_24(sum2#(xs,0())) sum2#(xs,y) = [0] >= [0] = c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) = [4] x + [6] >= [4] x + [4] = c_28(sum#(generate(x,y)),generate#(x,y)) * Step 8: NaturalMI 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)) 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))) - 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/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: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {1}, uargs(c_10) = {1}, uargs(c_12) = {1}, uargs(c_14) = {1,2}, uargs(c_15) = {1}, uargs(c_20) = {1}, uargs(c_23) = {1}, uargs(c_24) = {1}, uargs(c_25) = {1,2}, uargs(c_28) = {1,2} Following symbols are considered usable: {a#,ge#,gen#,generate#,head#,if#,ifsum#,ifsum2#,isNil#,isZero#,p#,sum#,sum2#,tail#,times#} TcT has computed the following interpretation: p(0) = [3] p(a) = [0] p(c) = [0] p(cons) = [2] p(d) = [1] p(error) = [2] p(false) = [0] p(ge) = [4] x1 + [2] x2 + [0] p(gen) = [4] x2 + [3] x3 + [4] p(generate) = [4] x2 + [0] p(head) = [0] p(if) = [1] x1 + [5] x2 + [1] x3 + [7] x4 + [0] p(ifsum) = [1] x1 + [1] x2 + [1] x4 + [1] p(ifsum2) = [1] x2 + [1] x3 + [4] p(isNil) = [0] p(isZero) = [0] p(nil) = [4] p(p) = [1] p(s) = [1] p(sum) = [4] p(sum2) = [1] x1 + [1] x2 + [2] p(tail) = [2] p(times) = [1] x2 + [2] p(true) = [0] p(a#) = [1] p(ge#) = [0] p(gen#) = [0] p(generate#) = [1] x1 + [5] x2 + [0] p(head#) = [1] x1 + [1] p(if#) = [0] p(ifsum#) = [0] p(ifsum2#) = [0] p(isNil#) = [2] x1 + [0] p(isZero#) = [0] p(p#) = [0] p(sum#) = [5] p(sum2#) = [0] p(tail#) = [1] x1 + [2] p(times#) = [1] x1 + [5] x2 + [5] p(c_1) = [0] p(c_2) = [1] p(c_3) = [4] p(c_4) = [1] p(c_5) = [4] x1 + [0] p(c_6) = [4] x1 + [4] x2 + [0] p(c_7) = [4] x1 + [0] p(c_8) = [1] p(c_9) = [1] p(c_10) = [4] x1 + [0] p(c_11) = [0] p(c_12) = [2] x1 + [0] p(c_13) = [0] p(c_14) = [1] x1 + [2] x2 + [0] p(c_15) = [4] x1 + [0] p(c_16) = [2] p(c_17) = [1] p(c_18) = [1] p(c_19) = [0] p(c_20) = [1] x1 + [0] p(c_21) = [1] p(c_22) = [1] p(c_23) = [4] x1 + [0] p(c_24) = [4] x1 + [4] p(c_25) = [4] x1 + [1] x2 + [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [1] x1 + [1] x2 + [0] Following rules are strictly oriented: sum#(xs) = [5] > [4] = c_24(sum2#(xs,0())) Following rules are (at-least) weakly oriented: ge#(s(x),s(y)) = [0] >= [0] = c_5(ge#(x,y)) gen#(x,y,z) = [0] >= [0] = c_6(if#(ge(z,x),x,y,z),ge#(z,x)) generate#(x,y) = [1] x + [5] y + [0] >= [0] = c_7(gen#(x,y,0())) if#(false(),x,y,z) = [0] >= [0] = c_10(gen#(x,y,s(z))) ifsum#(false(),b,xs,y) = [0] >= [0] = c_12(ifsum2#(b,xs,y)) ifsum2#(false(),xs,y) = [0] >= [0] = c_14(sum2#(cons(p(head(xs)),tail(xs)),s(y)),p#(head(xs))) ifsum2#(true(),xs,y) = [0] >= [0] = c_15(sum2#(tail(xs),y)) isZero#(s(s(x))) = [0] >= [0] = c_20(isZero#(s(x))) p#(s(s(x))) = [0] >= [0] = c_23(p#(s(x))) sum2#(xs,y) = [0] >= [0] = c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) times#(x,y) = [1] x + [5] y + [5] >= [1] x + [5] y + [5] = c_28(sum#(generate(x,y)),generate#(x,y)) * Step 9: Failure 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)) 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))) sum2#(xs,y) -> c_25(ifsum#(isNil(xs),isZero(head(xs)),xs,y),isZero#(head(xs))) - Weak DPs: generate#(x,y) -> c_7(gen#(x,y,0())) sum#(xs) -> c_24(sum2#(xs,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/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: EmptyProcessor + Details: The problem is still open. MAYBE