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