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