MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: a() -> c() a() -> d() div(x,y) -> div2(x,y,0()) div2(x,y,i) -> if1(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)) if1(false(),b,x,y,i,j) -> if2(b,x,y,i,j) if1(true(),b,x,y,i,j) -> divZeroError() if2(false(),x,y,i,j) -> i if2(true(),x,y,i,j) -> div2(minus(x,y),y,j) ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) ifPlus(true(),x,y,z) -> y inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) - Signature: {a/0,div/2,div2/3,if1/6,if2/5,ifPlus/4,inc/1,le/2,minus/2,plus/2,plusIter/3} / {0/0,c/0,d/0,divZeroError/0 ,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {a,div,div2,if1,if2,ifPlus,inc,le,minus,plus ,plusIter} and constructors {0,c,d,divZeroError,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) -> c_3(div2#(x,y,0())) div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)),le#(y,0()),le#(y,x),plus#(i,0()),inc#(i)) if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)) if1#(true(),b,x,y,i,j) -> c_6() if2#(false(),x,y,i,j) -> c_7() if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)) ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))) ifPlus#(true(),x,y,z) -> c_10() inc#(0()) -> c_11() inc#(s(i)) -> c_12(inc#(i)) le#(0(),y) -> c_13() le#(s(x),0()) -> c_14() le#(s(x),s(y)) -> c_15(le#(x,y)) minus#(x,0()) -> c_16() minus#(0(),y) -> c_17() minus#(s(x),s(y)) -> c_18(minus#(x,y)) plus#(x,y) -> c_19(plusIter#(x,y,0())) plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)) 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) -> c_3(div2#(x,y,0())) div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)),le#(y,0()),le#(y,x),plus#(i,0()),inc#(i)) if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)) if1#(true(),b,x,y,i,j) -> c_6() if2#(false(),x,y,i,j) -> c_7() if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)) ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))) ifPlus#(true(),x,y,z) -> c_10() inc#(0()) -> c_11() inc#(s(i)) -> c_12(inc#(i)) le#(0(),y) -> c_13() le#(s(x),0()) -> c_14() le#(s(x),s(y)) -> c_15(le#(x,y)) minus#(x,0()) -> c_16() minus#(0(),y) -> c_17() minus#(s(x),s(y)) -> c_18(minus#(x,y)) plus#(x,y) -> c_19(plusIter#(x,y,0())) plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)) - Weak TRS: a() -> c() a() -> d() div(x,y) -> div2(x,y,0()) div2(x,y,i) -> if1(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)) if1(false(),b,x,y,i,j) -> if2(b,x,y,i,j) if1(true(),b,x,y,i,j) -> divZeroError() if2(false(),x,y,i,j) -> i if2(true(),x,y,i,j) -> div2(minus(x,y),y,j) ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) ifPlus(true(),x,y,z) -> y inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) - Signature: {a/0,div/2,div2/3,if1/6,if2/5,ifPlus/4,inc/1,le/2,minus/2,plus/2,plusIter/3,a#/0,div#/2,div2#/3,if1#/6 ,if2#/5,ifPlus#/4,inc#/1,le#/2,minus#/2,plus#/2,plusIter#/3} / {0/0,c/0,d/0,divZeroError/0,false/0,s/1 ,true/0,c_1/0,c_2/0,c_3/1,c_4/5,c_5/1,c_6/0,c_7/0,c_8/2,c_9/1,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1 ,c_16/0,c_17/0,c_18/1,c_19/1,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,div#,div2#,if1#,if2#,ifPlus#,inc#,le#,minus#,plus# ,plusIter#} and constructors {0,c,d,divZeroError,false,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) ifPlus(true(),x,y,z) -> y inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) a#() -> c_1() a#() -> c_2() div#(x,y) -> c_3(div2#(x,y,0())) div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)),le#(y,0()),le#(y,x),plus#(i,0()),inc#(i)) if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)) if1#(true(),b,x,y,i,j) -> c_6() if2#(false(),x,y,i,j) -> c_7() if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)) ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))) ifPlus#(true(),x,y,z) -> c_10() inc#(0()) -> c_11() inc#(s(i)) -> c_12(inc#(i)) le#(0(),y) -> c_13() le#(s(x),0()) -> c_14() le#(s(x),s(y)) -> c_15(le#(x,y)) minus#(x,0()) -> c_16() minus#(0(),y) -> c_17() minus#(s(x),s(y)) -> c_18(minus#(x,y)) plus#(x,y) -> c_19(plusIter#(x,y,0())) plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a#() -> c_1() a#() -> c_2() div#(x,y) -> c_3(div2#(x,y,0())) div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)),le#(y,0()),le#(y,x),plus#(i,0()),inc#(i)) if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)) if1#(true(),b,x,y,i,j) -> c_6() if2#(false(),x,y,i,j) -> c_7() if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)) ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))) ifPlus#(true(),x,y,z) -> c_10() inc#(0()) -> c_11() inc#(s(i)) -> c_12(inc#(i)) le#(0(),y) -> c_13() le#(s(x),0()) -> c_14() le#(s(x),s(y)) -> c_15(le#(x,y)) minus#(x,0()) -> c_16() minus#(0(),y) -> c_17() minus#(s(x),s(y)) -> c_18(minus#(x,y)) plus#(x,y) -> c_19(plusIter#(x,y,0())) plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)) - Weak TRS: ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) ifPlus(true(),x,y,z) -> y inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) - Signature: {a/0,div/2,div2/3,if1/6,if2/5,ifPlus/4,inc/1,le/2,minus/2,plus/2,plusIter/3,a#/0,div#/2,div2#/3,if1#/6 ,if2#/5,ifPlus#/4,inc#/1,le#/2,minus#/2,plus#/2,plusIter#/3} / {0/0,c/0,d/0,divZeroError/0,false/0,s/1 ,true/0,c_1/0,c_2/0,c_3/1,c_4/5,c_5/1,c_6/0,c_7/0,c_8/2,c_9/1,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1 ,c_16/0,c_17/0,c_18/1,c_19/1,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,div#,div2#,if1#,if2#,ifPlus#,inc#,le#,minus#,plus# ,plusIter#} and constructors {0,c,d,divZeroError,false,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,6,7,10,11,13,14,16,17} by application of Pre({1,2,6,7,10,11,13,14,16,17}) = {4,5,8,12,15,18,20}. Here rules are labelled as follows: 1: a#() -> c_1() 2: a#() -> c_2() 3: div#(x,y) -> c_3(div2#(x,y,0())) 4: div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)) ,le#(y,0()) ,le#(y,x) ,plus#(i,0()) ,inc#(i)) 5: if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)) 6: if1#(true(),b,x,y,i,j) -> c_6() 7: if2#(false(),x,y,i,j) -> c_7() 8: if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)) 9: ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))) 10: ifPlus#(true(),x,y,z) -> c_10() 11: inc#(0()) -> c_11() 12: inc#(s(i)) -> c_12(inc#(i)) 13: le#(0(),y) -> c_13() 14: le#(s(x),0()) -> c_14() 15: le#(s(x),s(y)) -> c_15(le#(x,y)) 16: minus#(x,0()) -> c_16() 17: minus#(0(),y) -> c_17() 18: minus#(s(x),s(y)) -> c_18(minus#(x,y)) 19: plus#(x,y) -> c_19(plusIter#(x,y,0())) 20: plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: div#(x,y) -> c_3(div2#(x,y,0())) div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)),le#(y,0()),le#(y,x),plus#(i,0()),inc#(i)) if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)) if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)) ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))) inc#(s(i)) -> c_12(inc#(i)) le#(s(x),s(y)) -> c_15(le#(x,y)) minus#(s(x),s(y)) -> c_18(minus#(x,y)) plus#(x,y) -> c_19(plusIter#(x,y,0())) plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)) - Weak DPs: a#() -> c_1() a#() -> c_2() if1#(true(),b,x,y,i,j) -> c_6() if2#(false(),x,y,i,j) -> c_7() ifPlus#(true(),x,y,z) -> c_10() inc#(0()) -> c_11() le#(0(),y) -> c_13() le#(s(x),0()) -> c_14() minus#(x,0()) -> c_16() minus#(0(),y) -> c_17() - Weak TRS: ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) ifPlus(true(),x,y,z) -> y inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) - Signature: {a/0,div/2,div2/3,if1/6,if2/5,ifPlus/4,inc/1,le/2,minus/2,plus/2,plusIter/3,a#/0,div#/2,div2#/3,if1#/6 ,if2#/5,ifPlus#/4,inc#/1,le#/2,minus#/2,plus#/2,plusIter#/3} / {0/0,c/0,d/0,divZeroError/0,false/0,s/1 ,true/0,c_1/0,c_2/0,c_3/1,c_4/5,c_5/1,c_6/0,c_7/0,c_8/2,c_9/1,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1 ,c_16/0,c_17/0,c_18/1,c_19/1,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,div#,div2#,if1#,if2#,ifPlus#,inc#,le#,minus#,plus# ,plusIter#} and constructors {0,c,d,divZeroError,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:div#(x,y) -> c_3(div2#(x,y,0())) -->_1 div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)) ,le#(y,0()) ,le#(y,x) ,plus#(i,0()) ,inc#(i)):2 2:S:div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)) ,le#(y,0()) ,le#(y,x) ,plus#(i,0()) ,inc#(i)) -->_4 plus#(x,y) -> c_19(plusIter#(x,y,0())):9 -->_3 le#(s(x),s(y)) -> c_15(le#(x,y)):7 -->_5 inc#(s(i)) -> c_12(inc#(i)):6 -->_1 if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)):3 -->_3 le#(s(x),0()) -> c_14():18 -->_2 le#(s(x),0()) -> c_14():18 -->_3 le#(0(),y) -> c_13():17 -->_2 le#(0(),y) -> c_13():17 -->_5 inc#(0()) -> c_11():16 -->_1 if1#(true(),b,x,y,i,j) -> c_6():13 3:S:if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)) -->_1 if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)):4 -->_1 if2#(false(),x,y,i,j) -> c_7():14 4:S:if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)) -->_2 minus#(s(x),s(y)) -> c_18(minus#(x,y)):8 -->_2 minus#(0(),y) -> c_17():20 -->_2 minus#(x,0()) -> c_16():19 -->_1 div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)) ,le#(y,0()) ,le#(y,x) ,plus#(i,0()) ,inc#(i)):2 5:S:ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))) -->_1 plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)):10 6:S:inc#(s(i)) -> c_12(inc#(i)) -->_1 inc#(0()) -> c_11():16 -->_1 inc#(s(i)) -> c_12(inc#(i)):6 7:S:le#(s(x),s(y)) -> c_15(le#(x,y)) -->_1 le#(s(x),0()) -> c_14():18 -->_1 le#(0(),y) -> c_13():17 -->_1 le#(s(x),s(y)) -> c_15(le#(x,y)):7 8:S:minus#(s(x),s(y)) -> c_18(minus#(x,y)) -->_1 minus#(0(),y) -> c_17():20 -->_1 minus#(x,0()) -> c_16():19 -->_1 minus#(s(x),s(y)) -> c_18(minus#(x,y)):8 9:S:plus#(x,y) -> c_19(plusIter#(x,y,0())) -->_1 plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)):10 10:S:plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)) -->_2 le#(s(x),0()) -> c_14():18 -->_2 le#(0(),y) -> c_13():17 -->_1 ifPlus#(true(),x,y,z) -> c_10():15 -->_2 le#(s(x),s(y)) -> c_15(le#(x,y)):7 -->_1 ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))):5 11:W:a#() -> c_1() 12:W:a#() -> c_2() 13:W:if1#(true(),b,x,y,i,j) -> c_6() 14:W:if2#(false(),x,y,i,j) -> c_7() 15:W:ifPlus#(true(),x,y,z) -> c_10() 16:W:inc#(0()) -> c_11() 17:W:le#(0(),y) -> c_13() 18:W:le#(s(x),0()) -> c_14() 19:W:minus#(x,0()) -> c_16() 20:W:minus#(0(),y) -> c_17() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 12: a#() -> c_2() 11: a#() -> c_1() 13: if1#(true(),b,x,y,i,j) -> c_6() 14: if2#(false(),x,y,i,j) -> c_7() 19: minus#(x,0()) -> c_16() 20: minus#(0(),y) -> c_17() 16: inc#(0()) -> c_11() 15: ifPlus#(true(),x,y,z) -> c_10() 17: le#(0(),y) -> c_13() 18: le#(s(x),0()) -> c_14() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: div#(x,y) -> c_3(div2#(x,y,0())) div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)),le#(y,0()),le#(y,x),plus#(i,0()),inc#(i)) if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)) if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)) ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))) inc#(s(i)) -> c_12(inc#(i)) le#(s(x),s(y)) -> c_15(le#(x,y)) minus#(s(x),s(y)) -> c_18(minus#(x,y)) plus#(x,y) -> c_19(plusIter#(x,y,0())) plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)) - Weak TRS: ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) ifPlus(true(),x,y,z) -> y inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) - Signature: {a/0,div/2,div2/3,if1/6,if2/5,ifPlus/4,inc/1,le/2,minus/2,plus/2,plusIter/3,a#/0,div#/2,div2#/3,if1#/6 ,if2#/5,ifPlus#/4,inc#/1,le#/2,minus#/2,plus#/2,plusIter#/3} / {0/0,c/0,d/0,divZeroError/0,false/0,s/1 ,true/0,c_1/0,c_2/0,c_3/1,c_4/5,c_5/1,c_6/0,c_7/0,c_8/2,c_9/1,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1 ,c_16/0,c_17/0,c_18/1,c_19/1,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,div#,div2#,if1#,if2#,ifPlus#,inc#,le#,minus#,plus# ,plusIter#} and constructors {0,c,d,divZeroError,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:div#(x,y) -> c_3(div2#(x,y,0())) -->_1 div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)) ,le#(y,0()) ,le#(y,x) ,plus#(i,0()) ,inc#(i)):2 2:S:div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)) ,le#(y,0()) ,le#(y,x) ,plus#(i,0()) ,inc#(i)) -->_4 plus#(x,y) -> c_19(plusIter#(x,y,0())):9 -->_3 le#(s(x),s(y)) -> c_15(le#(x,y)):7 -->_5 inc#(s(i)) -> c_12(inc#(i)):6 -->_1 if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)):3 3:S:if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)) -->_1 if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)):4 4:S:if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)) -->_2 minus#(s(x),s(y)) -> c_18(minus#(x,y)):8 -->_1 div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)) ,le#(y,0()) ,le#(y,x) ,plus#(i,0()) ,inc#(i)):2 5:S:ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))) -->_1 plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)):10 6:S:inc#(s(i)) -> c_12(inc#(i)) -->_1 inc#(s(i)) -> c_12(inc#(i)):6 7:S:le#(s(x),s(y)) -> c_15(le#(x,y)) -->_1 le#(s(x),s(y)) -> c_15(le#(x,y)):7 8:S:minus#(s(x),s(y)) -> c_18(minus#(x,y)) -->_1 minus#(s(x),s(y)) -> c_18(minus#(x,y)):8 9:S:plus#(x,y) -> c_19(plusIter#(x,y,0())) -->_1 plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)):10 10:S:plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)) -->_2 le#(s(x),s(y)) -> c_15(le#(x,y)):7 -->_1 ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))):5 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)),le#(y,x),plus#(i,0()),inc#(i)) * Step 6: RemoveHeads MAYBE + Considered Problem: - Strict DPs: div#(x,y) -> c_3(div2#(x,y,0())) div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)),le#(y,x),plus#(i,0()),inc#(i)) if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)) if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)) ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))) inc#(s(i)) -> c_12(inc#(i)) le#(s(x),s(y)) -> c_15(le#(x,y)) minus#(s(x),s(y)) -> c_18(minus#(x,y)) plus#(x,y) -> c_19(plusIter#(x,y,0())) plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)) - Weak TRS: ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) ifPlus(true(),x,y,z) -> y inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) - Signature: {a/0,div/2,div2/3,if1/6,if2/5,ifPlus/4,inc/1,le/2,minus/2,plus/2,plusIter/3,a#/0,div#/2,div2#/3,if1#/6 ,if2#/5,ifPlus#/4,inc#/1,le#/2,minus#/2,plus#/2,plusIter#/3} / {0/0,c/0,d/0,divZeroError/0,false/0,s/1 ,true/0,c_1/0,c_2/0,c_3/1,c_4/4,c_5/1,c_6/0,c_7/0,c_8/2,c_9/1,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1 ,c_16/0,c_17/0,c_18/1,c_19/1,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,div#,div2#,if1#,if2#,ifPlus#,inc#,le#,minus#,plus# ,plusIter#} and constructors {0,c,d,divZeroError,false,s,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:div#(x,y) -> c_3(div2#(x,y,0())) -->_1 div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)),le#(y,x),plus#(i,0()),inc#(i)):2 2:S:div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)),le#(y,x),plus#(i,0()),inc#(i)) -->_3 plus#(x,y) -> c_19(plusIter#(x,y,0())):9 -->_2 le#(s(x),s(y)) -> c_15(le#(x,y)):7 -->_4 inc#(s(i)) -> c_12(inc#(i)):6 -->_1 if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)):3 3:S:if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)) -->_1 if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)):4 4:S:if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)) -->_2 minus#(s(x),s(y)) -> c_18(minus#(x,y)):8 -->_1 div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)),le#(y,x),plus#(i,0()),inc#(i)):2 5:S:ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))) -->_1 plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)):10 6:S:inc#(s(i)) -> c_12(inc#(i)) -->_1 inc#(s(i)) -> c_12(inc#(i)):6 7:S:le#(s(x),s(y)) -> c_15(le#(x,y)) -->_1 le#(s(x),s(y)) -> c_15(le#(x,y)):7 8:S:minus#(s(x),s(y)) -> c_18(minus#(x,y)) -->_1 minus#(s(x),s(y)) -> c_18(minus#(x,y)):8 9:S:plus#(x,y) -> c_19(plusIter#(x,y,0())) -->_1 plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)):10 10:S:plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)) -->_2 le#(s(x),s(y)) -> c_15(le#(x,y)):7 -->_1 ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))):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). [(1,div#(x,y) -> c_3(div2#(x,y,0())))] * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: div2#(x,y,i) -> c_4(if1#(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i)),le#(y,x),plus#(i,0()),inc#(i)) if1#(false(),b,x,y,i,j) -> c_5(if2#(b,x,y,i,j)) if2#(true(),x,y,i,j) -> c_8(div2#(minus(x,y),y,j),minus#(x,y)) ifPlus#(false(),x,y,z) -> c_9(plusIter#(x,s(y),s(z))) inc#(s(i)) -> c_12(inc#(i)) le#(s(x),s(y)) -> c_15(le#(x,y)) minus#(s(x),s(y)) -> c_18(minus#(x,y)) plus#(x,y) -> c_19(plusIter#(x,y,0())) plusIter#(x,y,z) -> c_20(ifPlus#(le(x,z),x,y,z),le#(x,z)) - Weak TRS: ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) ifPlus(true(),x,y,z) -> y inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) - Signature: {a/0,div/2,div2/3,if1/6,if2/5,ifPlus/4,inc/1,le/2,minus/2,plus/2,plusIter/3,a#/0,div#/2,div2#/3,if1#/6 ,if2#/5,ifPlus#/4,inc#/1,le#/2,minus#/2,plus#/2,plusIter#/3} / {0/0,c/0,d/0,divZeroError/0,false/0,s/1 ,true/0,c_1/0,c_2/0,c_3/1,c_4/4,c_5/1,c_6/0,c_7/0,c_8/2,c_9/1,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1 ,c_16/0,c_17/0,c_18/1,c_19/1,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {a#,div#,div2#,if1#,if2#,ifPlus#,inc#,le#,minus#,plus# ,plusIter#} and constructors {0,c,d,divZeroError,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE