MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x not(x) -> if(x,false(),true()) plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y times(x,0()) -> 0() times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z))) times(x,s(y)) -> plus(times(x,y),x) - Signature: {gt/2,id/1,if/3,not/1,plus/2,times/2} / {0/0,false/0,s/1,true/0,zero/0} - Obligation: innermost runtime complexity wrt. defined symbols {gt,id,if,not,plus,times} and constructors {0,false,s,true ,zero} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x not(x) -> if(x,false(),true()) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y times(x,0()) -> 0() times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z))) times(x,s(y)) -> plus(times(x,y),x) - Signature: {gt/2,id/1,if/3,not/1,plus/2,times/2} / {0/0,false/0,s/1,true/0,zero/0} - Obligation: innermost runtime complexity wrt. defined symbols {gt,id,if,not,plus,times} and constructors {0,false,s,true ,zero} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs gt#(s(x),s(y)) -> c_1(gt#(x,y)) gt#(s(x),zero()) -> c_2() gt#(zero(),y) -> c_3() id#(x) -> c_4() if#(false(),x,y) -> c_5() if#(true(),x,y) -> c_6() not#(x) -> c_7(if#(x,false(),true())) plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) plus#(zero(),y) -> c_10() times#(x,0()) -> c_11() times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(s(z),0()) ,times#(x,s(z))) times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)) Weak DPs and mark the set of starting terms. * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: gt#(s(x),s(y)) -> c_1(gt#(x,y)) gt#(s(x),zero()) -> c_2() gt#(zero(),y) -> c_3() id#(x) -> c_4() if#(false(),x,y) -> c_5() if#(true(),x,y) -> c_6() not#(x) -> c_7(if#(x,false(),true())) plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) plus#(zero(),y) -> c_10() times#(x,0()) -> c_11() times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(s(z),0()) ,times#(x,s(z))) times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)) - Weak TRS: gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x not(x) -> if(x,false(),true()) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y times(x,0()) -> 0() times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z))) times(x,s(y)) -> plus(times(x,y),x) - Signature: {gt/2,id/1,if/3,not/1,plus/2,times/2,gt#/2,id#/1,if#/3,not#/1,plus#/2,times#/2} / {0/0,false/0,s/1,true/0 ,zero/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/5,c_9/8,c_10/0,c_11/0,c_12/5,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {gt#,id#,if#,not#,plus#,times#} and constructors {0,false ,s,true,zero} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3,4,5,6,10,11} by application of Pre({2,3,4,5,6,10,11}) = {1,7,8,9,12,13}. Here rules are labelled as follows: 1: gt#(s(x),s(y)) -> c_1(gt#(x,y)) 2: gt#(s(x),zero()) -> c_2() 3: gt#(zero(),y) -> c_3() 4: id#(x) -> c_4() 5: if#(false(),x,y) -> c_5() 6: if#(true(),x,y) -> c_6() 7: not#(x) -> c_7(if#(x,false(),true())) 8: plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) 9: plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) 10: plus#(zero(),y) -> c_10() 11: times#(x,0()) -> c_11() 12: times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(s(z),0()) ,times#(x,s(z))) 13: times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)) * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: gt#(s(x),s(y)) -> c_1(gt#(x,y)) not#(x) -> c_7(if#(x,false(),true())) plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(s(z),0()) ,times#(x,s(z))) times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)) - Weak DPs: gt#(s(x),zero()) -> c_2() gt#(zero(),y) -> c_3() id#(x) -> c_4() if#(false(),x,y) -> c_5() if#(true(),x,y) -> c_6() plus#(zero(),y) -> c_10() times#(x,0()) -> c_11() - Weak TRS: gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x not(x) -> if(x,false(),true()) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y times(x,0()) -> 0() times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z))) times(x,s(y)) -> plus(times(x,y),x) - Signature: {gt/2,id/1,if/3,not/1,plus/2,times/2,gt#/2,id#/1,if#/3,not#/1,plus#/2,times#/2} / {0/0,false/0,s/1,true/0 ,zero/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/5,c_9/8,c_10/0,c_11/0,c_12/5,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {gt#,id#,if#,not#,plus#,times#} and constructors {0,false ,s,true,zero} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2} by application of Pre({2}) = {4}. Here rules are labelled as follows: 1: gt#(s(x),s(y)) -> c_1(gt#(x,y)) 2: not#(x) -> c_7(if#(x,false(),true())) 3: plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) 4: plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) 5: times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(s(z),0()) ,times#(x,s(z))) 6: times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)) 7: gt#(s(x),zero()) -> c_2() 8: gt#(zero(),y) -> c_3() 9: id#(x) -> c_4() 10: if#(false(),x,y) -> c_5() 11: if#(true(),x,y) -> c_6() 12: plus#(zero(),y) -> c_10() 13: times#(x,0()) -> c_11() * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: gt#(s(x),s(y)) -> c_1(gt#(x,y)) plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(s(z),0()) ,times#(x,s(z))) times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)) - Weak DPs: gt#(s(x),zero()) -> c_2() gt#(zero(),y) -> c_3() id#(x) -> c_4() if#(false(),x,y) -> c_5() if#(true(),x,y) -> c_6() not#(x) -> c_7(if#(x,false(),true())) plus#(zero(),y) -> c_10() times#(x,0()) -> c_11() - Weak TRS: gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x not(x) -> if(x,false(),true()) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y times(x,0()) -> 0() times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z))) times(x,s(y)) -> plus(times(x,y),x) - Signature: {gt/2,id/1,if/3,not/1,plus/2,times/2,gt#/2,id#/1,if#/3,not#/1,plus#/2,times#/2} / {0/0,false/0,s/1,true/0 ,zero/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/5,c_9/8,c_10/0,c_11/0,c_12/5,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {gt#,id#,if#,not#,plus#,times#} and constructors {0,false ,s,true,zero} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:gt#(s(x),s(y)) -> c_1(gt#(x,y)) -->_1 gt#(zero(),y) -> c_3():7 -->_1 gt#(s(x),zero()) -> c_2():6 -->_1 gt#(s(x),s(y)) -> c_1(gt#(x,y)):1 2:S:plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)) -->_1 plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):3 -->_1 plus#(zero(),y) -> c_10():12 -->_2 if#(true(),x,y) -> c_6():10 -->_2 if#(false(),x,y) -> c_5():9 -->_5 id#(x) -> c_4():8 -->_4 id#(x) -> c_4():8 -->_3 gt#(zero(),y) -> c_3():7 -->_1 plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):2 -->_3 gt#(s(x),s(y)) -> c_1(gt#(x,y)):1 3:S:plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) -->_5 not#(x) -> c_7(if#(x,false(),true())):11 -->_1 plus#(zero(),y) -> c_10():12 -->_4 if#(true(),x,y) -> c_6():10 -->_2 if#(true(),x,y) -> c_6():10 -->_4 if#(false(),x,y) -> c_5():9 -->_2 if#(false(),x,y) -> c_5():9 -->_8 id#(x) -> c_4():8 -->_7 id#(x) -> c_4():8 -->_6 gt#(zero(),y) -> c_3():7 -->_3 gt#(zero(),y) -> c_3():7 -->_6 gt#(s(x),zero()) -> c_2():6 -->_3 gt#(s(x),zero()) -> c_2():6 -->_1 plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):3 -->_1 plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):2 -->_6 gt#(s(x),s(y)) -> c_1(gt#(x,y)):1 -->_3 gt#(s(x),s(y)) -> c_1(gt#(x,y)):1 4:S:times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(s(z),0()) ,times#(x,s(z))) -->_5 times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)):5 -->_2 times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)):5 -->_4 times#(x,0()) -> c_11():13 -->_2 times#(x,0()) -> c_11():13 -->_3 plus#(zero(),y) -> c_10():12 -->_1 plus#(zero(),y) -> c_10():12 -->_2 times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(s(z),0()) ,times#(x,s(z))):4 -->_3 plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):3 -->_1 plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):3 -->_3 plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):2 -->_1 plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):2 5:S:times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)) -->_2 times#(x,0()) -> c_11():13 -->_1 plus#(zero(),y) -> c_10():12 -->_2 times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)):5 -->_2 times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(s(z),0()) ,times#(x,s(z))):4 -->_1 plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):3 -->_1 plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):2 6:W:gt#(s(x),zero()) -> c_2() 7:W:gt#(zero(),y) -> c_3() 8:W:id#(x) -> c_4() 9:W:if#(false(),x,y) -> c_5() 10:W:if#(true(),x,y) -> c_6() 11:W:not#(x) -> c_7(if#(x,false(),true())) -->_1 if#(true(),x,y) -> c_6():10 -->_1 if#(false(),x,y) -> c_5():9 12:W:plus#(zero(),y) -> c_10() 13:W:times#(x,0()) -> c_11() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 13: times#(x,0()) -> c_11() 8: id#(x) -> c_4() 12: plus#(zero(),y) -> c_10() 11: not#(x) -> c_7(if#(x,false(),true())) 9: if#(false(),x,y) -> c_5() 10: if#(true(),x,y) -> c_6() 6: gt#(s(x),zero()) -> c_2() 7: gt#(zero(),y) -> c_3() * Step 6: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: gt#(s(x),s(y)) -> c_1(gt#(x,y)) plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(s(z),0()) ,times#(x,s(z))) times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)) - Weak TRS: gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x not(x) -> if(x,false(),true()) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y times(x,0()) -> 0() times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z))) times(x,s(y)) -> plus(times(x,y),x) - Signature: {gt/2,id/1,if/3,not/1,plus/2,times/2,gt#/2,id#/1,if#/3,not#/1,plus#/2,times#/2} / {0/0,false/0,s/1,true/0 ,zero/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/5,c_9/8,c_10/0,c_11/0,c_12/5,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {gt#,id#,if#,not#,plus#,times#} and constructors {0,false ,s,true,zero} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:gt#(s(x),s(y)) -> c_1(gt#(x,y)) -->_1 gt#(s(x),s(y)) -> c_1(gt#(x,y)):1 2:S:plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)) -->_1 plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):3 -->_1 plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):2 -->_3 gt#(s(x),s(y)) -> c_1(gt#(x,y)):1 3:S:plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) -->_1 plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):3 -->_1 plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):2 -->_6 gt#(s(x),s(y)) -> c_1(gt#(x,y)):1 -->_3 gt#(s(x),s(y)) -> c_1(gt#(x,y)):1 4:S:times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(s(z),0()) ,times#(x,s(z))) -->_5 times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)):5 -->_2 times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)):5 -->_2 times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(s(z),0()) ,times#(x,s(z))):4 -->_3 plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):3 -->_1 plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):3 -->_3 plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):2 -->_1 plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):2 5:S:times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)) -->_2 times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)):5 -->_2 times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(s(z),0()) ,times#(x,s(z))):4 -->_1 plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):3 -->_1 plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)),gt#(x,x)) plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))),gt#(x,y),gt#(x,y)) times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(x,s(z))) * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: gt#(s(x),s(y)) -> c_1(gt#(x,y)) plus#(s(x),x) -> c_8(plus#(if(gt(x,x),id(x),id(x)),s(x)),gt#(x,x)) plus#(s(x),s(y)) -> c_9(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))),gt#(x,y),gt#(x,y)) times#(x,plus(y,s(z))) -> c_12(plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ,times#(x,plus(y,times(s(z),0()))) ,plus#(y,times(s(z),0())) ,times#(x,s(z))) times#(x,s(y)) -> c_13(plus#(times(x,y),x),times#(x,y)) - Weak TRS: gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x not(x) -> if(x,false(),true()) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y times(x,0()) -> 0() times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z))) times(x,s(y)) -> plus(times(x,y),x) - Signature: {gt/2,id/1,if/3,not/1,plus/2,times/2,gt#/2,id#/1,if#/3,not#/1,plus#/2,times#/2} / {0/0,false/0,s/1,true/0 ,zero/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/2,c_9/3,c_10/0,c_11/0,c_12/4,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {gt#,id#,if#,not#,plus#,times#} and constructors {0,false ,s,true,zero} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE