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