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