MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: cond1(false(),n,l) -> cond2(gt(n,max(l)),n,l) cond1(true(),n,l) -> cons(n,st(s(n),l)) cond2(false(),n,l) -> st(s(n),l) cond2(true(),n,l) -> nil() equal(0(),0()) -> true() equal(0(),s(y)) -> false() equal(s(x),0()) -> false() equal(s(x),s(y)) -> equal(x,y) gt(0(),v) -> false() gt(s(u),0()) -> true() gt(s(u),s(v)) -> gt(u,v) if(false(),u,v) -> v if(true(),u,v) -> u max(cons(u,l)) -> if(gt(u,max(l)),u,max(l)) max(nil()) -> 0() member(n,cons(m,l)) -> or(equal(n,m),member(n,l)) member(n,nil()) -> false() or(x,false()) -> x or(x,true()) -> true() sort(l) -> st(0(),l) st(n,l) -> cond1(member(n,l),n,l) - Signature: {cond1/3,cond2/3,equal/2,gt/2,if/3,max/1,member/2,or/2,sort/1,st/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {cond1,cond2,equal,gt,if,max,member,or,sort ,st} and constructors {0,cons,false,nil,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)) cond1#(true(),n,l) -> c_2(st#(s(n),l)) cond2#(false(),n,l) -> c_3(st#(s(n),l)) cond2#(true(),n,l) -> c_4() equal#(0(),0()) -> c_5() equal#(0(),s(y)) -> c_6() equal#(s(x),0()) -> c_7() equal#(s(x),s(y)) -> c_8(equal#(x,y)) gt#(0(),v) -> c_9() gt#(s(u),0()) -> c_10() gt#(s(u),s(v)) -> c_11(gt#(u,v)) if#(false(),u,v) -> c_12() if#(true(),u,v) -> c_13() max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)) max#(nil()) -> c_15() member#(n,cons(m,l)) -> c_16(or#(equal(n,m),member(n,l)),equal#(n,m),member#(n,l)) member#(n,nil()) -> c_17() or#(x,false()) -> c_18() or#(x,true()) -> c_19() sort#(l) -> c_20(st#(0(),l)) st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)) cond1#(true(),n,l) -> c_2(st#(s(n),l)) cond2#(false(),n,l) -> c_3(st#(s(n),l)) cond2#(true(),n,l) -> c_4() equal#(0(),0()) -> c_5() equal#(0(),s(y)) -> c_6() equal#(s(x),0()) -> c_7() equal#(s(x),s(y)) -> c_8(equal#(x,y)) gt#(0(),v) -> c_9() gt#(s(u),0()) -> c_10() gt#(s(u),s(v)) -> c_11(gt#(u,v)) if#(false(),u,v) -> c_12() if#(true(),u,v) -> c_13() max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)) max#(nil()) -> c_15() member#(n,cons(m,l)) -> c_16(or#(equal(n,m),member(n,l)),equal#(n,m),member#(n,l)) member#(n,nil()) -> c_17() or#(x,false()) -> c_18() or#(x,true()) -> c_19() sort#(l) -> c_20(st#(0(),l)) st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)) - Weak TRS: cond1(false(),n,l) -> cond2(gt(n,max(l)),n,l) cond1(true(),n,l) -> cons(n,st(s(n),l)) cond2(false(),n,l) -> st(s(n),l) cond2(true(),n,l) -> nil() equal(0(),0()) -> true() equal(0(),s(y)) -> false() equal(s(x),0()) -> false() equal(s(x),s(y)) -> equal(x,y) gt(0(),v) -> false() gt(s(u),0()) -> true() gt(s(u),s(v)) -> gt(u,v) if(false(),u,v) -> v if(true(),u,v) -> u max(cons(u,l)) -> if(gt(u,max(l)),u,max(l)) max(nil()) -> 0() member(n,cons(m,l)) -> or(equal(n,m),member(n,l)) member(n,nil()) -> false() or(x,false()) -> x or(x,true()) -> true() sort(l) -> st(0(),l) st(n,l) -> cond1(member(n,l),n,l) - Signature: {cond1/3,cond2/3,equal/2,gt/2,if/3,max/1,member/2,or/2,sort/1,st/2,cond1#/3,cond2#/3,equal#/2,gt#/2,if#/3 ,max#/1,member#/2,or#/2,sort#/1,st#/2} / {0/0,cons/2,false/0,nil/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/1,c_12/0,c_13/0,c_14/4,c_15/0,c_16/3,c_17/0,c_18/0,c_19/0,c_20/1 ,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {cond1#,cond2#,equal#,gt#,if#,max#,member#,or#,sort# ,st#} and constructors {0,cons,false,nil,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: equal(0(),0()) -> true() equal(0(),s(y)) -> false() equal(s(x),0()) -> false() equal(s(x),s(y)) -> equal(x,y) gt(0(),v) -> false() gt(s(u),0()) -> true() gt(s(u),s(v)) -> gt(u,v) if(false(),u,v) -> v if(true(),u,v) -> u max(cons(u,l)) -> if(gt(u,max(l)),u,max(l)) max(nil()) -> 0() member(n,cons(m,l)) -> or(equal(n,m),member(n,l)) member(n,nil()) -> false() or(x,false()) -> x or(x,true()) -> true() cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)) cond1#(true(),n,l) -> c_2(st#(s(n),l)) cond2#(false(),n,l) -> c_3(st#(s(n),l)) cond2#(true(),n,l) -> c_4() equal#(0(),0()) -> c_5() equal#(0(),s(y)) -> c_6() equal#(s(x),0()) -> c_7() equal#(s(x),s(y)) -> c_8(equal#(x,y)) gt#(0(),v) -> c_9() gt#(s(u),0()) -> c_10() gt#(s(u),s(v)) -> c_11(gt#(u,v)) if#(false(),u,v) -> c_12() if#(true(),u,v) -> c_13() max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)) max#(nil()) -> c_15() member#(n,cons(m,l)) -> c_16(or#(equal(n,m),member(n,l)),equal#(n,m),member#(n,l)) member#(n,nil()) -> c_17() or#(x,false()) -> c_18() or#(x,true()) -> c_19() sort#(l) -> c_20(st#(0(),l)) st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)) cond1#(true(),n,l) -> c_2(st#(s(n),l)) cond2#(false(),n,l) -> c_3(st#(s(n),l)) cond2#(true(),n,l) -> c_4() equal#(0(),0()) -> c_5() equal#(0(),s(y)) -> c_6() equal#(s(x),0()) -> c_7() equal#(s(x),s(y)) -> c_8(equal#(x,y)) gt#(0(),v) -> c_9() gt#(s(u),0()) -> c_10() gt#(s(u),s(v)) -> c_11(gt#(u,v)) if#(false(),u,v) -> c_12() if#(true(),u,v) -> c_13() max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)) max#(nil()) -> c_15() member#(n,cons(m,l)) -> c_16(or#(equal(n,m),member(n,l)),equal#(n,m),member#(n,l)) member#(n,nil()) -> c_17() or#(x,false()) -> c_18() or#(x,true()) -> c_19() sort#(l) -> c_20(st#(0(),l)) st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)) - Weak TRS: equal(0(),0()) -> true() equal(0(),s(y)) -> false() equal(s(x),0()) -> false() equal(s(x),s(y)) -> equal(x,y) gt(0(),v) -> false() gt(s(u),0()) -> true() gt(s(u),s(v)) -> gt(u,v) if(false(),u,v) -> v if(true(),u,v) -> u max(cons(u,l)) -> if(gt(u,max(l)),u,max(l)) max(nil()) -> 0() member(n,cons(m,l)) -> or(equal(n,m),member(n,l)) member(n,nil()) -> false() or(x,false()) -> x or(x,true()) -> true() - Signature: {cond1/3,cond2/3,equal/2,gt/2,if/3,max/1,member/2,or/2,sort/1,st/2,cond1#/3,cond2#/3,equal#/2,gt#/2,if#/3 ,max#/1,member#/2,or#/2,sort#/1,st#/2} / {0/0,cons/2,false/0,nil/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/1,c_12/0,c_13/0,c_14/4,c_15/0,c_16/3,c_17/0,c_18/0,c_19/0,c_20/1 ,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {cond1#,cond2#,equal#,gt#,if#,max#,member#,or#,sort# ,st#} and constructors {0,cons,false,nil,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,12,13,15,17,18,19} by application of Pre({4,5,6,7,9,10,12,13,15,17,18,19}) = {1,8,11,14,16,21}. Here rules are labelled as follows: 1: cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)) 2: cond1#(true(),n,l) -> c_2(st#(s(n),l)) 3: cond2#(false(),n,l) -> c_3(st#(s(n),l)) 4: cond2#(true(),n,l) -> c_4() 5: equal#(0(),0()) -> c_5() 6: equal#(0(),s(y)) -> c_6() 7: equal#(s(x),0()) -> c_7() 8: equal#(s(x),s(y)) -> c_8(equal#(x,y)) 9: gt#(0(),v) -> c_9() 10: gt#(s(u),0()) -> c_10() 11: gt#(s(u),s(v)) -> c_11(gt#(u,v)) 12: if#(false(),u,v) -> c_12() 13: if#(true(),u,v) -> c_13() 14: max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)) 15: max#(nil()) -> c_15() 16: member#(n,cons(m,l)) -> c_16(or#(equal(n,m),member(n,l)),equal#(n,m),member#(n,l)) 17: member#(n,nil()) -> c_17() 18: or#(x,false()) -> c_18() 19: or#(x,true()) -> c_19() 20: sort#(l) -> c_20(st#(0(),l)) 21: st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)) cond1#(true(),n,l) -> c_2(st#(s(n),l)) cond2#(false(),n,l) -> c_3(st#(s(n),l)) equal#(s(x),s(y)) -> c_8(equal#(x,y)) gt#(s(u),s(v)) -> c_11(gt#(u,v)) max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)) member#(n,cons(m,l)) -> c_16(or#(equal(n,m),member(n,l)),equal#(n,m),member#(n,l)) sort#(l) -> c_20(st#(0(),l)) st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)) - Weak DPs: cond2#(true(),n,l) -> c_4() equal#(0(),0()) -> c_5() equal#(0(),s(y)) -> c_6() equal#(s(x),0()) -> c_7() gt#(0(),v) -> c_9() gt#(s(u),0()) -> c_10() if#(false(),u,v) -> c_12() if#(true(),u,v) -> c_13() max#(nil()) -> c_15() member#(n,nil()) -> c_17() or#(x,false()) -> c_18() or#(x,true()) -> c_19() - Weak TRS: equal(0(),0()) -> true() equal(0(),s(y)) -> false() equal(s(x),0()) -> false() equal(s(x),s(y)) -> equal(x,y) gt(0(),v) -> false() gt(s(u),0()) -> true() gt(s(u),s(v)) -> gt(u,v) if(false(),u,v) -> v if(true(),u,v) -> u max(cons(u,l)) -> if(gt(u,max(l)),u,max(l)) max(nil()) -> 0() member(n,cons(m,l)) -> or(equal(n,m),member(n,l)) member(n,nil()) -> false() or(x,false()) -> x or(x,true()) -> true() - Signature: {cond1/3,cond2/3,equal/2,gt/2,if/3,max/1,member/2,or/2,sort/1,st/2,cond1#/3,cond2#/3,equal#/2,gt#/2,if#/3 ,max#/1,member#/2,or#/2,sort#/1,st#/2} / {0/0,cons/2,false/0,nil/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/1,c_12/0,c_13/0,c_14/4,c_15/0,c_16/3,c_17/0,c_18/0,c_19/0,c_20/1 ,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {cond1#,cond2#,equal#,gt#,if#,max#,member#,or#,sort# ,st#} and constructors {0,cons,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)) -->_3 max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)):6 -->_2 gt#(s(u),s(v)) -> c_11(gt#(u,v)):5 -->_1 cond2#(false(),n,l) -> c_3(st#(s(n),l)):3 -->_3 max#(nil()) -> c_15():18 -->_2 gt#(s(u),0()) -> c_10():15 -->_2 gt#(0(),v) -> c_9():14 -->_1 cond2#(true(),n,l) -> c_4():10 2:S:cond1#(true(),n,l) -> c_2(st#(s(n),l)) -->_1 st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)):9 3:S:cond2#(false(),n,l) -> c_3(st#(s(n),l)) -->_1 st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)):9 4:S:equal#(s(x),s(y)) -> c_8(equal#(x,y)) -->_1 equal#(s(x),0()) -> c_7():13 -->_1 equal#(0(),s(y)) -> c_6():12 -->_1 equal#(0(),0()) -> c_5():11 -->_1 equal#(s(x),s(y)) -> c_8(equal#(x,y)):4 5:S:gt#(s(u),s(v)) -> c_11(gt#(u,v)) -->_1 gt#(s(u),0()) -> c_10():15 -->_1 gt#(0(),v) -> c_9():14 -->_1 gt#(s(u),s(v)) -> c_11(gt#(u,v)):5 6:S:max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)) -->_4 max#(nil()) -> c_15():18 -->_3 max#(nil()) -> c_15():18 -->_1 if#(true(),u,v) -> c_13():17 -->_1 if#(false(),u,v) -> c_12():16 -->_2 gt#(s(u),0()) -> c_10():15 -->_2 gt#(0(),v) -> c_9():14 -->_4 max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)):6 -->_3 max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)):6 -->_2 gt#(s(u),s(v)) -> c_11(gt#(u,v)):5 7:S:member#(n,cons(m,l)) -> c_16(or#(equal(n,m),member(n,l)),equal#(n,m),member#(n,l)) -->_1 or#(x,true()) -> c_19():21 -->_1 or#(x,false()) -> c_18():20 -->_3 member#(n,nil()) -> c_17():19 -->_2 equal#(s(x),0()) -> c_7():13 -->_2 equal#(0(),s(y)) -> c_6():12 -->_2 equal#(0(),0()) -> c_5():11 -->_3 member#(n,cons(m,l)) -> c_16(or#(equal(n,m),member(n,l)),equal#(n,m),member#(n,l)):7 -->_2 equal#(s(x),s(y)) -> c_8(equal#(x,y)):4 8:S:sort#(l) -> c_20(st#(0(),l)) -->_1 st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)):9 9:S:st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)) -->_2 member#(n,nil()) -> c_17():19 -->_2 member#(n,cons(m,l)) -> c_16(or#(equal(n,m),member(n,l)),equal#(n,m),member#(n,l)):7 -->_1 cond1#(true(),n,l) -> c_2(st#(s(n),l)):2 -->_1 cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)):1 10:W:cond2#(true(),n,l) -> c_4() 11:W:equal#(0(),0()) -> c_5() 12:W:equal#(0(),s(y)) -> c_6() 13:W:equal#(s(x),0()) -> c_7() 14:W:gt#(0(),v) -> c_9() 15:W:gt#(s(u),0()) -> c_10() 16:W:if#(false(),u,v) -> c_12() 17:W:if#(true(),u,v) -> c_13() 18:W:max#(nil()) -> c_15() 19:W:member#(n,nil()) -> c_17() 20:W:or#(x,false()) -> c_18() 21:W:or#(x,true()) -> c_19() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: cond2#(true(),n,l) -> c_4() 11: equal#(0(),0()) -> c_5() 12: equal#(0(),s(y)) -> c_6() 13: equal#(s(x),0()) -> c_7() 20: or#(x,false()) -> c_18() 21: or#(x,true()) -> c_19() 19: member#(n,nil()) -> c_17() 14: gt#(0(),v) -> c_9() 15: gt#(s(u),0()) -> c_10() 16: if#(false(),u,v) -> c_12() 17: if#(true(),u,v) -> c_13() 18: max#(nil()) -> c_15() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)) cond1#(true(),n,l) -> c_2(st#(s(n),l)) cond2#(false(),n,l) -> c_3(st#(s(n),l)) equal#(s(x),s(y)) -> c_8(equal#(x,y)) gt#(s(u),s(v)) -> c_11(gt#(u,v)) max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)) member#(n,cons(m,l)) -> c_16(or#(equal(n,m),member(n,l)),equal#(n,m),member#(n,l)) sort#(l) -> c_20(st#(0(),l)) st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)) - Weak TRS: equal(0(),0()) -> true() equal(0(),s(y)) -> false() equal(s(x),0()) -> false() equal(s(x),s(y)) -> equal(x,y) gt(0(),v) -> false() gt(s(u),0()) -> true() gt(s(u),s(v)) -> gt(u,v) if(false(),u,v) -> v if(true(),u,v) -> u max(cons(u,l)) -> if(gt(u,max(l)),u,max(l)) max(nil()) -> 0() member(n,cons(m,l)) -> or(equal(n,m),member(n,l)) member(n,nil()) -> false() or(x,false()) -> x or(x,true()) -> true() - Signature: {cond1/3,cond2/3,equal/2,gt/2,if/3,max/1,member/2,or/2,sort/1,st/2,cond1#/3,cond2#/3,equal#/2,gt#/2,if#/3 ,max#/1,member#/2,or#/2,sort#/1,st#/2} / {0/0,cons/2,false/0,nil/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/1,c_12/0,c_13/0,c_14/4,c_15/0,c_16/3,c_17/0,c_18/0,c_19/0,c_20/1 ,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {cond1#,cond2#,equal#,gt#,if#,max#,member#,or#,sort# ,st#} and constructors {0,cons,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)) -->_3 max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)):6 -->_2 gt#(s(u),s(v)) -> c_11(gt#(u,v)):5 -->_1 cond2#(false(),n,l) -> c_3(st#(s(n),l)):3 2:S:cond1#(true(),n,l) -> c_2(st#(s(n),l)) -->_1 st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)):9 3:S:cond2#(false(),n,l) -> c_3(st#(s(n),l)) -->_1 st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)):9 4:S:equal#(s(x),s(y)) -> c_8(equal#(x,y)) -->_1 equal#(s(x),s(y)) -> c_8(equal#(x,y)):4 5:S:gt#(s(u),s(v)) -> c_11(gt#(u,v)) -->_1 gt#(s(u),s(v)) -> c_11(gt#(u,v)):5 6:S:max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)) -->_4 max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)):6 -->_3 max#(cons(u,l)) -> c_14(if#(gt(u,max(l)),u,max(l)),gt#(u,max(l)),max#(l),max#(l)):6 -->_2 gt#(s(u),s(v)) -> c_11(gt#(u,v)):5 7:S:member#(n,cons(m,l)) -> c_16(or#(equal(n,m),member(n,l)),equal#(n,m),member#(n,l)) -->_3 member#(n,cons(m,l)) -> c_16(or#(equal(n,m),member(n,l)),equal#(n,m),member#(n,l)):7 -->_2 equal#(s(x),s(y)) -> c_8(equal#(x,y)):4 8:S:sort#(l) -> c_20(st#(0(),l)) -->_1 st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)):9 9:S:st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)) -->_2 member#(n,cons(m,l)) -> c_16(or#(equal(n,m),member(n,l)),equal#(n,m),member#(n,l)):7 -->_1 cond1#(true(),n,l) -> c_2(st#(s(n),l)):2 -->_1 cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: max#(cons(u,l)) -> c_14(gt#(u,max(l)),max#(l),max#(l)) member#(n,cons(m,l)) -> c_16(equal#(n,m),member#(n,l)) * Step 6: RemoveHeads MAYBE + Considered Problem: - Strict DPs: cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)) cond1#(true(),n,l) -> c_2(st#(s(n),l)) cond2#(false(),n,l) -> c_3(st#(s(n),l)) equal#(s(x),s(y)) -> c_8(equal#(x,y)) gt#(s(u),s(v)) -> c_11(gt#(u,v)) max#(cons(u,l)) -> c_14(gt#(u,max(l)),max#(l),max#(l)) member#(n,cons(m,l)) -> c_16(equal#(n,m),member#(n,l)) sort#(l) -> c_20(st#(0(),l)) st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)) - Weak TRS: equal(0(),0()) -> true() equal(0(),s(y)) -> false() equal(s(x),0()) -> false() equal(s(x),s(y)) -> equal(x,y) gt(0(),v) -> false() gt(s(u),0()) -> true() gt(s(u),s(v)) -> gt(u,v) if(false(),u,v) -> v if(true(),u,v) -> u max(cons(u,l)) -> if(gt(u,max(l)),u,max(l)) max(nil()) -> 0() member(n,cons(m,l)) -> or(equal(n,m),member(n,l)) member(n,nil()) -> false() or(x,false()) -> x or(x,true()) -> true() - Signature: {cond1/3,cond2/3,equal/2,gt/2,if/3,max/1,member/2,or/2,sort/1,st/2,cond1#/3,cond2#/3,equal#/2,gt#/2,if#/3 ,max#/1,member#/2,or#/2,sort#/1,st#/2} / {0/0,cons/2,false/0,nil/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/1,c_12/0,c_13/0,c_14/3,c_15/0,c_16/2,c_17/0,c_18/0,c_19/0,c_20/1 ,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {cond1#,cond2#,equal#,gt#,if#,max#,member#,or#,sort# ,st#} and constructors {0,cons,false,nil,s,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)) -->_3 max#(cons(u,l)) -> c_14(gt#(u,max(l)),max#(l),max#(l)):6 -->_2 gt#(s(u),s(v)) -> c_11(gt#(u,v)):5 -->_1 cond2#(false(),n,l) -> c_3(st#(s(n),l)):3 2:S:cond1#(true(),n,l) -> c_2(st#(s(n),l)) -->_1 st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)):9 3:S:cond2#(false(),n,l) -> c_3(st#(s(n),l)) -->_1 st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)):9 4:S:equal#(s(x),s(y)) -> c_8(equal#(x,y)) -->_1 equal#(s(x),s(y)) -> c_8(equal#(x,y)):4 5:S:gt#(s(u),s(v)) -> c_11(gt#(u,v)) -->_1 gt#(s(u),s(v)) -> c_11(gt#(u,v)):5 6:S:max#(cons(u,l)) -> c_14(gt#(u,max(l)),max#(l),max#(l)) -->_3 max#(cons(u,l)) -> c_14(gt#(u,max(l)),max#(l),max#(l)):6 -->_2 max#(cons(u,l)) -> c_14(gt#(u,max(l)),max#(l),max#(l)):6 -->_1 gt#(s(u),s(v)) -> c_11(gt#(u,v)):5 7:S:member#(n,cons(m,l)) -> c_16(equal#(n,m),member#(n,l)) -->_2 member#(n,cons(m,l)) -> c_16(equal#(n,m),member#(n,l)):7 -->_1 equal#(s(x),s(y)) -> c_8(equal#(x,y)):4 8:S:sort#(l) -> c_20(st#(0(),l)) -->_1 st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)):9 9:S:st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)) -->_2 member#(n,cons(m,l)) -> c_16(equal#(n,m),member#(n,l)):7 -->_1 cond1#(true(),n,l) -> c_2(st#(s(n),l)):2 -->_1 cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)):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). [(8,sort#(l) -> c_20(st#(0(),l)))] * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: cond1#(false(),n,l) -> c_1(cond2#(gt(n,max(l)),n,l),gt#(n,max(l)),max#(l)) cond1#(true(),n,l) -> c_2(st#(s(n),l)) cond2#(false(),n,l) -> c_3(st#(s(n),l)) equal#(s(x),s(y)) -> c_8(equal#(x,y)) gt#(s(u),s(v)) -> c_11(gt#(u,v)) max#(cons(u,l)) -> c_14(gt#(u,max(l)),max#(l),max#(l)) member#(n,cons(m,l)) -> c_16(equal#(n,m),member#(n,l)) st#(n,l) -> c_21(cond1#(member(n,l),n,l),member#(n,l)) - Weak TRS: equal(0(),0()) -> true() equal(0(),s(y)) -> false() equal(s(x),0()) -> false() equal(s(x),s(y)) -> equal(x,y) gt(0(),v) -> false() gt(s(u),0()) -> true() gt(s(u),s(v)) -> gt(u,v) if(false(),u,v) -> v if(true(),u,v) -> u max(cons(u,l)) -> if(gt(u,max(l)),u,max(l)) max(nil()) -> 0() member(n,cons(m,l)) -> or(equal(n,m),member(n,l)) member(n,nil()) -> false() or(x,false()) -> x or(x,true()) -> true() - Signature: {cond1/3,cond2/3,equal/2,gt/2,if/3,max/1,member/2,or/2,sort/1,st/2,cond1#/3,cond2#/3,equal#/2,gt#/2,if#/3 ,max#/1,member#/2,or#/2,sort#/1,st#/2} / {0/0,cons/2,false/0,nil/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/1,c_12/0,c_13/0,c_14/3,c_15/0,c_16/2,c_17/0,c_18/0,c_19/0,c_20/1 ,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {cond1#,cond2#,equal#,gt#,if#,max#,member#,or#,sort# ,st#} and constructors {0,cons,false,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE