MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: div(x,y) -> quot(x,y,y) div(0(),y) -> 0() div(div(x,y),z) -> div(x,times(y,z)) divides(y,x) -> eq(x,times(div(x,y),y)) eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) if(false(),x,y) -> pr(x,y) if(true(),x,y) -> false() p(s(x)) -> x plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,p(s(y)))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(s(x),y) -> s(plus(p(s(x)),y)) pr(x,s(0())) -> true() pr(x,s(s(y))) -> if(divides(s(s(y)),x),x,s(y)) prime(s(s(x))) -> pr(s(s(x)),s(x)) quot(x,0(),s(z)) -> s(div(x,s(z))) quot(0(),s(y),z) -> 0() quot(s(x),s(y),z) -> quot(x,y,z) times(0(),y) -> 0() times(s(x),y) -> plus(y,times(x,y)) times(s(0()),y) -> y - Signature: {div/2,divides/2,eq/2,if/3,p/1,plus/2,pr/2,prime/1,quot/3,times/2} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div,divides,eq,if,p,plus,pr,prime,quot ,times} and constructors {0,false,s,true} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. div(div(x,y),z) -> div(x,times(y,z)) All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: div(x,y) -> quot(x,y,y) div(0(),y) -> 0() divides(y,x) -> eq(x,times(div(x,y),y)) eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) if(false(),x,y) -> pr(x,y) if(true(),x,y) -> false() p(s(x)) -> x plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,p(s(y)))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(s(x),y) -> s(plus(p(s(x)),y)) pr(x,s(0())) -> true() pr(x,s(s(y))) -> if(divides(s(s(y)),x),x,s(y)) prime(s(s(x))) -> pr(s(s(x)),s(x)) quot(x,0(),s(z)) -> s(div(x,s(z))) quot(0(),s(y),z) -> 0() quot(s(x),s(y),z) -> quot(x,y,z) times(0(),y) -> 0() times(s(x),y) -> plus(y,times(x,y)) times(s(0()),y) -> y - Signature: {div/2,divides/2,eq/2,if/3,p/1,plus/2,pr/2,prime/1,quot/3,times/2} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div,divides,eq,if,p,plus,pr,prime,quot ,times} and constructors {0,false,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs div#(x,y) -> c_1(quot#(x,y,y)) div#(0(),y) -> c_2() divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)) eq#(0(),0()) -> c_4() eq#(0(),s(y)) -> c_5() eq#(s(x),0()) -> c_6() eq#(s(x),s(y)) -> c_7(eq#(x,y)) if#(false(),x,y) -> c_8(pr#(x,y)) if#(true(),x,y) -> c_9() p#(s(x)) -> c_10() plus#(x,0()) -> c_11() plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))) plus#(0(),y) -> c_13() plus#(s(x),y) -> c_14(plus#(x,y)) plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))) pr#(x,s(0())) -> c_16() pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_18(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_19(div#(x,s(z))) quot#(0(),s(y),z) -> c_20() quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) times#(0(),y) -> c_22() times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)) times#(s(0()),y) -> c_24() Weak DPs and mark the set of starting terms. * Step 3: UsableRules MAYBE + Considered Problem: - Strict DPs: div#(x,y) -> c_1(quot#(x,y,y)) div#(0(),y) -> c_2() divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)) eq#(0(),0()) -> c_4() eq#(0(),s(y)) -> c_5() eq#(s(x),0()) -> c_6() eq#(s(x),s(y)) -> c_7(eq#(x,y)) if#(false(),x,y) -> c_8(pr#(x,y)) if#(true(),x,y) -> c_9() p#(s(x)) -> c_10() plus#(x,0()) -> c_11() plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))) plus#(0(),y) -> c_13() plus#(s(x),y) -> c_14(plus#(x,y)) plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))) pr#(x,s(0())) -> c_16() pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_18(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_19(div#(x,s(z))) quot#(0(),s(y),z) -> c_20() quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) times#(0(),y) -> c_22() times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)) times#(s(0()),y) -> c_24() - Weak TRS: div(x,y) -> quot(x,y,y) div(0(),y) -> 0() divides(y,x) -> eq(x,times(div(x,y),y)) eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) if(false(),x,y) -> pr(x,y) if(true(),x,y) -> false() p(s(x)) -> x plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,p(s(y)))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(s(x),y) -> s(plus(p(s(x)),y)) pr(x,s(0())) -> true() pr(x,s(s(y))) -> if(divides(s(s(y)),x),x,s(y)) prime(s(s(x))) -> pr(s(s(x)),s(x)) quot(x,0(),s(z)) -> s(div(x,s(z))) quot(0(),s(y),z) -> 0() quot(s(x),s(y),z) -> quot(x,y,z) times(0(),y) -> 0() times(s(x),y) -> plus(y,times(x,y)) times(s(0()),y) -> y - Signature: {div/2,divides/2,eq/2,if/3,p/1,plus/2,pr/2,prime/1,quot/3,times/2,div#/2,divides#/2,eq#/2,if#/3,p#/1,plus#/2 ,pr#/2,prime#/1,quot#/3,times#/2} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1 ,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/1,c_15/2,c_16/0,c_17/2,c_18/1,c_19/1,c_20/0,c_21/1,c_22/0,c_23/2 ,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot# ,times#} and constructors {0,false,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: div(x,y) -> quot(x,y,y) div(0(),y) -> 0() divides(y,x) -> eq(x,times(div(x,y),y)) eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) p(s(x)) -> x plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,p(s(y)))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(s(x),y) -> s(plus(p(s(x)),y)) quot(x,0(),s(z)) -> s(div(x,s(z))) quot(0(),s(y),z) -> 0() quot(s(x),s(y),z) -> quot(x,y,z) times(0(),y) -> 0() times(s(x),y) -> plus(y,times(x,y)) times(s(0()),y) -> y div#(x,y) -> c_1(quot#(x,y,y)) div#(0(),y) -> c_2() divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)) eq#(0(),0()) -> c_4() eq#(0(),s(y)) -> c_5() eq#(s(x),0()) -> c_6() eq#(s(x),s(y)) -> c_7(eq#(x,y)) if#(false(),x,y) -> c_8(pr#(x,y)) if#(true(),x,y) -> c_9() p#(s(x)) -> c_10() plus#(x,0()) -> c_11() plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))) plus#(0(),y) -> c_13() plus#(s(x),y) -> c_14(plus#(x,y)) plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))) pr#(x,s(0())) -> c_16() pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_18(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_19(div#(x,s(z))) quot#(0(),s(y),z) -> c_20() quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) times#(0(),y) -> c_22() times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)) times#(s(0()),y) -> c_24() * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: div#(x,y) -> c_1(quot#(x,y,y)) div#(0(),y) -> c_2() divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)) eq#(0(),0()) -> c_4() eq#(0(),s(y)) -> c_5() eq#(s(x),0()) -> c_6() eq#(s(x),s(y)) -> c_7(eq#(x,y)) if#(false(),x,y) -> c_8(pr#(x,y)) if#(true(),x,y) -> c_9() p#(s(x)) -> c_10() plus#(x,0()) -> c_11() plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))) plus#(0(),y) -> c_13() plus#(s(x),y) -> c_14(plus#(x,y)) plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))) pr#(x,s(0())) -> c_16() pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_18(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_19(div#(x,s(z))) quot#(0(),s(y),z) -> c_20() quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) times#(0(),y) -> c_22() times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)) times#(s(0()),y) -> c_24() - Weak TRS: div(x,y) -> quot(x,y,y) div(0(),y) -> 0() divides(y,x) -> eq(x,times(div(x,y),y)) eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) p(s(x)) -> x plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,p(s(y)))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(s(x),y) -> s(plus(p(s(x)),y)) quot(x,0(),s(z)) -> s(div(x,s(z))) quot(0(),s(y),z) -> 0() quot(s(x),s(y),z) -> quot(x,y,z) times(0(),y) -> 0() times(s(x),y) -> plus(y,times(x,y)) times(s(0()),y) -> y - Signature: {div/2,divides/2,eq/2,if/3,p/1,plus/2,pr/2,prime/1,quot/3,times/2,div#/2,divides#/2,eq#/2,if#/3,p#/1,plus#/2 ,pr#/2,prime#/1,quot#/3,times#/2} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1 ,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/1,c_15/2,c_16/0,c_17/2,c_18/1,c_19/1,c_20/0,c_21/1,c_22/0,c_23/2 ,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot# ,times#} and constructors {0,false,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,4,5,6,9,10,11,13,16,20,22,24} by application of Pre({2,4,5,6,9,10,11,13,16,20,22,24}) = {1,3,7,8,12,14,15,17,18,19,21,23}. Here rules are labelled as follows: 1: div#(x,y) -> c_1(quot#(x,y,y)) 2: div#(0(),y) -> c_2() 3: divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)) 4: eq#(0(),0()) -> c_4() 5: eq#(0(),s(y)) -> c_5() 6: eq#(s(x),0()) -> c_6() 7: eq#(s(x),s(y)) -> c_7(eq#(x,y)) 8: if#(false(),x,y) -> c_8(pr#(x,y)) 9: if#(true(),x,y) -> c_9() 10: p#(s(x)) -> c_10() 11: plus#(x,0()) -> c_11() 12: plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))) 13: plus#(0(),y) -> c_13() 14: plus#(s(x),y) -> c_14(plus#(x,y)) 15: plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))) 16: pr#(x,s(0())) -> c_16() 17: pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) 18: prime#(s(s(x))) -> c_18(pr#(s(s(x)),s(x))) 19: quot#(x,0(),s(z)) -> c_19(div#(x,s(z))) 20: quot#(0(),s(y),z) -> c_20() 21: quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) 22: times#(0(),y) -> c_22() 23: times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)) 24: times#(s(0()),y) -> c_24() * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: div#(x,y) -> c_1(quot#(x,y,y)) divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)) eq#(s(x),s(y)) -> c_7(eq#(x,y)) if#(false(),x,y) -> c_8(pr#(x,y)) plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))) plus#(s(x),y) -> c_14(plus#(x,y)) plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))) pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_18(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_19(div#(x,s(z))) quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)) - Weak DPs: div#(0(),y) -> c_2() eq#(0(),0()) -> c_4() eq#(0(),s(y)) -> c_5() eq#(s(x),0()) -> c_6() if#(true(),x,y) -> c_9() p#(s(x)) -> c_10() plus#(x,0()) -> c_11() plus#(0(),y) -> c_13() pr#(x,s(0())) -> c_16() quot#(0(),s(y),z) -> c_20() times#(0(),y) -> c_22() times#(s(0()),y) -> c_24() - Weak TRS: div(x,y) -> quot(x,y,y) div(0(),y) -> 0() divides(y,x) -> eq(x,times(div(x,y),y)) eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) p(s(x)) -> x plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,p(s(y)))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(s(x),y) -> s(plus(p(s(x)),y)) quot(x,0(),s(z)) -> s(div(x,s(z))) quot(0(),s(y),z) -> 0() quot(s(x),s(y),z) -> quot(x,y,z) times(0(),y) -> 0() times(s(x),y) -> plus(y,times(x,y)) times(s(0()),y) -> y - Signature: {div/2,divides/2,eq/2,if/3,p/1,plus/2,pr/2,prime/1,quot/3,times/2,div#/2,divides#/2,eq#/2,if#/3,p#/1,plus#/2 ,pr#/2,prime#/1,quot#/3,times#/2} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1 ,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/1,c_15/2,c_16/0,c_17/2,c_18/1,c_19/1,c_20/0,c_21/1,c_22/0,c_23/2 ,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot# ,times#} and constructors {0,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:div#(x,y) -> c_1(quot#(x,y,y)) -->_1 quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)):11 -->_1 quot#(0(),s(y),z) -> c_20():22 2:S:divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)) -->_2 times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)):12 -->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3 -->_2 times#(s(0()),y) -> c_24():24 -->_2 times#(0(),y) -> c_22():23 -->_1 eq#(s(x),0()) -> c_6():16 -->_1 eq#(0(),s(y)) -> c_5():15 -->_1 eq#(0(),0()) -> c_4():14 -->_3 div#(0(),y) -> c_2():13 -->_3 div#(x,y) -> c_1(quot#(x,y,y)):1 3:S:eq#(s(x),s(y)) -> c_7(eq#(x,y)) -->_1 eq#(s(x),0()) -> c_6():16 -->_1 eq#(0(),s(y)) -> c_5():15 -->_1 eq#(0(),0()) -> c_4():14 -->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3 4:S:if#(false(),x,y) -> c_8(pr#(x,y)) -->_1 pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):8 -->_1 pr#(x,s(0())) -> c_16():21 5:S:plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))) -->_1 plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_14(plus#(x,y)):6 -->_1 plus#(0(),y) -> c_13():20 -->_1 plus#(x,0()) -> c_11():19 -->_2 p#(s(x)) -> c_10():18 -->_1 plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))):5 6:S:plus#(s(x),y) -> c_14(plus#(x,y)) -->_1 plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(0(),y) -> c_13():20 -->_1 plus#(x,0()) -> c_11():19 -->_1 plus#(s(x),y) -> c_14(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))):5 7:S:plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))) -->_1 plus#(0(),y) -> c_13():20 -->_1 plus#(x,0()) -> c_11():19 -->_2 p#(s(x)) -> c_10():18 -->_1 plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_14(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))):5 8:S:pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) -->_1 if#(true(),x,y) -> c_9():17 -->_1 if#(false(),x,y) -> c_8(pr#(x,y)):4 -->_2 divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)):2 9:S:prime#(s(s(x))) -> c_18(pr#(s(s(x)),s(x))) -->_1 pr#(x,s(0())) -> c_16():21 -->_1 pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):8 10:S:quot#(x,0(),s(z)) -> c_19(div#(x,s(z))) -->_1 div#(0(),y) -> c_2():13 -->_1 div#(x,y) -> c_1(quot#(x,y,y)):1 11:S:quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) -->_1 quot#(0(),s(y),z) -> c_20():22 -->_1 quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)):11 -->_1 quot#(x,0(),s(z)) -> c_19(div#(x,s(z))):10 12:S:times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)) -->_2 times#(s(0()),y) -> c_24():24 -->_2 times#(0(),y) -> c_22():23 -->_1 plus#(0(),y) -> c_13():20 -->_1 plus#(x,0()) -> c_11():19 -->_2 times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)):12 -->_1 plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_14(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))):5 13:W:div#(0(),y) -> c_2() 14:W:eq#(0(),0()) -> c_4() 15:W:eq#(0(),s(y)) -> c_5() 16:W:eq#(s(x),0()) -> c_6() 17:W:if#(true(),x,y) -> c_9() 18:W:p#(s(x)) -> c_10() 19:W:plus#(x,0()) -> c_11() 20:W:plus#(0(),y) -> c_13() 21:W:pr#(x,s(0())) -> c_16() 22:W:quot#(0(),s(y),z) -> c_20() 23:W:times#(0(),y) -> c_22() 24:W:times#(s(0()),y) -> c_24() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 21: pr#(x,s(0())) -> c_16() 17: if#(true(),x,y) -> c_9() 14: eq#(0(),0()) -> c_4() 15: eq#(0(),s(y)) -> c_5() 16: eq#(s(x),0()) -> c_6() 18: p#(s(x)) -> c_10() 19: plus#(x,0()) -> c_11() 20: plus#(0(),y) -> c_13() 23: times#(0(),y) -> c_22() 24: times#(s(0()),y) -> c_24() 13: div#(0(),y) -> c_2() 22: quot#(0(),s(y),z) -> c_20() * Step 6: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: div#(x,y) -> c_1(quot#(x,y,y)) divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)) eq#(s(x),s(y)) -> c_7(eq#(x,y)) if#(false(),x,y) -> c_8(pr#(x,y)) plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))) plus#(s(x),y) -> c_14(plus#(x,y)) plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))) pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_18(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_19(div#(x,s(z))) quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)) - Weak TRS: div(x,y) -> quot(x,y,y) div(0(),y) -> 0() divides(y,x) -> eq(x,times(div(x,y),y)) eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) p(s(x)) -> x plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,p(s(y)))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(s(x),y) -> s(plus(p(s(x)),y)) quot(x,0(),s(z)) -> s(div(x,s(z))) quot(0(),s(y),z) -> 0() quot(s(x),s(y),z) -> quot(x,y,z) times(0(),y) -> 0() times(s(x),y) -> plus(y,times(x,y)) times(s(0()),y) -> y - Signature: {div/2,divides/2,eq/2,if/3,p/1,plus/2,pr/2,prime/1,quot/3,times/2,div#/2,divides#/2,eq#/2,if#/3,p#/1,plus#/2 ,pr#/2,prime#/1,quot#/3,times#/2} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1 ,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/1,c_15/2,c_16/0,c_17/2,c_18/1,c_19/1,c_20/0,c_21/1,c_22/0,c_23/2 ,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot# ,times#} and constructors {0,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:div#(x,y) -> c_1(quot#(x,y,y)) -->_1 quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)):11 2:S:divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)) -->_2 times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)):12 -->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3 -->_3 div#(x,y) -> c_1(quot#(x,y,y)):1 3:S:eq#(s(x),s(y)) -> c_7(eq#(x,y)) -->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3 4:S:if#(false(),x,y) -> c_8(pr#(x,y)) -->_1 pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):8 5:S:plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))) -->_1 plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_14(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))):5 6:S:plus#(s(x),y) -> c_14(plus#(x,y)) -->_1 plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_14(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))):5 7:S:plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))) -->_1 plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_14(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))):5 8:S:pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) -->_1 if#(false(),x,y) -> c_8(pr#(x,y)):4 -->_2 divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)):2 9:S:prime#(s(s(x))) -> c_18(pr#(s(s(x)),s(x))) -->_1 pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):8 10:S:quot#(x,0(),s(z)) -> c_19(div#(x,s(z))) -->_1 div#(x,y) -> c_1(quot#(x,y,y)):1 11:S:quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) -->_1 quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)):11 -->_1 quot#(x,0(),s(z)) -> c_19(div#(x,s(z))):10 12:S:times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)) -->_2 times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)):12 -->_1 plus#(s(x),y) -> c_15(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_14(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_12(plus#(x,p(s(y))),p#(s(y))):5 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: plus#(x,s(y)) -> c_12(plus#(x,p(s(y)))) plus#(s(x),y) -> c_15(plus#(p(s(x)),y)) * Step 7: RemoveHeads MAYBE + Considered Problem: - Strict DPs: div#(x,y) -> c_1(quot#(x,y,y)) divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)) eq#(s(x),s(y)) -> c_7(eq#(x,y)) if#(false(),x,y) -> c_8(pr#(x,y)) plus#(x,s(y)) -> c_12(plus#(x,p(s(y)))) plus#(s(x),y) -> c_14(plus#(x,y)) plus#(s(x),y) -> c_15(plus#(p(s(x)),y)) pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_18(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_19(div#(x,s(z))) quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)) - Weak TRS: div(x,y) -> quot(x,y,y) div(0(),y) -> 0() divides(y,x) -> eq(x,times(div(x,y),y)) eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) p(s(x)) -> x plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,p(s(y)))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(s(x),y) -> s(plus(p(s(x)),y)) quot(x,0(),s(z)) -> s(div(x,s(z))) quot(0(),s(y),z) -> 0() quot(s(x),s(y),z) -> quot(x,y,z) times(0(),y) -> 0() times(s(x),y) -> plus(y,times(x,y)) times(s(0()),y) -> y - Signature: {div/2,divides/2,eq/2,if/3,p/1,plus/2,pr/2,prime/1,quot/3,times/2,div#/2,divides#/2,eq#/2,if#/3,p#/1,plus#/2 ,pr#/2,prime#/1,quot#/3,times#/2} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1 ,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1,c_15/1,c_16/0,c_17/2,c_18/1,c_19/1,c_20/0,c_21/1,c_22/0,c_23/2 ,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot# ,times#} and constructors {0,false,s,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:div#(x,y) -> c_1(quot#(x,y,y)) -->_1 quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)):11 2:S:divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)) -->_2 times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)):12 -->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3 -->_3 div#(x,y) -> c_1(quot#(x,y,y)):1 3:S:eq#(s(x),s(y)) -> c_7(eq#(x,y)) -->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3 4:S:if#(false(),x,y) -> c_8(pr#(x,y)) -->_1 pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):8 5:S:plus#(x,s(y)) -> c_12(plus#(x,p(s(y)))) -->_1 plus#(s(x),y) -> c_15(plus#(p(s(x)),y)):7 -->_1 plus#(s(x),y) -> c_14(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_12(plus#(x,p(s(y)))):5 6:S:plus#(s(x),y) -> c_14(plus#(x,y)) -->_1 plus#(s(x),y) -> c_15(plus#(p(s(x)),y)):7 -->_1 plus#(s(x),y) -> c_14(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_12(plus#(x,p(s(y)))):5 7:S:plus#(s(x),y) -> c_15(plus#(p(s(x)),y)) -->_1 plus#(s(x),y) -> c_15(plus#(p(s(x)),y)):7 -->_1 plus#(s(x),y) -> c_14(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_12(plus#(x,p(s(y)))):5 8:S:pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) -->_1 if#(false(),x,y) -> c_8(pr#(x,y)):4 -->_2 divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)):2 9:S:prime#(s(s(x))) -> c_18(pr#(s(s(x)),s(x))) -->_1 pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):8 10:S:quot#(x,0(),s(z)) -> c_19(div#(x,s(z))) -->_1 div#(x,y) -> c_1(quot#(x,y,y)):1 11:S:quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) -->_1 quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)):11 -->_1 quot#(x,0(),s(z)) -> c_19(div#(x,s(z))):10 12:S:times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)) -->_2 times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)):12 -->_1 plus#(s(x),y) -> c_15(plus#(p(s(x)),y)):7 -->_1 plus#(s(x),y) -> c_14(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_12(plus#(x,p(s(y)))):5 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(9,prime#(s(s(x))) -> c_18(pr#(s(s(x)),s(x))))] * Step 8: Failure MAYBE + Considered Problem: - Strict DPs: div#(x,y) -> c_1(quot#(x,y,y)) divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)) eq#(s(x),s(y)) -> c_7(eq#(x,y)) if#(false(),x,y) -> c_8(pr#(x,y)) plus#(x,s(y)) -> c_12(plus#(x,p(s(y)))) plus#(s(x),y) -> c_14(plus#(x,y)) plus#(s(x),y) -> c_15(plus#(p(s(x)),y)) pr#(x,s(s(y))) -> c_17(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) quot#(x,0(),s(z)) -> c_19(div#(x,s(z))) quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) times#(s(x),y) -> c_23(plus#(y,times(x,y)),times#(x,y)) - Weak TRS: div(x,y) -> quot(x,y,y) div(0(),y) -> 0() divides(y,x) -> eq(x,times(div(x,y),y)) eq(0(),0()) -> true() eq(0(),s(y)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) p(s(x)) -> x plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,p(s(y)))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(s(x),y) -> s(plus(p(s(x)),y)) quot(x,0(),s(z)) -> s(div(x,s(z))) quot(0(),s(y),z) -> 0() quot(s(x),s(y),z) -> quot(x,y,z) times(0(),y) -> 0() times(s(x),y) -> plus(y,times(x,y)) times(s(0()),y) -> y - Signature: {div/2,divides/2,eq/2,if/3,p/1,plus/2,pr/2,prime/1,quot/3,times/2,div#/2,divides#/2,eq#/2,if#/3,p#/1,plus#/2 ,pr#/2,prime#/1,quot#/3,times#/2} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1 ,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1,c_15/1,c_16/0,c_17/2,c_18/1,c_19/1,c_20/0,c_21/1,c_22/0,c_23/2 ,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot# ,times#} and constructors {0,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE