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