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(zero(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(0()) -> 0() 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(s(x),s(y),z) -> quot(x,y,z) quot(zero(y),s(y),z) -> 0() times(0(),y) -> 0() times(s(x),y) -> plus(y,times(x,y)) times(s(0()),y) -> y zero(div(x,x)) -> x zero(divides(x,x)) -> x zero(quot(x,x,x)) -> x zero(s(x)) -> if(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))) zero(times(x,x)) -> x - Signature: {div/2,divides/2,eq/2,if/3,p/1,plus/2,pr/2,prime/1,quot/3,times/2,zero/1} / {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 ,zero} 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(zero(y),z)) zero(div(x,x)) -> x zero(divides(x,x)) -> x 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(0()) -> 0() 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(s(x),s(y),z) -> quot(x,y,z) quot(zero(y),s(y),z) -> 0() times(0(),y) -> 0() times(s(x),y) -> plus(y,times(x,y)) times(s(0()),y) -> y zero(quot(x,x,x)) -> x zero(s(x)) -> if(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))) zero(times(x,x)) -> x - Signature: {div/2,divides/2,eq/2,if/3,p/1,plus/2,pr/2,prime/1,quot/3,times/2,zero/1} / {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 ,zero} 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#(0()) -> c_10() p#(s(x)) -> c_11() plus#(x,0()) -> c_12() plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))) plus#(0(),y) -> c_14() plus#(s(x),y) -> c_15(plus#(x,y)) plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))) pr#(x,s(0())) -> c_17() pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_19(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_20(div#(x,s(z))) quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) quot#(zero(y),s(y),z) -> c_22() times#(0(),y) -> c_23() times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)) times#(s(0()),y) -> c_25() zero#(quot(x,x,x)) -> c_26() zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))) ,eq#(x,s(0())) ,plus#(zero(0()),0()) ,zero#(0()) ,plus#(0(),zero(0())) ,zero#(0())) zero#(times(x,x)) -> c_28() 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#(0()) -> c_10() p#(s(x)) -> c_11() plus#(x,0()) -> c_12() plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))) plus#(0(),y) -> c_14() plus#(s(x),y) -> c_15(plus#(x,y)) plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))) pr#(x,s(0())) -> c_17() pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_19(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_20(div#(x,s(z))) quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) quot#(zero(y),s(y),z) -> c_22() times#(0(),y) -> c_23() times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)) times#(s(0()),y) -> c_25() zero#(quot(x,x,x)) -> c_26() zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))) ,eq#(x,s(0())) ,plus#(zero(0()),0()) ,zero#(0()) ,plus#(0(),zero(0())) ,zero#(0())) zero#(times(x,x)) -> c_28() - 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(0()) -> 0() 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(s(x),s(y),z) -> quot(x,y,z) quot(zero(y),s(y),z) -> 0() times(0(),y) -> 0() times(s(x),y) -> plus(y,times(x,y)) times(s(0()),y) -> y zero(quot(x,x,x)) -> x zero(s(x)) -> if(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))) zero(times(x,x)) -> x - Signature: {div/2,divides/2,eq/2,if/3,p/1,plus/2,pr/2,prime/1,quot/3,times/2,zero/1,div#/2,divides#/2,eq#/2,if#/3,p#/1 ,plus#/2,pr#/2,prime#/1,quot#/3,times#/2,zero#/1} / {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/0,c_13/2,c_14/0,c_15/1,c_16/2,c_17/0,c_18/2,c_19/1,c_20/1,c_21/1 ,c_22/0,c_23/0,c_24/2,c_25/0,c_26/0,c_27/6,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot#,times# ,zero#} 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(s(x),s(y),z) -> quot(x,y,z) quot(zero(y),s(y),z) -> 0() 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#(0()) -> c_10() p#(s(x)) -> c_11() plus#(x,0()) -> c_12() plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))) plus#(0(),y) -> c_14() plus#(s(x),y) -> c_15(plus#(x,y)) plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))) pr#(x,s(0())) -> c_17() pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_19(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_20(div#(x,s(z))) quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) quot#(zero(y),s(y),z) -> c_22() times#(0(),y) -> c_23() times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)) times#(s(0()),y) -> c_25() zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))) ,eq#(x,s(0())) ,plus#(zero(0()),0()) ,zero#(0()) ,plus#(0(),zero(0())) ,zero#(0())) * 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#(0()) -> c_10() p#(s(x)) -> c_11() plus#(x,0()) -> c_12() plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))) plus#(0(),y) -> c_14() plus#(s(x),y) -> c_15(plus#(x,y)) plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))) pr#(x,s(0())) -> c_17() pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_19(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_20(div#(x,s(z))) quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) quot#(zero(y),s(y),z) -> c_22() times#(0(),y) -> c_23() times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)) times#(s(0()),y) -> c_25() zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))) ,eq#(x,s(0())) ,plus#(zero(0()),0()) ,zero#(0()) ,plus#(0(),zero(0())) ,zero#(0())) - 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(s(x),s(y),z) -> quot(x,y,z) quot(zero(y),s(y),z) -> 0() 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,zero/1,div#/2,divides#/2,eq#/2,if#/3,p#/1 ,plus#/2,pr#/2,prime#/1,quot#/3,times#/2,zero#/1} / {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/0,c_13/2,c_14/0,c_15/1,c_16/2,c_17/0,c_18/2,c_19/1,c_20/1,c_21/1 ,c_22/0,c_23/0,c_24/2,c_25/0,c_26/0,c_27/6,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot#,times# ,zero#} 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,12,14,17,22,23,25} by application of Pre({2,4,5,6,9,10,11,12,14,17,22,23,25}) = {1,3,7,8,13,15,16,18,19,20,21,24,26}. 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#(0()) -> c_10() 11: p#(s(x)) -> c_11() 12: plus#(x,0()) -> c_12() 13: plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))) 14: plus#(0(),y) -> c_14() 15: plus#(s(x),y) -> c_15(plus#(x,y)) 16: plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))) 17: pr#(x,s(0())) -> c_17() 18: pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) 19: prime#(s(s(x))) -> c_19(pr#(s(s(x)),s(x))) 20: quot#(x,0(),s(z)) -> c_20(div#(x,s(z))) 21: quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) 22: quot#(zero(y),s(y),z) -> c_22() 23: times#(0(),y) -> c_23() 24: times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)) 25: times#(s(0()),y) -> c_25() 26: zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))) ,eq#(x,s(0())) ,plus#(zero(0()),0()) ,zero#(0()) ,plus#(0(),zero(0())) ,zero#(0())) * 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_13(plus#(x,p(s(y))),p#(s(y))) plus#(s(x),y) -> c_15(plus#(x,y)) plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))) pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_19(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_20(div#(x,s(z))) quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)) zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))) ,eq#(x,s(0())) ,plus#(zero(0()),0()) ,zero#(0()) ,plus#(0(),zero(0())) ,zero#(0())) - 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#(0()) -> c_10() p#(s(x)) -> c_11() plus#(x,0()) -> c_12() plus#(0(),y) -> c_14() pr#(x,s(0())) -> c_17() quot#(zero(y),s(y),z) -> c_22() times#(0(),y) -> c_23() times#(s(0()),y) -> c_25() - 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(s(x),s(y),z) -> quot(x,y,z) quot(zero(y),s(y),z) -> 0() 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,zero/1,div#/2,divides#/2,eq#/2,if#/3,p#/1 ,plus#/2,pr#/2,prime#/1,quot#/3,times#/2,zero#/1} / {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/0,c_13/2,c_14/0,c_15/1,c_16/2,c_17/0,c_18/2,c_19/1,c_20/1,c_21/1 ,c_22/0,c_23/0,c_24/2,c_25/0,c_26/0,c_27/6,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot#,times# ,zero#} 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#(zero(y),s(y),z) -> c_22():24 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_24(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_25():26 -->_2 times#(0(),y) -> c_23():25 -->_1 eq#(s(x),0()) -> c_6():17 -->_1 eq#(0(),s(y)) -> c_5():16 -->_1 eq#(0(),0()) -> c_4():15 -->_3 div#(0(),y) -> c_2():14 -->_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():17 -->_1 eq#(0(),s(y)) -> c_5():16 -->_1 eq#(0(),0()) -> c_4():15 -->_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_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):8 -->_1 pr#(x,s(0())) -> c_17():23 5:S:plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))) -->_1 plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_15(plus#(x,y)):6 -->_1 plus#(0(),y) -> c_14():22 -->_1 plus#(x,0()) -> c_12():21 -->_2 p#(s(x)) -> c_11():20 -->_1 plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))):5 6:S:plus#(s(x),y) -> c_15(plus#(x,y)) -->_1 plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(0(),y) -> c_14():22 -->_1 plus#(x,0()) -> c_12():21 -->_1 plus#(s(x),y) -> c_15(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))):5 7:S:plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))) -->_1 plus#(0(),y) -> c_14():22 -->_1 plus#(x,0()) -> c_12():21 -->_2 p#(s(x)) -> c_11():20 -->_1 plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_15(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))):5 8:S:pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) -->_1 if#(true(),x,y) -> c_9():18 -->_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_19(pr#(s(s(x)),s(x))) -->_1 pr#(x,s(0())) -> c_17():23 -->_1 pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):8 10:S:quot#(x,0(),s(z)) -> c_20(div#(x,s(z))) -->_1 div#(0(),y) -> c_2():14 -->_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#(zero(y),s(y),z) -> c_22():24 -->_1 quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)):11 -->_1 quot#(x,0(),s(z)) -> c_20(div#(x,s(z))):10 12:S:times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)) -->_2 times#(s(0()),y) -> c_25():26 -->_2 times#(0(),y) -> c_23():25 -->_1 plus#(0(),y) -> c_14():22 -->_1 plus#(x,0()) -> c_12():21 -->_2 times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)):12 -->_1 plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_15(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))):5 13:S:zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))) ,eq#(x,s(0())) ,plus#(zero(0()),0()) ,zero#(0()) ,plus#(0(),zero(0())) ,zero#(0())) -->_5 plus#(0(),y) -> c_14():22 -->_3 plus#(x,0()) -> c_12():21 -->_1 if#(true(),x,y) -> c_9():18 -->_2 eq#(0(),s(y)) -> c_5():16 -->_1 if#(false(),x,y) -> c_8(pr#(x,y)):4 -->_2 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3 14:W:div#(0(),y) -> c_2() 15:W:eq#(0(),0()) -> c_4() 16:W:eq#(0(),s(y)) -> c_5() 17:W:eq#(s(x),0()) -> c_6() 18:W:if#(true(),x,y) -> c_9() 19:W:p#(0()) -> c_10() 20:W:p#(s(x)) -> c_11() 21:W:plus#(x,0()) -> c_12() 22:W:plus#(0(),y) -> c_14() 23:W:pr#(x,s(0())) -> c_17() 24:W:quot#(zero(y),s(y),z) -> c_22() 25:W:times#(0(),y) -> c_23() 26:W:times#(s(0()),y) -> c_25() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 19: p#(0()) -> c_10() 23: pr#(x,s(0())) -> c_17() 18: if#(true(),x,y) -> c_9() 15: eq#(0(),0()) -> c_4() 16: eq#(0(),s(y)) -> c_5() 17: eq#(s(x),0()) -> c_6() 20: p#(s(x)) -> c_11() 21: plus#(x,0()) -> c_12() 22: plus#(0(),y) -> c_14() 25: times#(0(),y) -> c_23() 26: times#(s(0()),y) -> c_25() 14: div#(0(),y) -> c_2() 24: quot#(zero(y),s(y),z) -> c_22() * 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_13(plus#(x,p(s(y))),p#(s(y))) plus#(s(x),y) -> c_15(plus#(x,y)) plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))) pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_19(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_20(div#(x,s(z))) quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)) zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))) ,eq#(x,s(0())) ,plus#(zero(0()),0()) ,zero#(0()) ,plus#(0(),zero(0())) ,zero#(0())) - 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(s(x),s(y),z) -> quot(x,y,z) quot(zero(y),s(y),z) -> 0() 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,zero/1,div#/2,divides#/2,eq#/2,if#/3,p#/1 ,plus#/2,pr#/2,prime#/1,quot#/3,times#/2,zero#/1} / {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/0,c_13/2,c_14/0,c_15/1,c_16/2,c_17/0,c_18/2,c_19/1,c_20/1,c_21/1 ,c_22/0,c_23/0,c_24/2,c_25/0,c_26/0,c_27/6,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot#,times# ,zero#} 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_24(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_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):8 5:S:plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))) -->_1 plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_15(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))):5 6:S:plus#(s(x),y) -> c_15(plus#(x,y)) -->_1 plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_15(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))):5 7:S:plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))) -->_1 plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_15(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))):5 8:S:pr#(x,s(s(y))) -> c_18(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_19(pr#(s(s(x)),s(x))) -->_1 pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):8 10:S:quot#(x,0(),s(z)) -> c_20(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_20(div#(x,s(z))):10 12:S:times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)) -->_2 times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)):12 -->_1 plus#(s(x),y) -> c_16(plus#(p(s(x)),y),p#(s(x))):7 -->_1 plus#(s(x),y) -> c_15(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_13(plus#(x,p(s(y))),p#(s(y))):5 13:S:zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))) ,eq#(x,s(0())) ,plus#(zero(0()),0()) ,zero#(0()) ,plus#(0(),zero(0())) ,zero#(0())) -->_1 if#(false(),x,y) -> c_8(pr#(x,y)):4 -->_2 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: plus#(x,s(y)) -> c_13(plus#(x,p(s(y)))) plus#(s(x),y) -> c_16(plus#(p(s(x)),y)) zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))),eq#(x,s(0()))) * 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_13(plus#(x,p(s(y)))) plus#(s(x),y) -> c_15(plus#(x,y)) plus#(s(x),y) -> c_16(plus#(p(s(x)),y)) pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) prime#(s(s(x))) -> c_19(pr#(s(s(x)),s(x))) quot#(x,0(),s(z)) -> c_20(div#(x,s(z))) quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)) zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))),eq#(x,s(0()))) - 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(s(x),s(y),z) -> quot(x,y,z) quot(zero(y),s(y),z) -> 0() 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,zero/1,div#/2,divides#/2,eq#/2,if#/3,p#/1 ,plus#/2,pr#/2,prime#/1,quot#/3,times#/2,zero#/1} / {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/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/2,c_19/1,c_20/1,c_21/1 ,c_22/0,c_23/0,c_24/2,c_25/0,c_26/0,c_27/2,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot#,times# ,zero#} 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_24(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_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):8 5:S:plus#(x,s(y)) -> c_13(plus#(x,p(s(y)))) -->_1 plus#(s(x),y) -> c_16(plus#(p(s(x)),y)):7 -->_1 plus#(s(x),y) -> c_15(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_13(plus#(x,p(s(y)))):5 6:S:plus#(s(x),y) -> c_15(plus#(x,y)) -->_1 plus#(s(x),y) -> c_16(plus#(p(s(x)),y)):7 -->_1 plus#(s(x),y) -> c_15(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_13(plus#(x,p(s(y)))):5 7:S:plus#(s(x),y) -> c_16(plus#(p(s(x)),y)) -->_1 plus#(s(x),y) -> c_16(plus#(p(s(x)),y)):7 -->_1 plus#(s(x),y) -> c_15(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_13(plus#(x,p(s(y)))):5 8:S:pr#(x,s(s(y))) -> c_18(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_19(pr#(s(s(x)),s(x))) -->_1 pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):8 10:S:quot#(x,0(),s(z)) -> c_20(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_20(div#(x,s(z))):10 12:S:times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)) -->_2 times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)):12 -->_1 plus#(s(x),y) -> c_16(plus#(p(s(x)),y)):7 -->_1 plus#(s(x),y) -> c_15(plus#(x,y)):6 -->_1 plus#(x,s(y)) -> c_13(plus#(x,p(s(y)))):5 13:S:zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))),eq#(x,s(0()))) -->_1 if#(false(),x,y) -> c_8(pr#(x,y)):4 -->_2 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3 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_19(pr#(s(s(x)),s(x))))] * Step 8: NaturalMI 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_13(plus#(x,p(s(y)))) plus#(s(x),y) -> c_15(plus#(x,y)) plus#(s(x),y) -> c_16(plus#(p(s(x)),y)) pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) quot#(x,0(),s(z)) -> c_20(div#(x,s(z))) quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)) zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))),eq#(x,s(0()))) - 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(s(x),s(y),z) -> quot(x,y,z) quot(zero(y),s(y),z) -> 0() 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,zero/1,div#/2,divides#/2,eq#/2,if#/3,p#/1 ,plus#/2,pr#/2,prime#/1,quot#/3,times#/2,zero#/1} / {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/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/2,c_19/1,c_20/1,c_21/1 ,c_22/0,c_23/0,c_24/2,c_25/0,c_26/0,c_27/2,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot#,times# ,zero#} and constructors {0,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_1) = {1}, uargs(c_3) = {1,2,3}, uargs(c_7) = {1}, uargs(c_8) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1}, uargs(c_18) = {1,2}, uargs(c_20) = {1}, uargs(c_21) = {1}, uargs(c_24) = {1,2}, uargs(c_27) = {1,2} Following symbols are considered usable: {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot#,times#,zero#} TcT has computed the following interpretation: p(0) = [1] p(div) = [2] x2 + [2] p(divides) = [1] x2 + [0] p(eq) = [0] p(false) = [0] p(if) = [0] p(p) = [6] p(plus) = [2] x2 + [2] p(pr) = [2] x2 + [0] p(prime) = [1] x1 + [0] p(quot) = [3] x1 + [5] x2 + [4] x3 + [5] p(s) = [0] p(times) = [2] x1 + [0] p(true) = [1] p(zero) = [2] x1 + [2] p(div#) = [1] x2 + [0] p(divides#) = [1] x1 + [0] p(eq#) = [0] p(if#) = [0] p(p#) = [1] p(plus#) = [0] p(pr#) = [0] p(prime#) = [1] p(quot#) = [0] p(times#) = [0] p(zero#) = [6] p(c_1) = [2] x1 + [0] p(c_2) = [1] p(c_3) = [1] x1 + [1] x2 + [1] x3 + [0] p(c_4) = [1] p(c_5) = [1] p(c_6) = [4] p(c_7) = [4] x1 + [0] p(c_8) = [4] x1 + [0] p(c_9) = [1] p(c_10) = [1] p(c_11) = [0] p(c_12) = [2] p(c_13) = [4] x1 + [0] p(c_14) = [0] p(c_15) = [1] x1 + [0] p(c_16) = [4] x1 + [0] p(c_17) = [0] p(c_18) = [4] x1 + [2] x2 + [0] p(c_19) = [4] x1 + [0] p(c_20) = [1] x1 + [0] p(c_21) = [1] x1 + [0] p(c_22) = [2] p(c_23) = [0] p(c_24) = [4] x1 + [4] x2 + [0] p(c_25) = [1] p(c_26) = [1] p(c_27) = [4] x1 + [1] x2 + [3] p(c_28) = [0] Following rules are strictly oriented: zero#(s(x)) = [6] > [3] = c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))),eq#(x,s(0()))) Following rules are (at-least) weakly oriented: div#(x,y) = [1] y + [0] >= [0] = c_1(quot#(x,y,y)) divides#(y,x) = [1] y + [0] >= [1] y + [0] = c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)) eq#(s(x),s(y)) = [0] >= [0] = c_7(eq#(x,y)) if#(false(),x,y) = [0] >= [0] = c_8(pr#(x,y)) plus#(x,s(y)) = [0] >= [0] = c_13(plus#(x,p(s(y)))) plus#(s(x),y) = [0] >= [0] = c_15(plus#(x,y)) plus#(s(x),y) = [0] >= [0] = c_16(plus#(p(s(x)),y)) pr#(x,s(s(y))) = [0] >= [0] = c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) quot#(x,0(),s(z)) = [0] >= [0] = c_20(div#(x,s(z))) quot#(s(x),s(y),z) = [0] >= [0] = c_21(quot#(x,y,z)) times#(s(x),y) = [0] >= [0] = c_24(plus#(y,times(x,y)),times#(x,y)) * Step 9: 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_13(plus#(x,p(s(y)))) plus#(s(x),y) -> c_15(plus#(x,y)) plus#(s(x),y) -> c_16(plus#(p(s(x)),y)) pr#(x,s(s(y))) -> c_18(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)) quot#(x,0(),s(z)) -> c_20(div#(x,s(z))) quot#(s(x),s(y),z) -> c_21(quot#(x,y,z)) times#(s(x),y) -> c_24(plus#(y,times(x,y)),times#(x,y)) - Weak DPs: zero#(s(x)) -> c_27(if#(eq(x,s(0())),plus(zero(0()),0()),s(plus(0(),zero(0())))),eq#(x,s(0()))) - 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(s(x),s(y),z) -> quot(x,y,z) quot(zero(y),s(y),z) -> 0() 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,zero/1,div#/2,divides#/2,eq#/2,if#/3,p#/1 ,plus#/2,pr#/2,prime#/1,quot#/3,times#/2,zero#/1} / {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/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/2,c_19/1,c_20/1,c_21/1 ,c_22/0,c_23/0,c_24/2,c_25/0,c_26/0,c_27/2,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,p#,plus#,pr#,prime#,quot#,times# ,zero#} and constructors {0,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE