MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) help(false(),c,x,y,z) -> towerIter(s(c),x,y,exp(y,z)) help(true(),c,x,y,z) -> z 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)) tower(x,y) -> towerIter(0(),x,y,s(0())) towerIter(c,x,y,z) -> help(ge(c,x),c,x,y,z) - Signature: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {exp,ge,help,plus,times,tower ,towerIter} and constructors {0,false,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs exp#(x,0()) -> c_1() exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) ge#(x,0()) -> c_3() ge#(0(),s(x)) -> c_4() ge#(s(x),s(y)) -> c_5(ge#(x,y)) help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) help#(true(),c,x,y,z) -> c_7() plus#(0(),x) -> c_8() plus#(s(x),y) -> c_9(plus#(x,y)) times#(0(),y) -> c_10() times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) tower#(x,y) -> c_12(towerIter#(0(),x,y,s(0()))) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: exp#(x,0()) -> c_1() exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) ge#(x,0()) -> c_3() ge#(0(),s(x)) -> c_4() ge#(s(x),s(y)) -> c_5(ge#(x,y)) help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) help#(true(),c,x,y,z) -> c_7() plus#(0(),x) -> c_8() plus#(s(x),y) -> c_9(plus#(x,y)) times#(0(),y) -> c_10() times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) tower#(x,y) -> c_12(towerIter#(0(),x,y,s(0()))) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) help(false(),c,x,y,z) -> towerIter(s(c),x,y,exp(y,z)) help(true(),c,x,y,z) -> z 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)) tower(x,y) -> towerIter(0(),x,y,s(0())) towerIter(c,x,y,z) -> help(ge(c,x),c,x,y,z) - Signature: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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)) exp#(x,0()) -> c_1() exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) ge#(x,0()) -> c_3() ge#(0(),s(x)) -> c_4() ge#(s(x),s(y)) -> c_5(ge#(x,y)) help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) help#(true(),c,x,y,z) -> c_7() plus#(0(),x) -> c_8() plus#(s(x),y) -> c_9(plus#(x,y)) times#(0(),y) -> c_10() times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) tower#(x,y) -> c_12(towerIter#(0(),x,y,s(0()))) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: exp#(x,0()) -> c_1() exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) ge#(x,0()) -> c_3() ge#(0(),s(x)) -> c_4() ge#(s(x),s(y)) -> c_5(ge#(x,y)) help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) help#(true(),c,x,y,z) -> c_7() plus#(0(),x) -> c_8() plus#(s(x),y) -> c_9(plus#(x,y)) times#(0(),y) -> c_10() times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) tower#(x,y) -> c_12(towerIter#(0(),x,y,s(0()))) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} 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,4,7,8,10} by application of Pre({1,3,4,7,8,10}) = {2,5,6,9,11,13}. Here rules are labelled as follows: 1: exp#(x,0()) -> c_1() 2: exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) 3: ge#(x,0()) -> c_3() 4: ge#(0(),s(x)) -> c_4() 5: ge#(s(x),s(y)) -> c_5(ge#(x,y)) 6: help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) 7: help#(true(),c,x,y,z) -> c_7() 8: plus#(0(),x) -> c_8() 9: plus#(s(x),y) -> c_9(plus#(x,y)) 10: times#(0(),y) -> c_10() 11: times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) 12: tower#(x,y) -> c_12(towerIter#(0(),x,y,s(0()))) 13: towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) ge#(s(x),s(y)) -> c_5(ge#(x,y)) help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) plus#(s(x),y) -> c_9(plus#(x,y)) times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) tower#(x,y) -> c_12(towerIter#(0(),x,y,s(0()))) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak DPs: exp#(x,0()) -> c_1() ge#(x,0()) -> c_3() ge#(0(),s(x)) -> c_4() help#(true(),c,x,y,z) -> c_7() plus#(0(),x) -> c_8() times#(0(),y) -> c_10() - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) -->_1 times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)):5 -->_1 times#(0(),y) -> c_10():13 -->_2 exp#(x,0()) -> c_1():8 -->_2 exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)):1 2:S:ge#(s(x),s(y)) -> c_5(ge#(x,y)) -->_1 ge#(0(),s(x)) -> c_4():10 -->_1 ge#(x,0()) -> c_3():9 -->_1 ge#(s(x),s(y)) -> c_5(ge#(x,y)):2 3:S:help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) -->_1 towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)):7 -->_2 exp#(x,0()) -> c_1():8 -->_2 exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)):1 4:S:plus#(s(x),y) -> c_9(plus#(x,y)) -->_1 plus#(0(),x) -> c_8():12 -->_1 plus#(s(x),y) -> c_9(plus#(x,y)):4 5:S:times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) -->_2 times#(0(),y) -> c_10():13 -->_1 plus#(0(),x) -> c_8():12 -->_2 times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)):5 -->_1 plus#(s(x),y) -> c_9(plus#(x,y)):4 6:S:tower#(x,y) -> c_12(towerIter#(0(),x,y,s(0()))) -->_1 towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)):7 7:S:towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) -->_1 help#(true(),c,x,y,z) -> c_7():11 -->_2 ge#(0(),s(x)) -> c_4():10 -->_2 ge#(x,0()) -> c_3():9 -->_1 help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)):3 -->_2 ge#(s(x),s(y)) -> c_5(ge#(x,y)):2 8:W:exp#(x,0()) -> c_1() 9:W:ge#(x,0()) -> c_3() 10:W:ge#(0(),s(x)) -> c_4() 11:W:help#(true(),c,x,y,z) -> c_7() 12:W:plus#(0(),x) -> c_8() 13:W:times#(0(),y) -> c_10() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 11: help#(true(),c,x,y,z) -> c_7() 9: ge#(x,0()) -> c_3() 10: ge#(0(),s(x)) -> c_4() 8: exp#(x,0()) -> c_1() 12: plus#(0(),x) -> c_8() 13: times#(0(),y) -> c_10() * Step 5: RemoveHeads MAYBE + Considered Problem: - Strict DPs: exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) ge#(s(x),s(y)) -> c_5(ge#(x,y)) help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) plus#(s(x),y) -> c_9(plus#(x,y)) times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) tower#(x,y) -> c_12(towerIter#(0(),x,y,s(0()))) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) -->_1 times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)):5 -->_2 exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)):1 2:S:ge#(s(x),s(y)) -> c_5(ge#(x,y)) -->_1 ge#(s(x),s(y)) -> c_5(ge#(x,y)):2 3:S:help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) -->_1 towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)):7 -->_2 exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)):1 4:S:plus#(s(x),y) -> c_9(plus#(x,y)) -->_1 plus#(s(x),y) -> c_9(plus#(x,y)):4 5:S:times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) -->_2 times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)):5 -->_1 plus#(s(x),y) -> c_9(plus#(x,y)):4 6:S:tower#(x,y) -> c_12(towerIter#(0(),x,y,s(0()))) -->_1 towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)):7 7:S:towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) -->_1 help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)):3 -->_2 ge#(s(x),s(y)) -> c_5(ge#(x,y)):2 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,tower#(x,y) -> c_12(towerIter#(0(),x,y,s(0()))))] * Step 6: Decompose MAYBE + Considered Problem: - Strict DPs: exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) ge#(s(x),s(y)) -> c_5(ge#(x,y)) help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) plus#(s(x),y) -> c_9(plus#(x,y)) times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,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: exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) plus#(s(x),y) -> c_9(plus#(x,y)) times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) - Weak DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0 ,c_11/2,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} Problem (S) - Strict DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak DPs: exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) plus#(s(x),y) -> c_9(plus#(x,y)) times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0 ,c_11/2,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} ** Step 6.a:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) plus#(s(x),y) -> c_9(plus#(x,y)) times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) - Weak DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) -->_1 times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)):5 -->_2 exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)):1 2:W:ge#(s(x),s(y)) -> c_5(ge#(x,y)) -->_1 ge#(s(x),s(y)) -> c_5(ge#(x,y)):2 3:W:help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) -->_2 exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)):1 -->_1 towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)):7 4:S:plus#(s(x),y) -> c_9(plus#(x,y)) -->_1 plus#(s(x),y) -> c_9(plus#(x,y)):4 5:S:times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) -->_1 plus#(s(x),y) -> c_9(plus#(x,y)):4 -->_2 times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)):5 7:W:towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) -->_2 ge#(s(x),s(y)) -> c_5(ge#(x,y)):2 -->_1 help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: ge#(s(x),s(y)) -> c_5(ge#(x,y)) ** Step 6.a:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) plus#(s(x),y) -> c_9(plus#(x,y)) times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) - Weak DPs: help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) -->_1 times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)):5 -->_2 exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)):1 3:W:help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) -->_2 exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)):1 -->_1 towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)):7 4:S:plus#(s(x),y) -> c_9(plus#(x,y)) -->_1 plus#(s(x),y) -> c_9(plus#(x,y)):4 5:S:times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) -->_1 plus#(s(x),y) -> c_9(plus#(x,y)):4 -->_2 times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)):5 7:W:towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) -->_1 help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z)) ** Step 6.a:3: Failure MAYBE + Considered Problem: - Strict DPs: exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) plus#(s(x),y) -> c_9(plus#(x,y)) times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) - Weak DPs: help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/1} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. ** Step 6.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak DPs: exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) plus#(s(x),y) -> c_9(plus#(x,y)) times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:ge#(s(x),s(y)) -> c_5(ge#(x,y)) -->_1 ge#(s(x),s(y)) -> c_5(ge#(x,y)):1 2:S:help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) -->_2 exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)):4 -->_1 towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)):3 3:S:towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) -->_1 help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)):2 -->_2 ge#(s(x),s(y)) -> c_5(ge#(x,y)):1 4:W:exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) -->_1 times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)):6 -->_2 exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)):4 5:W:plus#(s(x),y) -> c_9(plus#(x,y)) -->_1 plus#(s(x),y) -> c_9(plus#(x,y)):5 6:W:times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) -->_2 times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)):6 -->_1 plus#(s(x),y) -> c_9(plus#(x,y)):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: exp#(x,s(y)) -> c_2(times#(x,exp(x,y)),exp#(x,y)) 6: times#(s(x),y) -> c_11(plus#(y,times(x,y)),times#(x,y)) 5: plus#(s(x),y) -> c_9(plus#(x,y)) ** Step 6.b:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:ge#(s(x),s(y)) -> c_5(ge#(x,y)) -->_1 ge#(s(x),s(y)) -> c_5(ge#(x,y)):1 2:S:help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)) -->_1 towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)):3 3:S:towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) -->_1 help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z)),exp#(y,z)):2 -->_2 ge#(s(x),s(y)) -> c_5(ge#(x,y)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z))) ** Step 6.b:3: Decompose MAYBE + Considered Problem: - Strict DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z))) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,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: ge#(s(x),s(y)) -> c_5(ge#(x,y)) - Weak DPs: help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z))) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/0 ,c_11/2,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} Problem (S) - Strict DPs: help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z))) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/0 ,c_11/2,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} *** Step 6.b:3.a:1: Failure MAYBE + Considered Problem: - Strict DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) - Weak DPs: help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z))) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. *** Step 6.b:3.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z))) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak DPs: ge#(s(x),s(y)) -> c_5(ge#(x,y)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z))) -->_1 towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)):2 2:S:towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) -->_2 ge#(s(x),s(y)) -> c_5(ge#(x,y)):3 -->_1 help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z))):1 3:W:ge#(s(x),s(y)) -> c_5(ge#(x,y)) -->_1 ge#(s(x),s(y)) -> c_5(ge#(x,y)):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: ge#(s(x),s(y)) -> c_5(ge#(x,y)) *** Step 6.b:3.b:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z))) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z))) -->_1 towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)):2 2:S:towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z),ge#(c,x)) -->_1 help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z))):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z)) *** Step 6.b:3.b:3: Failure MAYBE + Considered Problem: - Strict DPs: help#(false(),c,x,y,z) -> c_6(towerIter#(s(c),x,y,exp(y,z))) towerIter#(c,x,y,z) -> c_13(help#(ge(c,x),c,x,y,z)) - Weak TRS: exp(x,0()) -> s(0()) exp(x,s(y)) -> times(x,exp(x,y)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) 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: {exp/2,ge/2,help/5,plus/2,times/2,tower/2,towerIter/4,exp#/2,ge#/2,help#/5,plus#/2,times#/2,tower#/2 ,towerIter#/4} / {0/0,false/0,s/1,true/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2 ,c_12/1,c_13/1} - Obligation: innermost runtime complexity wrt. defined symbols {exp#,ge#,help#,plus#,times#,tower# ,towerIter#} and constructors {0,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE