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