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