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: Decompose 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: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: eq#(s(x),s(y)) -> c_5(eq#(x,y)) - Weak DPs: 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} Problem (S) - Strict DPs: 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 DPs: eq#(s(x),s(y)) -> c_5(eq#(x,y)) - 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} ** Step 7.a:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq#(s(x),s(y)) -> c_5(eq#(x,y)) - Weak DPs: 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: RemoveWeakSuffixes + 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:W: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:W: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:W:inc#(s(x)) -> c_13(inc#(x)) -->_1 inc#(s(x)) -> c_13(inc#(x)):4 5:W:minus#(s(x),s(y)) -> c_17(minus#(x,y)) -->_1 minus#(s(x),s(y)) -> c_17(minus#(x,y)):5 6:W:plus#(x,y) -> c_18(ifPlus#(eq(x,0()),minus(x,s(0())),x,inc(x)),minus#(x,s(0())),inc#(x)) -->_1 ifPlus#(false(),x,y,z) -> c_8(plus#(x,z)):2 -->_3 inc#(s(x)) -> c_13(inc#(x)):4 -->_2 minus#(s(x),s(y)) -> c_17(minus#(x,y)):5 8:W: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)) -->_1 ifTimes#(false(),x,y,z,u) -> c_10(timesIter#(x,y,u)):3 -->_2 minus#(s(x),s(y)) -> c_17(minus#(x,y)):5 -->_3 plus#(x,y) -> c_18(ifPlus#(eq(x,0()),minus(x,s(0())),x,inc(x)),minus#(x,s(0())),inc#(x)):6 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: ifTimes#(false(),x,y,z,u) -> c_10(timesIter#(x,y,u)) 8: 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)) 2: ifPlus#(false(),x,y,z) -> c_8(plus#(x,z)) 6: plus#(x,y) -> c_18(ifPlus#(eq(x,0()),minus(x,s(0())),x,inc(x)),minus#(x,s(0())),inc#(x)) 4: inc#(s(x)) -> c_13(inc#(x)) 5: minus#(s(x),s(y)) -> c_17(minus#(x,y)) ** Step 7.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq#(s(x),s(y)) -> c_5(eq#(x,y)) - 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: UsableRules + Details: We replace rewrite rules by usable rules: eq#(s(x),s(y)) -> c_5(eq#(x,y)) ** Step 7.a:3: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq#(s(x),s(y)) -> c_5(eq#(x,y)) - 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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: eq#(s(x),s(y)) -> c_5(eq#(x,y)) The strictly oriented rules are moved into the weak component. *** Step 7.a:3.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq#(s(x),s(y)) -> c_5(eq#(x,y)) - 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1} Following symbols are considered usable: {eq#,f#,ifPlus#,ifTimes#,inc#,minus#,plus#,times#,timesIter#} TcT has computed the following interpretation: p(0) = [0] p(eq) = [1] x1 + [4] p(f) = [0] p(false) = [0] p(g) = [0] p(h) = [0] p(ifPlus) = [1] x4 + [0] p(ifTimes) = [1] x1 + [2] x2 + [1] x4 + [2] p(inc) = [0] p(minus) = [1] x2 + [2] p(plus) = [1] p(s) = [1] x1 + [1] p(times) = [1] x1 + [1] x2 + [8] p(timesIter) = [1] x1 + [1] x2 + [1] x3 + [4] p(true) = [1] p(eq#) = [1] x2 + [0] p(f#) = [2] p(ifPlus#) = [1] x2 + [1] x3 + [1] x4 + [1] p(ifTimes#) = [1] x2 + [2] x4 + [1] x5 + [1] p(inc#) = [2] p(minus#) = [1] x1 + [2] x2 + [0] p(plus#) = [4] x1 + [1] x2 + [1] p(times#) = [1] x2 + [2] p(timesIter#) = [2] p(c_1) = [1] p(c_2) = [0] p(c_3) = [0] p(c_4) = [2] p(c_5) = [1] x1 + [0] p(c_6) = [2] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [2] x1 + [1] p(c_11) = [1] p(c_12) = [0] p(c_13) = [1] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] p(c_17) = [1] x1 + [8] p(c_18) = [8] x2 + [1] x3 + [0] p(c_19) = [1] x1 + [1] p(c_20) = [1] x2 + [4] x3 + [2] Following rules are strictly oriented: eq#(s(x),s(y)) = [1] y + [1] > [1] y + [0] = c_5(eq#(x,y)) Following rules are (at-least) weakly oriented: *** Step 7.a:3.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: eq#(s(x),s(y)) -> c_5(eq#(x,y)) - 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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 7.a:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: eq#(s(x),s(y)) -> c_5(eq#(x,y)) - 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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:eq#(s(x),s(y)) -> c_5(eq#(x,y)) -->_1 eq#(s(x),s(y)) -> c_5(eq#(x,y)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: eq#(s(x),s(y)) -> c_5(eq#(x,y)) *** Step 7.a:3.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - 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 already closed. The intended complexity is O(1). ** Step 7.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: 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 DPs: eq#(s(x),s(y)) -> c_5(eq#(x,y)) - 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: RemoveWeakSuffixes + Details: Consider the dependency graph 1: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)):5 2: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)):6 3:S:inc#(s(x)) -> c_13(inc#(x)) -->_1 inc#(s(x)) -> c_13(inc#(x)):3 4:S:minus#(s(x),s(y)) -> c_17(minus#(x,y)) -->_1 minus#(s(x),s(y)) -> c_17(minus#(x,y)):4 5: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)):4 -->_3 inc#(s(x)) -> c_13(inc#(x)):3 -->_1 ifPlus#(false(),x,y,z) -> c_8(plus#(x,z)):1 6: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)):5 -->_2 minus#(s(x),s(y)) -> c_17(minus#(x,y)):4 -->_1 ifTimes#(false(),x,y,z,u) -> c_10(timesIter#(x,y,u)):2 7:W:eq#(s(x),s(y)) -> c_5(eq#(x,y)) -->_1 eq#(s(x),s(y)) -> c_5(eq#(x,y)):7 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 7: eq#(s(x),s(y)) -> c_5(eq#(x,y)) ** Step 7.b:2: Decompose MAYBE + Considered Problem: - Strict DPs: 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: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: ifPlus#(false(),x,y,z) -> c_8(plus#(x,z)) 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)) - Weak DPs: ifTimes#(false(),x,y,z,u) -> c_10(timesIter#(x,y,u)) 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} Problem (S) - Strict DPs: ifTimes#(false(),x,y,z,u) -> c_10(timesIter#(x,y,u)) 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 DPs: ifPlus#(false(),x,y,z) -> c_8(plus#(x,z)) 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)) - 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} *** Step 7.b:2.a:1: Failure MAYBE + Considered Problem: - Strict DPs: ifPlus#(false(),x,y,z) -> c_8(plus#(x,z)) 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)) - Weak DPs: ifTimes#(false(),x,y,z,u) -> c_10(timesIter#(x,y,u)) 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. *** Step 7.b:2.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: ifTimes#(false(),x,y,z,u) -> c_10(timesIter#(x,y,u)) 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 DPs: ifPlus#(false(),x,y,z) -> c_8(plus#(x,z)) 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)) - 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: RemoveWeakSuffixes + Details: Consider the dependency graph 1: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)):2 2: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)):1 3:W: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 4:W:inc#(s(x)) -> c_13(inc#(x)) -->_1 inc#(s(x)) -> c_13(inc#(x)):4 5:W:minus#(s(x),s(y)) -> c_17(minus#(x,y)) -->_1 minus#(s(x),s(y)) -> c_17(minus#(x,y)):5 6:W: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)):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: plus#(x,y) -> c_18(ifPlus#(eq(x,0()),minus(x,s(0())),x,inc(x)),minus#(x,s(0())),inc#(x)) 3: ifPlus#(false(),x,y,z) -> c_8(plus#(x,z)) 4: inc#(s(x)) -> c_13(inc#(x)) 5: minus#(s(x),s(y)) -> c_17(minus#(x,y)) *** Step 7.b:2.b:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: ifTimes#(false(),x,y,z,u) -> c_10(timesIter#(x,y,u)) 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: SimplifyRHS + Details: Consider the dependency graph 1: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)):2 2: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)) -->_1 ifTimes#(false(),x,y,z,u) -> c_10(timesIter#(x,y,u)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: timesIter#(x,y,z) -> c_20(ifTimes#(eq(x,0()),minus(x,s(0())),y,z,plus(y,z))) *** Step 7.b:2.b:3: Failure MAYBE + Considered Problem: - Strict DPs: ifTimes#(false(),x,y,z,u) -> c_10(timesIter#(x,y,u)) timesIter#(x,y,z) -> c_20(ifTimes#(eq(x,0()),minus(x,s(0())),y,z,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/1} - 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