MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: a() -> b() a() -> c() div(x,y,0()) -> divisible(x,y) div(0(),y,s(z)) -> false() div(s(x),y,s(z)) -> div(x,y,z) divisible(0(),s(y)) -> true() divisible(s(x),s(y)) -> div(s(x),s(y),s(y)) ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) if(false(),x,y,z,u) -> if2(divisible(z,y),x,y,z,u) if(true(),x,y,z,u) -> z if2(false(),x,y,z,u) -> lcmIter(x,y,plus(x,z),u) if2(true(),x,y,z,u) -> z ifTimes(false(),x,y) -> plus(y,times(y,p(x))) ifTimes(true(),x,y) -> 0() lcm(x,y) -> lcmIter(x,y,0(),times(x,y)) lcmIter(x,y,z,u) -> if(or(ge(0(),x),ge(z,u)),x,y,z,u) or(false(),y) -> y or(true(),y) -> true() p(0()) -> s(s(0())) p(s(x)) -> x plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) times(x,y) -> ifTimes(ge(0(),x),x,y) - Signature: {a/0,div/3,divisible/2,ge/2,if/5,if2/5,ifTimes/3,lcm/2,lcmIter/4,or/2,p/1,plus/2,times/2} / {0/0,b/0,c/0 ,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {a,div,divisible,ge,if,if2,ifTimes,lcm,lcmIter,or,p,plus ,times} and constructors {0,b,c,false,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a#() -> c_1() a#() -> c_2() div#(x,y,0()) -> c_3(divisible#(x,y)) div#(0(),y,s(z)) -> c_4() div#(s(x),y,s(z)) -> c_5(div#(x,y,z)) divisible#(0(),s(y)) -> c_6() divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))) ge#(x,0()) -> c_8() ge#(0(),s(y)) -> c_9() ge#(s(x),s(y)) -> c_10(ge#(x,y)) if#(false(),x,y,z,u) -> c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)) if#(true(),x,y,z,u) -> c_12() if2#(false(),x,y,z,u) -> c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)) if2#(true(),x,y,z,u) -> c_14() ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x)),p#(x)) ifTimes#(true(),x,y) -> c_16() lcm#(x,y) -> c_17(lcmIter#(x,y,0(),times(x,y)),times#(x,y)) lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u),or#(ge(0(),x),ge(z,u)),ge#(0(),x),ge#(z,u)) or#(false(),y) -> c_19() or#(true(),y) -> c_20() p#(0()) -> c_21() p#(s(x)) -> c_22() plus#(0(),y) -> c_23() plus#(s(x),y) -> c_24(plus#(x,y)) times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y),ge#(0(),x)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: a#() -> c_1() a#() -> c_2() div#(x,y,0()) -> c_3(divisible#(x,y)) div#(0(),y,s(z)) -> c_4() div#(s(x),y,s(z)) -> c_5(div#(x,y,z)) divisible#(0(),s(y)) -> c_6() divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))) ge#(x,0()) -> c_8() ge#(0(),s(y)) -> c_9() ge#(s(x),s(y)) -> c_10(ge#(x,y)) if#(false(),x,y,z,u) -> c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)) if#(true(),x,y,z,u) -> c_12() if2#(false(),x,y,z,u) -> c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)) if2#(true(),x,y,z,u) -> c_14() ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x)),p#(x)) ifTimes#(true(),x,y) -> c_16() lcm#(x,y) -> c_17(lcmIter#(x,y,0(),times(x,y)),times#(x,y)) lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u),or#(ge(0(),x),ge(z,u)),ge#(0(),x),ge#(z,u)) or#(false(),y) -> c_19() or#(true(),y) -> c_20() p#(0()) -> c_21() p#(s(x)) -> c_22() plus#(0(),y) -> c_23() plus#(s(x),y) -> c_24(plus#(x,y)) times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y),ge#(0(),x)) - Weak TRS: a() -> b() a() -> c() div(x,y,0()) -> divisible(x,y) div(0(),y,s(z)) -> false() div(s(x),y,s(z)) -> div(x,y,z) divisible(0(),s(y)) -> true() divisible(s(x),s(y)) -> div(s(x),s(y),s(y)) ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) if(false(),x,y,z,u) -> if2(divisible(z,y),x,y,z,u) if(true(),x,y,z,u) -> z if2(false(),x,y,z,u) -> lcmIter(x,y,plus(x,z),u) if2(true(),x,y,z,u) -> z ifTimes(false(),x,y) -> plus(y,times(y,p(x))) ifTimes(true(),x,y) -> 0() lcm(x,y) -> lcmIter(x,y,0(),times(x,y)) lcmIter(x,y,z,u) -> if(or(ge(0(),x),ge(z,u)),x,y,z,u) or(false(),y) -> y or(true(),y) -> true() p(0()) -> s(s(0())) p(s(x)) -> x plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) times(x,y) -> ifTimes(ge(0(),x),x,y) - Signature: {a/0,div/3,divisible/2,ge/2,if/5,if2/5,ifTimes/3,lcm/2,lcmIter/4,or/2,p/1,plus/2,times/2,a#/0,div#/3 ,divisible#/2,ge#/2,if#/5,if2#/5,ifTimes#/3,lcm#/2,lcmIter#/4,or#/2,p#/1,plus#/2,times#/2} / {0/0,b/0,c/0 ,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0 ,c_15/3,c_16/0,c_17/2,c_18/4,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,div#,divisible#,ge#,if#,if2#,ifTimes#,lcm#,lcmIter# ,or#,p#,plus#,times#} and constructors {0,b,c,false,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: div(x,y,0()) -> divisible(x,y) div(0(),y,s(z)) -> false() div(s(x),y,s(z)) -> div(x,y,z) divisible(0(),s(y)) -> true() divisible(s(x),s(y)) -> div(s(x),s(y),s(y)) ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) ifTimes(false(),x,y) -> plus(y,times(y,p(x))) ifTimes(true(),x,y) -> 0() or(false(),y) -> y or(true(),y) -> true() p(0()) -> s(s(0())) p(s(x)) -> x plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) times(x,y) -> ifTimes(ge(0(),x),x,y) a#() -> c_1() a#() -> c_2() div#(x,y,0()) -> c_3(divisible#(x,y)) div#(0(),y,s(z)) -> c_4() div#(s(x),y,s(z)) -> c_5(div#(x,y,z)) divisible#(0(),s(y)) -> c_6() divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))) ge#(x,0()) -> c_8() ge#(0(),s(y)) -> c_9() ge#(s(x),s(y)) -> c_10(ge#(x,y)) if#(false(),x,y,z,u) -> c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)) if#(true(),x,y,z,u) -> c_12() if2#(false(),x,y,z,u) -> c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)) if2#(true(),x,y,z,u) -> c_14() ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x)),p#(x)) ifTimes#(true(),x,y) -> c_16() lcm#(x,y) -> c_17(lcmIter#(x,y,0(),times(x,y)),times#(x,y)) lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u),or#(ge(0(),x),ge(z,u)),ge#(0(),x),ge#(z,u)) or#(false(),y) -> c_19() or#(true(),y) -> c_20() p#(0()) -> c_21() p#(s(x)) -> c_22() plus#(0(),y) -> c_23() plus#(s(x),y) -> c_24(plus#(x,y)) times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y),ge#(0(),x)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a#() -> c_1() a#() -> c_2() div#(x,y,0()) -> c_3(divisible#(x,y)) div#(0(),y,s(z)) -> c_4() div#(s(x),y,s(z)) -> c_5(div#(x,y,z)) divisible#(0(),s(y)) -> c_6() divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))) ge#(x,0()) -> c_8() ge#(0(),s(y)) -> c_9() ge#(s(x),s(y)) -> c_10(ge#(x,y)) if#(false(),x,y,z,u) -> c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)) if#(true(),x,y,z,u) -> c_12() if2#(false(),x,y,z,u) -> c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)) if2#(true(),x,y,z,u) -> c_14() ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x)),p#(x)) ifTimes#(true(),x,y) -> c_16() lcm#(x,y) -> c_17(lcmIter#(x,y,0(),times(x,y)),times#(x,y)) lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u),or#(ge(0(),x),ge(z,u)),ge#(0(),x),ge#(z,u)) or#(false(),y) -> c_19() or#(true(),y) -> c_20() p#(0()) -> c_21() p#(s(x)) -> c_22() plus#(0(),y) -> c_23() plus#(s(x),y) -> c_24(plus#(x,y)) times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y),ge#(0(),x)) - Weak TRS: div(x,y,0()) -> divisible(x,y) div(0(),y,s(z)) -> false() div(s(x),y,s(z)) -> div(x,y,z) divisible(0(),s(y)) -> true() divisible(s(x),s(y)) -> div(s(x),s(y),s(y)) ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) ifTimes(false(),x,y) -> plus(y,times(y,p(x))) ifTimes(true(),x,y) -> 0() or(false(),y) -> y or(true(),y) -> true() p(0()) -> s(s(0())) p(s(x)) -> x plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) times(x,y) -> ifTimes(ge(0(),x),x,y) - Signature: {a/0,div/3,divisible/2,ge/2,if/5,if2/5,ifTimes/3,lcm/2,lcmIter/4,or/2,p/1,plus/2,times/2,a#/0,div#/3 ,divisible#/2,ge#/2,if#/5,if2#/5,ifTimes#/3,lcm#/2,lcmIter#/4,or#/2,p#/1,plus#/2,times#/2} / {0/0,b/0,c/0 ,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0 ,c_15/3,c_16/0,c_17/2,c_18/4,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,div#,divisible#,ge#,if#,if2#,ifTimes#,lcm#,lcmIter# ,or#,p#,plus#,times#} and constructors {0,b,c,false,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,4,6,8,9,12,14,16,19,20,21,22,23} by application of Pre({1,2,4,6,8,9,12,14,16,19,20,21,22,23}) = {3,5,10,11,13,15,18,24,25}. Here rules are labelled as follows: 1: a#() -> c_1() 2: a#() -> c_2() 3: div#(x,y,0()) -> c_3(divisible#(x,y)) 4: div#(0(),y,s(z)) -> c_4() 5: div#(s(x),y,s(z)) -> c_5(div#(x,y,z)) 6: divisible#(0(),s(y)) -> c_6() 7: divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))) 8: ge#(x,0()) -> c_8() 9: ge#(0(),s(y)) -> c_9() 10: ge#(s(x),s(y)) -> c_10(ge#(x,y)) 11: if#(false(),x,y,z,u) -> c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)) 12: if#(true(),x,y,z,u) -> c_12() 13: if2#(false(),x,y,z,u) -> c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)) 14: if2#(true(),x,y,z,u) -> c_14() 15: ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x)),p#(x)) 16: ifTimes#(true(),x,y) -> c_16() 17: lcm#(x,y) -> c_17(lcmIter#(x,y,0(),times(x,y)),times#(x,y)) 18: lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u),or#(ge(0(),x),ge(z,u)),ge#(0(),x),ge#(z,u)) 19: or#(false(),y) -> c_19() 20: or#(true(),y) -> c_20() 21: p#(0()) -> c_21() 22: p#(s(x)) -> c_22() 23: plus#(0(),y) -> c_23() 24: plus#(s(x),y) -> c_24(plus#(x,y)) 25: times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y),ge#(0(),x)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: div#(x,y,0()) -> c_3(divisible#(x,y)) div#(s(x),y,s(z)) -> c_5(div#(x,y,z)) divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))) ge#(s(x),s(y)) -> c_10(ge#(x,y)) if#(false(),x,y,z,u) -> c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)) if2#(false(),x,y,z,u) -> c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)) ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x)),p#(x)) lcm#(x,y) -> c_17(lcmIter#(x,y,0(),times(x,y)),times#(x,y)) lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u),or#(ge(0(),x),ge(z,u)),ge#(0(),x),ge#(z,u)) plus#(s(x),y) -> c_24(plus#(x,y)) times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y),ge#(0(),x)) - Weak DPs: a#() -> c_1() a#() -> c_2() div#(0(),y,s(z)) -> c_4() divisible#(0(),s(y)) -> c_6() ge#(x,0()) -> c_8() ge#(0(),s(y)) -> c_9() if#(true(),x,y,z,u) -> c_12() if2#(true(),x,y,z,u) -> c_14() ifTimes#(true(),x,y) -> c_16() or#(false(),y) -> c_19() or#(true(),y) -> c_20() p#(0()) -> c_21() p#(s(x)) -> c_22() plus#(0(),y) -> c_23() - Weak TRS: div(x,y,0()) -> divisible(x,y) div(0(),y,s(z)) -> false() div(s(x),y,s(z)) -> div(x,y,z) divisible(0(),s(y)) -> true() divisible(s(x),s(y)) -> div(s(x),s(y),s(y)) ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) ifTimes(false(),x,y) -> plus(y,times(y,p(x))) ifTimes(true(),x,y) -> 0() or(false(),y) -> y or(true(),y) -> true() p(0()) -> s(s(0())) p(s(x)) -> x plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) times(x,y) -> ifTimes(ge(0(),x),x,y) - Signature: {a/0,div/3,divisible/2,ge/2,if/5,if2/5,ifTimes/3,lcm/2,lcmIter/4,or/2,p/1,plus/2,times/2,a#/0,div#/3 ,divisible#/2,ge#/2,if#/5,if2#/5,ifTimes#/3,lcm#/2,lcmIter#/4,or#/2,p#/1,plus#/2,times#/2} / {0/0,b/0,c/0 ,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0 ,c_15/3,c_16/0,c_17/2,c_18/4,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,div#,divisible#,ge#,if#,if2#,ifTimes#,lcm#,lcmIter# ,or#,p#,plus#,times#} and constructors {0,b,c,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:div#(x,y,0()) -> c_3(divisible#(x,y)) -->_1 divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))):3 -->_1 divisible#(0(),s(y)) -> c_6():15 2:S:div#(s(x),y,s(z)) -> c_5(div#(x,y,z)) -->_1 div#(0(),y,s(z)) -> c_4():14 -->_1 div#(s(x),y,s(z)) -> c_5(div#(x,y,z)):2 -->_1 div#(x,y,0()) -> c_3(divisible#(x,y)):1 3:S:divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))) -->_1 div#(s(x),y,s(z)) -> c_5(div#(x,y,z)):2 4:S:ge#(s(x),s(y)) -> c_10(ge#(x,y)) -->_1 ge#(0(),s(y)) -> c_9():17 -->_1 ge#(x,0()) -> c_8():16 -->_1 ge#(s(x),s(y)) -> c_10(ge#(x,y)):4 5:S:if#(false(),x,y,z,u) -> c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)) -->_1 if2#(false(),x,y,z,u) -> c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)):6 -->_1 if2#(true(),x,y,z,u) -> c_14():19 -->_2 divisible#(0(),s(y)) -> c_6():15 -->_2 divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))):3 6:S:if2#(false(),x,y,z,u) -> c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)) -->_2 plus#(s(x),y) -> c_24(plus#(x,y)):10 -->_1 lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u) ,or#(ge(0(),x),ge(z,u)) ,ge#(0(),x) ,ge#(z,u)):9 -->_2 plus#(0(),y) -> c_23():25 7:S:ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x)),p#(x)) -->_2 times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y),ge#(0(),x)):11 -->_1 plus#(s(x),y) -> c_24(plus#(x,y)):10 -->_1 plus#(0(),y) -> c_23():25 -->_3 p#(s(x)) -> c_22():24 -->_3 p#(0()) -> c_21():23 8:S:lcm#(x,y) -> c_17(lcmIter#(x,y,0(),times(x,y)),times#(x,y)) -->_2 times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y),ge#(0(),x)):11 -->_1 lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u) ,or#(ge(0(),x),ge(z,u)) ,ge#(0(),x) ,ge#(z,u)):9 9:S:lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u),or#(ge(0(),x),ge(z,u)),ge#(0(),x),ge#(z,u)) -->_2 or#(true(),y) -> c_20():22 -->_2 or#(false(),y) -> c_19():21 -->_1 if#(true(),x,y,z,u) -> c_12():18 -->_4 ge#(0(),s(y)) -> c_9():17 -->_3 ge#(0(),s(y)) -> c_9():17 -->_4 ge#(x,0()) -> c_8():16 -->_3 ge#(x,0()) -> c_8():16 -->_1 if#(false(),x,y,z,u) -> c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)):5 -->_4 ge#(s(x),s(y)) -> c_10(ge#(x,y)):4 10:S:plus#(s(x),y) -> c_24(plus#(x,y)) -->_1 plus#(0(),y) -> c_23():25 -->_1 plus#(s(x),y) -> c_24(plus#(x,y)):10 11:S:times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y),ge#(0(),x)) -->_1 ifTimes#(true(),x,y) -> c_16():20 -->_2 ge#(0(),s(y)) -> c_9():17 -->_2 ge#(x,0()) -> c_8():16 -->_1 ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x)),p#(x)):7 12:W:a#() -> c_1() 13:W:a#() -> c_2() 14:W:div#(0(),y,s(z)) -> c_4() 15:W:divisible#(0(),s(y)) -> c_6() 16:W:ge#(x,0()) -> c_8() 17:W:ge#(0(),s(y)) -> c_9() 18:W:if#(true(),x,y,z,u) -> c_12() 19:W:if2#(true(),x,y,z,u) -> c_14() 20:W:ifTimes#(true(),x,y) -> c_16() 21:W:or#(false(),y) -> c_19() 22:W:or#(true(),y) -> c_20() 23:W:p#(0()) -> c_21() 24:W:p#(s(x)) -> c_22() 25:W:plus#(0(),y) -> c_23() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 13: a#() -> c_2() 12: a#() -> c_1() 23: p#(0()) -> c_21() 24: p#(s(x)) -> c_22() 20: ifTimes#(true(),x,y) -> c_16() 19: if2#(true(),x,y,z,u) -> c_14() 18: if#(true(),x,y,z,u) -> c_12() 21: or#(false(),y) -> c_19() 22: or#(true(),y) -> c_20() 25: plus#(0(),y) -> c_23() 16: ge#(x,0()) -> c_8() 17: ge#(0(),s(y)) -> c_9() 15: divisible#(0(),s(y)) -> c_6() 14: div#(0(),y,s(z)) -> c_4() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: div#(x,y,0()) -> c_3(divisible#(x,y)) div#(s(x),y,s(z)) -> c_5(div#(x,y,z)) divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))) ge#(s(x),s(y)) -> c_10(ge#(x,y)) if#(false(),x,y,z,u) -> c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)) if2#(false(),x,y,z,u) -> c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)) ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x)),p#(x)) lcm#(x,y) -> c_17(lcmIter#(x,y,0(),times(x,y)),times#(x,y)) lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u),or#(ge(0(),x),ge(z,u)),ge#(0(),x),ge#(z,u)) plus#(s(x),y) -> c_24(plus#(x,y)) times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y),ge#(0(),x)) - Weak TRS: div(x,y,0()) -> divisible(x,y) div(0(),y,s(z)) -> false() div(s(x),y,s(z)) -> div(x,y,z) divisible(0(),s(y)) -> true() divisible(s(x),s(y)) -> div(s(x),s(y),s(y)) ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) ifTimes(false(),x,y) -> plus(y,times(y,p(x))) ifTimes(true(),x,y) -> 0() or(false(),y) -> y or(true(),y) -> true() p(0()) -> s(s(0())) p(s(x)) -> x plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) times(x,y) -> ifTimes(ge(0(),x),x,y) - Signature: {a/0,div/3,divisible/2,ge/2,if/5,if2/5,ifTimes/3,lcm/2,lcmIter/4,or/2,p/1,plus/2,times/2,a#/0,div#/3 ,divisible#/2,ge#/2,if#/5,if2#/5,ifTimes#/3,lcm#/2,lcmIter#/4,or#/2,p#/1,plus#/2,times#/2} / {0/0,b/0,c/0 ,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0 ,c_15/3,c_16/0,c_17/2,c_18/4,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,div#,divisible#,ge#,if#,if2#,ifTimes#,lcm#,lcmIter# ,or#,p#,plus#,times#} and constructors {0,b,c,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:div#(x,y,0()) -> c_3(divisible#(x,y)) -->_1 divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))):3 2:S:div#(s(x),y,s(z)) -> c_5(div#(x,y,z)) -->_1 div#(s(x),y,s(z)) -> c_5(div#(x,y,z)):2 -->_1 div#(x,y,0()) -> c_3(divisible#(x,y)):1 3:S:divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))) -->_1 div#(s(x),y,s(z)) -> c_5(div#(x,y,z)):2 4:S:ge#(s(x),s(y)) -> c_10(ge#(x,y)) -->_1 ge#(s(x),s(y)) -> c_10(ge#(x,y)):4 5:S:if#(false(),x,y,z,u) -> c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)) -->_1 if2#(false(),x,y,z,u) -> c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)):6 -->_2 divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))):3 6:S:if2#(false(),x,y,z,u) -> c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)) -->_2 plus#(s(x),y) -> c_24(plus#(x,y)):10 -->_1 lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u) ,or#(ge(0(),x),ge(z,u)) ,ge#(0(),x) ,ge#(z,u)):9 7:S:ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x)),p#(x)) -->_2 times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y),ge#(0(),x)):11 -->_1 plus#(s(x),y) -> c_24(plus#(x,y)):10 8:S:lcm#(x,y) -> c_17(lcmIter#(x,y,0(),times(x,y)),times#(x,y)) -->_2 times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y),ge#(0(),x)):11 -->_1 lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u) ,or#(ge(0(),x),ge(z,u)) ,ge#(0(),x) ,ge#(z,u)):9 9:S:lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u),or#(ge(0(),x),ge(z,u)),ge#(0(),x),ge#(z,u)) -->_1 if#(false(),x,y,z,u) -> c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)):5 -->_4 ge#(s(x),s(y)) -> c_10(ge#(x,y)):4 10:S:plus#(s(x),y) -> c_24(plus#(x,y)) -->_1 plus#(s(x),y) -> c_24(plus#(x,y)):10 11:S:times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y),ge#(0(),x)) -->_1 ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x)),p#(x)):7 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x))) lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u),ge#(z,u)) times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y)) * Step 6: NaturalMI MAYBE + Considered Problem: - Strict DPs: div#(x,y,0()) -> c_3(divisible#(x,y)) div#(s(x),y,s(z)) -> c_5(div#(x,y,z)) divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))) ge#(s(x),s(y)) -> c_10(ge#(x,y)) if#(false(),x,y,z,u) -> c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)) if2#(false(),x,y,z,u) -> c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)) ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x))) lcm#(x,y) -> c_17(lcmIter#(x,y,0(),times(x,y)),times#(x,y)) lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u),ge#(z,u)) plus#(s(x),y) -> c_24(plus#(x,y)) times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y)) - Weak TRS: div(x,y,0()) -> divisible(x,y) div(0(),y,s(z)) -> false() div(s(x),y,s(z)) -> div(x,y,z) divisible(0(),s(y)) -> true() divisible(s(x),s(y)) -> div(s(x),s(y),s(y)) ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) ifTimes(false(),x,y) -> plus(y,times(y,p(x))) ifTimes(true(),x,y) -> 0() or(false(),y) -> y or(true(),y) -> true() p(0()) -> s(s(0())) p(s(x)) -> x plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) times(x,y) -> ifTimes(ge(0(),x),x,y) - Signature: {a/0,div/3,divisible/2,ge/2,if/5,if2/5,ifTimes/3,lcm/2,lcmIter/4,or/2,p/1,plus/2,times/2,a#/0,div#/3 ,divisible#/2,ge#/2,if#/5,if2#/5,ifTimes#/3,lcm#/2,lcmIter#/4,or#/2,p#/1,plus#/2,times#/2} / {0/0,b/0,c/0 ,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0 ,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,div#,divisible#,ge#,if#,if2#,ifTimes#,lcm#,lcmIter# ,or#,p#,plus#,times#} and constructors {0,b,c,false,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_3) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1,2}, uargs(c_13) = {1,2}, uargs(c_15) = {1,2}, uargs(c_17) = {1,2}, uargs(c_18) = {1,2}, uargs(c_24) = {1}, uargs(c_25) = {1} Following symbols are considered usable: {a#,div#,divisible#,ge#,if#,if2#,ifTimes#,lcm#,lcmIter#,or#,p#,plus#,times#} TcT has computed the following interpretation: p(0) = [6] p(a) = [0] p(b) = [0] p(c) = [0] p(div) = [1] x1 + [7] p(divisible) = [0] p(false) = [0] p(ge) = [3] p(if) = [2] x3 + [1] p(if2) = [1] x1 + [1] x2 + [4] x3 + [1] x5 + [1] p(ifTimes) = [3] x1 + [1] x3 + [0] p(lcm) = [0] p(lcmIter) = [2] x1 + [1] p(or) = [5] x2 + [0] p(p) = [0] p(plus) = [2] x2 + [1] p(s) = [0] p(times) = [2] x1 + [1] p(true) = [3] p(a#) = [0] p(div#) = [0] p(divisible#) = [0] p(ge#) = [0] p(if#) = [0] p(if2#) = [0] p(ifTimes#) = [0] p(lcm#) = [1] x1 + [2] p(lcmIter#) = [0] p(or#) = [1] p(p#) = [2] x1 + [2] p(plus#) = [0] p(times#) = [0] p(c_1) = [0] p(c_2) = [4] p(c_3) = [4] x1 + [0] p(c_4) = [0] p(c_5) = [4] x1 + [0] p(c_6) = [1] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [1] p(c_10) = [1] x1 + [0] p(c_11) = [1] x1 + [4] x2 + [0] p(c_12) = [0] p(c_13) = [4] x1 + [4] x2 + [0] p(c_14) = [1] p(c_15) = [1] x1 + [4] x2 + [0] p(c_16) = [1] p(c_17) = [2] x1 + [4] x2 + [0] p(c_18) = [2] x1 + [4] x2 + [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [2] p(c_22) = [0] p(c_23) = [1] p(c_24) = [2] x1 + [0] p(c_25) = [1] x1 + [0] Following rules are strictly oriented: lcm#(x,y) = [1] x + [2] > [0] = c_17(lcmIter#(x,y,0(),times(x,y)),times#(x,y)) Following rules are (at-least) weakly oriented: div#(x,y,0()) = [0] >= [0] = c_3(divisible#(x,y)) div#(s(x),y,s(z)) = [0] >= [0] = c_5(div#(x,y,z)) divisible#(s(x),s(y)) = [0] >= [0] = c_7(div#(s(x),s(y),s(y))) ge#(s(x),s(y)) = [0] >= [0] = c_10(ge#(x,y)) if#(false(),x,y,z,u) = [0] >= [0] = c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)) if2#(false(),x,y,z,u) = [0] >= [0] = c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)) ifTimes#(false(),x,y) = [0] >= [0] = c_15(plus#(y,times(y,p(x))),times#(y,p(x))) lcmIter#(x,y,z,u) = [0] >= [0] = c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u),ge#(z,u)) plus#(s(x),y) = [0] >= [0] = c_24(plus#(x,y)) times#(x,y) = [0] >= [0] = c_25(ifTimes#(ge(0(),x),x,y)) * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: div#(x,y,0()) -> c_3(divisible#(x,y)) div#(s(x),y,s(z)) -> c_5(div#(x,y,z)) divisible#(s(x),s(y)) -> c_7(div#(s(x),s(y),s(y))) ge#(s(x),s(y)) -> c_10(ge#(x,y)) if#(false(),x,y,z,u) -> c_11(if2#(divisible(z,y),x,y,z,u),divisible#(z,y)) if2#(false(),x,y,z,u) -> c_13(lcmIter#(x,y,plus(x,z),u),plus#(x,z)) ifTimes#(false(),x,y) -> c_15(plus#(y,times(y,p(x))),times#(y,p(x))) lcmIter#(x,y,z,u) -> c_18(if#(or(ge(0(),x),ge(z,u)),x,y,z,u),ge#(z,u)) plus#(s(x),y) -> c_24(plus#(x,y)) times#(x,y) -> c_25(ifTimes#(ge(0(),x),x,y)) - Weak DPs: lcm#(x,y) -> c_17(lcmIter#(x,y,0(),times(x,y)),times#(x,y)) - Weak TRS: div(x,y,0()) -> divisible(x,y) div(0(),y,s(z)) -> false() div(s(x),y,s(z)) -> div(x,y,z) divisible(0(),s(y)) -> true() divisible(s(x),s(y)) -> div(s(x),s(y),s(y)) ge(x,0()) -> true() ge(0(),s(y)) -> false() ge(s(x),s(y)) -> ge(x,y) ifTimes(false(),x,y) -> plus(y,times(y,p(x))) ifTimes(true(),x,y) -> 0() or(false(),y) -> y or(true(),y) -> true() p(0()) -> s(s(0())) p(s(x)) -> x plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) times(x,y) -> ifTimes(ge(0(),x),x,y) - Signature: {a/0,div/3,divisible/2,ge/2,if/5,if2/5,ifTimes/3,lcm/2,lcmIter/4,or/2,p/1,plus/2,times/2,a#/0,div#/3 ,divisible#/2,ge#/2,if#/5,if2#/5,ifTimes#/3,lcm#/2,lcmIter#/4,or#/2,p#/1,plus#/2,times#/2} / {0/0,b/0,c/0 ,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0 ,c_15/2,c_16/0,c_17/2,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {a#,div#,divisible#,ge#,if#,if2#,ifTimes#,lcm#,lcmIter# ,or#,p#,plus#,times#} and constructors {0,b,c,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE