MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: app(add(n,x),y) -> add(n,app(x,y)) app(nil(),y) -> y eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) head(add(n,x)) -> n if_min(false(),x,y,m) -> minIter(x,y,m) if_min(true(),x,y,m) -> m if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y)) if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil())) if_rm(false(),n,add(m,x)) -> add(m,rm(n,x)) if_rm(true(),n,add(m,x)) -> rm(n,x) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) min(add(n,x)) -> minIter(add(n,x),add(n,x),0()) min(nil()) -> 0() minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m) minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m)) minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y) minsort(nil(),nil()) -> nil() null(add(n,x)) -> false() null(nil()) -> true() rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x)) rm(n,nil()) -> nil() tail(add(n,x)) -> x tail(nil()) -> nil() - Signature: {app/2,eq/2,head/1,if_min/4,if_minsort/3,if_rm/3,le/2,min/1,minIter/3,minsort/2,null/1,rm/2,tail/1} / {0/0 ,add/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {app,eq,head,if_min,if_minsort,if_rm,le,min,minIter ,minsort,null,rm,tail} and constructors {0,add,false,nil,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs app#(add(n,x),y) -> c_1(app#(x,y)) app#(nil(),y) -> c_2() eq#(0(),0()) -> c_3() eq#(0(),s(x)) -> c_4() eq#(s(x),0()) -> c_5() eq#(s(x),s(y)) -> c_6(eq#(x,y)) head#(add(n,x)) -> c_7() if_min#(false(),x,y,m) -> c_8(minIter#(x,y,m)) if_min#(true(),x,y,m) -> c_9() if_minsort#(false(),add(n,x),y) -> c_10(minsort#(x,add(n,y))) if_minsort#(true(),add(n,x),y) -> c_11(minsort#(app(rm(n,x),y),nil()),app#(rm(n,x),y),rm#(n,x)) if_rm#(false(),n,add(m,x)) -> c_12(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_13(rm#(n,x)) le#(0(),y) -> c_14() le#(s(x),0()) -> c_15() le#(s(x),s(y)) -> c_16(le#(x,y)) min#(add(n,x)) -> c_17(minIter#(add(n,x),add(n,x),0())) min#(nil()) -> c_18() minIter#(add(n,x),y,m) -> c_19(if_min#(le(n,m),x,y,m),le#(n,m)) minIter#(nil(),add(n,y),m) -> c_20(minIter#(add(n,y),add(n,y),s(m))) minsort#(add(n,x),y) -> c_21(if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ,eq#(n,min(add(n,x))) ,min#(add(n,x))) minsort#(nil(),nil()) -> c_22() null#(add(n,x)) -> c_23() null#(nil()) -> c_24() rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)) rm#(n,nil()) -> c_26() tail#(add(n,x)) -> c_27() tail#(nil()) -> c_28() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: app#(add(n,x),y) -> c_1(app#(x,y)) app#(nil(),y) -> c_2() eq#(0(),0()) -> c_3() eq#(0(),s(x)) -> c_4() eq#(s(x),0()) -> c_5() eq#(s(x),s(y)) -> c_6(eq#(x,y)) head#(add(n,x)) -> c_7() if_min#(false(),x,y,m) -> c_8(minIter#(x,y,m)) if_min#(true(),x,y,m) -> c_9() if_minsort#(false(),add(n,x),y) -> c_10(minsort#(x,add(n,y))) if_minsort#(true(),add(n,x),y) -> c_11(minsort#(app(rm(n,x),y),nil()),app#(rm(n,x),y),rm#(n,x)) if_rm#(false(),n,add(m,x)) -> c_12(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_13(rm#(n,x)) le#(0(),y) -> c_14() le#(s(x),0()) -> c_15() le#(s(x),s(y)) -> c_16(le#(x,y)) min#(add(n,x)) -> c_17(minIter#(add(n,x),add(n,x),0())) min#(nil()) -> c_18() minIter#(add(n,x),y,m) -> c_19(if_min#(le(n,m),x,y,m),le#(n,m)) minIter#(nil(),add(n,y),m) -> c_20(minIter#(add(n,y),add(n,y),s(m))) minsort#(add(n,x),y) -> c_21(if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ,eq#(n,min(add(n,x))) ,min#(add(n,x))) minsort#(nil(),nil()) -> c_22() null#(add(n,x)) -> c_23() null#(nil()) -> c_24() rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)) rm#(n,nil()) -> c_26() tail#(add(n,x)) -> c_27() tail#(nil()) -> c_28() - Weak TRS: app(add(n,x),y) -> add(n,app(x,y)) app(nil(),y) -> y eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) head(add(n,x)) -> n if_min(false(),x,y,m) -> minIter(x,y,m) if_min(true(),x,y,m) -> m if_minsort(false(),add(n,x),y) -> minsort(x,add(n,y)) if_minsort(true(),add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil())) if_rm(false(),n,add(m,x)) -> add(m,rm(n,x)) if_rm(true(),n,add(m,x)) -> rm(n,x) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) min(add(n,x)) -> minIter(add(n,x),add(n,x),0()) min(nil()) -> 0() minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m) minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m)) minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y) minsort(nil(),nil()) -> nil() null(add(n,x)) -> false() null(nil()) -> true() rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x)) rm(n,nil()) -> nil() tail(add(n,x)) -> x tail(nil()) -> nil() - Signature: {app/2,eq/2,head/1,if_min/4,if_minsort/3,if_rm/3,le/2,min/1,minIter/3,minsort/2,null/1,rm/2,tail/1,app#/2 ,eq#/2,head#/1,if_min#/4,if_minsort#/3,if_rm#/3,le#/2,min#/1,minIter#/3,minsort#/2,null#/1,rm#/2 ,tail#/1} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/1 ,c_11/3,c_12/1,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/0,c_19/2,c_20/1,c_21/3,c_22/0,c_23/0,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,eq#,head#,if_min#,if_minsort#,if_rm#,le#,min# ,minIter#,minsort#,null#,rm#,tail#} and constructors {0,add,false,nil,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: app(add(n,x),y) -> add(n,app(x,y)) app(nil(),y) -> y eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) if_min(false(),x,y,m) -> minIter(x,y,m) if_min(true(),x,y,m) -> m if_rm(false(),n,add(m,x)) -> add(m,rm(n,x)) if_rm(true(),n,add(m,x)) -> rm(n,x) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) min(add(n,x)) -> minIter(add(n,x),add(n,x),0()) minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m) minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m)) rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x)) rm(n,nil()) -> nil() app#(add(n,x),y) -> c_1(app#(x,y)) app#(nil(),y) -> c_2() eq#(0(),0()) -> c_3() eq#(0(),s(x)) -> c_4() eq#(s(x),0()) -> c_5() eq#(s(x),s(y)) -> c_6(eq#(x,y)) head#(add(n,x)) -> c_7() if_min#(false(),x,y,m) -> c_8(minIter#(x,y,m)) if_min#(true(),x,y,m) -> c_9() if_minsort#(false(),add(n,x),y) -> c_10(minsort#(x,add(n,y))) if_minsort#(true(),add(n,x),y) -> c_11(minsort#(app(rm(n,x),y),nil()),app#(rm(n,x),y),rm#(n,x)) if_rm#(false(),n,add(m,x)) -> c_12(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_13(rm#(n,x)) le#(0(),y) -> c_14() le#(s(x),0()) -> c_15() le#(s(x),s(y)) -> c_16(le#(x,y)) min#(add(n,x)) -> c_17(minIter#(add(n,x),add(n,x),0())) min#(nil()) -> c_18() minIter#(add(n,x),y,m) -> c_19(if_min#(le(n,m),x,y,m),le#(n,m)) minIter#(nil(),add(n,y),m) -> c_20(minIter#(add(n,y),add(n,y),s(m))) minsort#(add(n,x),y) -> c_21(if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ,eq#(n,min(add(n,x))) ,min#(add(n,x))) minsort#(nil(),nil()) -> c_22() null#(add(n,x)) -> c_23() null#(nil()) -> c_24() rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)) rm#(n,nil()) -> c_26() tail#(add(n,x)) -> c_27() tail#(nil()) -> c_28() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: app#(add(n,x),y) -> c_1(app#(x,y)) app#(nil(),y) -> c_2() eq#(0(),0()) -> c_3() eq#(0(),s(x)) -> c_4() eq#(s(x),0()) -> c_5() eq#(s(x),s(y)) -> c_6(eq#(x,y)) head#(add(n,x)) -> c_7() if_min#(false(),x,y,m) -> c_8(minIter#(x,y,m)) if_min#(true(),x,y,m) -> c_9() if_minsort#(false(),add(n,x),y) -> c_10(minsort#(x,add(n,y))) if_minsort#(true(),add(n,x),y) -> c_11(minsort#(app(rm(n,x),y),nil()),app#(rm(n,x),y),rm#(n,x)) if_rm#(false(),n,add(m,x)) -> c_12(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_13(rm#(n,x)) le#(0(),y) -> c_14() le#(s(x),0()) -> c_15() le#(s(x),s(y)) -> c_16(le#(x,y)) min#(add(n,x)) -> c_17(minIter#(add(n,x),add(n,x),0())) min#(nil()) -> c_18() minIter#(add(n,x),y,m) -> c_19(if_min#(le(n,m),x,y,m),le#(n,m)) minIter#(nil(),add(n,y),m) -> c_20(minIter#(add(n,y),add(n,y),s(m))) minsort#(add(n,x),y) -> c_21(if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ,eq#(n,min(add(n,x))) ,min#(add(n,x))) minsort#(nil(),nil()) -> c_22() null#(add(n,x)) -> c_23() null#(nil()) -> c_24() rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)) rm#(n,nil()) -> c_26() tail#(add(n,x)) -> c_27() tail#(nil()) -> c_28() - Weak TRS: app(add(n,x),y) -> add(n,app(x,y)) app(nil(),y) -> y eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) if_min(false(),x,y,m) -> minIter(x,y,m) if_min(true(),x,y,m) -> m if_rm(false(),n,add(m,x)) -> add(m,rm(n,x)) if_rm(true(),n,add(m,x)) -> rm(n,x) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) min(add(n,x)) -> minIter(add(n,x),add(n,x),0()) minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m) minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m)) rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x)) rm(n,nil()) -> nil() - Signature: {app/2,eq/2,head/1,if_min/4,if_minsort/3,if_rm/3,le/2,min/1,minIter/3,minsort/2,null/1,rm/2,tail/1,app#/2 ,eq#/2,head#/1,if_min#/4,if_minsort#/3,if_rm#/3,le#/2,min#/1,minIter#/3,minsort#/2,null#/1,rm#/2 ,tail#/1} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/1 ,c_11/3,c_12/1,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/0,c_19/2,c_20/1,c_21/3,c_22/0,c_23/0,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,eq#,head#,if_min#,if_minsort#,if_rm#,le#,min# ,minIter#,minsort#,null#,rm#,tail#} and constructors {0,add,false,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3,4,5,7,9,14,15,18,22,23,24,26,27,28} by application of Pre({2,3,4,5,7,9,14,15,18,22,23,24,26,27,28}) = {1,6,11,12,13,16,19,21,25}. Here rules are labelled as follows: 1: app#(add(n,x),y) -> c_1(app#(x,y)) 2: app#(nil(),y) -> c_2() 3: eq#(0(),0()) -> c_3() 4: eq#(0(),s(x)) -> c_4() 5: eq#(s(x),0()) -> c_5() 6: eq#(s(x),s(y)) -> c_6(eq#(x,y)) 7: head#(add(n,x)) -> c_7() 8: if_min#(false(),x,y,m) -> c_8(minIter#(x,y,m)) 9: if_min#(true(),x,y,m) -> c_9() 10: if_minsort#(false(),add(n,x),y) -> c_10(minsort#(x,add(n,y))) 11: if_minsort#(true(),add(n,x),y) -> c_11(minsort#(app(rm(n,x),y),nil()),app#(rm(n,x),y),rm#(n,x)) 12: if_rm#(false(),n,add(m,x)) -> c_12(rm#(n,x)) 13: if_rm#(true(),n,add(m,x)) -> c_13(rm#(n,x)) 14: le#(0(),y) -> c_14() 15: le#(s(x),0()) -> c_15() 16: le#(s(x),s(y)) -> c_16(le#(x,y)) 17: min#(add(n,x)) -> c_17(minIter#(add(n,x),add(n,x),0())) 18: min#(nil()) -> c_18() 19: minIter#(add(n,x),y,m) -> c_19(if_min#(le(n,m),x,y,m),le#(n,m)) 20: minIter#(nil(),add(n,y),m) -> c_20(minIter#(add(n,y),add(n,y),s(m))) 21: minsort#(add(n,x),y) -> c_21(if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ,eq#(n,min(add(n,x))) ,min#(add(n,x))) 22: minsort#(nil(),nil()) -> c_22() 23: null#(add(n,x)) -> c_23() 24: null#(nil()) -> c_24() 25: rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)) 26: rm#(n,nil()) -> c_26() 27: tail#(add(n,x)) -> c_27() 28: tail#(nil()) -> c_28() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: app#(add(n,x),y) -> c_1(app#(x,y)) eq#(s(x),s(y)) -> c_6(eq#(x,y)) if_min#(false(),x,y,m) -> c_8(minIter#(x,y,m)) if_minsort#(false(),add(n,x),y) -> c_10(minsort#(x,add(n,y))) if_minsort#(true(),add(n,x),y) -> c_11(minsort#(app(rm(n,x),y),nil()),app#(rm(n,x),y),rm#(n,x)) if_rm#(false(),n,add(m,x)) -> c_12(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_13(rm#(n,x)) le#(s(x),s(y)) -> c_16(le#(x,y)) min#(add(n,x)) -> c_17(minIter#(add(n,x),add(n,x),0())) minIter#(add(n,x),y,m) -> c_19(if_min#(le(n,m),x,y,m),le#(n,m)) minIter#(nil(),add(n,y),m) -> c_20(minIter#(add(n,y),add(n,y),s(m))) minsort#(add(n,x),y) -> c_21(if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ,eq#(n,min(add(n,x))) ,min#(add(n,x))) rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)) - Weak DPs: app#(nil(),y) -> c_2() eq#(0(),0()) -> c_3() eq#(0(),s(x)) -> c_4() eq#(s(x),0()) -> c_5() head#(add(n,x)) -> c_7() if_min#(true(),x,y,m) -> c_9() le#(0(),y) -> c_14() le#(s(x),0()) -> c_15() min#(nil()) -> c_18() minsort#(nil(),nil()) -> c_22() null#(add(n,x)) -> c_23() null#(nil()) -> c_24() rm#(n,nil()) -> c_26() tail#(add(n,x)) -> c_27() tail#(nil()) -> c_28() - Weak TRS: app(add(n,x),y) -> add(n,app(x,y)) app(nil(),y) -> y eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) if_min(false(),x,y,m) -> minIter(x,y,m) if_min(true(),x,y,m) -> m if_rm(false(),n,add(m,x)) -> add(m,rm(n,x)) if_rm(true(),n,add(m,x)) -> rm(n,x) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) min(add(n,x)) -> minIter(add(n,x),add(n,x),0()) minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m) minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m)) rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x)) rm(n,nil()) -> nil() - Signature: {app/2,eq/2,head/1,if_min/4,if_minsort/3,if_rm/3,le/2,min/1,minIter/3,minsort/2,null/1,rm/2,tail/1,app#/2 ,eq#/2,head#/1,if_min#/4,if_minsort#/3,if_rm#/3,le#/2,min#/1,minIter#/3,minsort#/2,null#/1,rm#/2 ,tail#/1} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/1 ,c_11/3,c_12/1,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/0,c_19/2,c_20/1,c_21/3,c_22/0,c_23/0,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,eq#,head#,if_min#,if_minsort#,if_rm#,le#,min# ,minIter#,minsort#,null#,rm#,tail#} and constructors {0,add,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:app#(add(n,x),y) -> c_1(app#(x,y)) -->_1 app#(nil(),y) -> c_2():14 -->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1 2:S:eq#(s(x),s(y)) -> c_6(eq#(x,y)) -->_1 eq#(s(x),0()) -> c_5():17 -->_1 eq#(0(),s(x)) -> c_4():16 -->_1 eq#(0(),0()) -> c_3():15 -->_1 eq#(s(x),s(y)) -> c_6(eq#(x,y)):2 3:S:if_min#(false(),x,y,m) -> c_8(minIter#(x,y,m)) -->_1 minIter#(nil(),add(n,y),m) -> c_20(minIter#(add(n,y),add(n,y),s(m))):11 -->_1 minIter#(add(n,x),y,m) -> c_19(if_min#(le(n,m),x,y,m),le#(n,m)):10 4:S:if_minsort#(false(),add(n,x),y) -> c_10(minsort#(x,add(n,y))) -->_1 minsort#(add(n,x),y) -> c_21(if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ,eq#(n,min(add(n,x))) ,min#(add(n,x))):12 5:S:if_minsort#(true(),add(n,x),y) -> c_11(minsort#(app(rm(n,x),y),nil()),app#(rm(n,x),y),rm#(n,x)) -->_3 rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)):13 -->_1 minsort#(add(n,x),y) -> c_21(if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ,eq#(n,min(add(n,x))) ,min#(add(n,x))):12 -->_3 rm#(n,nil()) -> c_26():26 -->_1 minsort#(nil(),nil()) -> c_22():23 -->_2 app#(nil(),y) -> c_2():14 -->_2 app#(add(n,x),y) -> c_1(app#(x,y)):1 6:S:if_rm#(false(),n,add(m,x)) -> c_12(rm#(n,x)) -->_1 rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)):13 -->_1 rm#(n,nil()) -> c_26():26 7:S:if_rm#(true(),n,add(m,x)) -> c_13(rm#(n,x)) -->_1 rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)):13 -->_1 rm#(n,nil()) -> c_26():26 8:S:le#(s(x),s(y)) -> c_16(le#(x,y)) -->_1 le#(s(x),0()) -> c_15():21 -->_1 le#(0(),y) -> c_14():20 -->_1 le#(s(x),s(y)) -> c_16(le#(x,y)):8 9:S:min#(add(n,x)) -> c_17(minIter#(add(n,x),add(n,x),0())) -->_1 minIter#(add(n,x),y,m) -> c_19(if_min#(le(n,m),x,y,m),le#(n,m)):10 10:S:minIter#(add(n,x),y,m) -> c_19(if_min#(le(n,m),x,y,m),le#(n,m)) -->_2 le#(s(x),0()) -> c_15():21 -->_2 le#(0(),y) -> c_14():20 -->_1 if_min#(true(),x,y,m) -> c_9():19 -->_2 le#(s(x),s(y)) -> c_16(le#(x,y)):8 -->_1 if_min#(false(),x,y,m) -> c_8(minIter#(x,y,m)):3 11:S:minIter#(nil(),add(n,y),m) -> c_20(minIter#(add(n,y),add(n,y),s(m))) -->_1 minIter#(add(n,x),y,m) -> c_19(if_min#(le(n,m),x,y,m),le#(n,m)):10 12:S:minsort#(add(n,x),y) -> c_21(if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ,eq#(n,min(add(n,x))) ,min#(add(n,x))) -->_2 eq#(s(x),0()) -> c_5():17 -->_2 eq#(0(),s(x)) -> c_4():16 -->_2 eq#(0(),0()) -> c_3():15 -->_3 min#(add(n,x)) -> c_17(minIter#(add(n,x),add(n,x),0())):9 -->_1 if_minsort#(true(),add(n,x),y) -> c_11(minsort#(app(rm(n,x),y),nil()),app#(rm(n,x),y),rm#(n,x)):5 -->_1 if_minsort#(false(),add(n,x),y) -> c_10(minsort#(x,add(n,y))):4 -->_2 eq#(s(x),s(y)) -> c_6(eq#(x,y)):2 13:S:rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)) -->_2 eq#(s(x),0()) -> c_5():17 -->_2 eq#(0(),s(x)) -> c_4():16 -->_2 eq#(0(),0()) -> c_3():15 -->_1 if_rm#(true(),n,add(m,x)) -> c_13(rm#(n,x)):7 -->_1 if_rm#(false(),n,add(m,x)) -> c_12(rm#(n,x)):6 -->_2 eq#(s(x),s(y)) -> c_6(eq#(x,y)):2 14:W:app#(nil(),y) -> c_2() 15:W:eq#(0(),0()) -> c_3() 16:W:eq#(0(),s(x)) -> c_4() 17:W:eq#(s(x),0()) -> c_5() 18:W:head#(add(n,x)) -> c_7() 19:W:if_min#(true(),x,y,m) -> c_9() 20:W:le#(0(),y) -> c_14() 21:W:le#(s(x),0()) -> c_15() 22:W:min#(nil()) -> c_18() 23:W:minsort#(nil(),nil()) -> c_22() 24:W:null#(add(n,x)) -> c_23() 25:W:null#(nil()) -> c_24() 26:W:rm#(n,nil()) -> c_26() 27:W:tail#(add(n,x)) -> c_27() 28:W:tail#(nil()) -> c_28() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 28: tail#(nil()) -> c_28() 27: tail#(add(n,x)) -> c_27() 25: null#(nil()) -> c_24() 24: null#(add(n,x)) -> c_23() 22: min#(nil()) -> c_18() 18: head#(add(n,x)) -> c_7() 23: minsort#(nil(),nil()) -> c_22() 26: rm#(n,nil()) -> c_26() 19: if_min#(true(),x,y,m) -> c_9() 20: le#(0(),y) -> c_14() 21: le#(s(x),0()) -> c_15() 15: eq#(0(),0()) -> c_3() 16: eq#(0(),s(x)) -> c_4() 17: eq#(s(x),0()) -> c_5() 14: app#(nil(),y) -> c_2() * Step 5: Failure MAYBE + Considered Problem: - Strict DPs: app#(add(n,x),y) -> c_1(app#(x,y)) eq#(s(x),s(y)) -> c_6(eq#(x,y)) if_min#(false(),x,y,m) -> c_8(minIter#(x,y,m)) if_minsort#(false(),add(n,x),y) -> c_10(minsort#(x,add(n,y))) if_minsort#(true(),add(n,x),y) -> c_11(minsort#(app(rm(n,x),y),nil()),app#(rm(n,x),y),rm#(n,x)) if_rm#(false(),n,add(m,x)) -> c_12(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_13(rm#(n,x)) le#(s(x),s(y)) -> c_16(le#(x,y)) min#(add(n,x)) -> c_17(minIter#(add(n,x),add(n,x),0())) minIter#(add(n,x),y,m) -> c_19(if_min#(le(n,m),x,y,m),le#(n,m)) minIter#(nil(),add(n,y),m) -> c_20(minIter#(add(n,y),add(n,y),s(m))) minsort#(add(n,x),y) -> c_21(if_minsort#(eq(n,min(add(n,x))),add(n,x),y) ,eq#(n,min(add(n,x))) ,min#(add(n,x))) rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)) - Weak TRS: app(add(n,x),y) -> add(n,app(x,y)) app(nil(),y) -> y eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) if_min(false(),x,y,m) -> minIter(x,y,m) if_min(true(),x,y,m) -> m if_rm(false(),n,add(m,x)) -> add(m,rm(n,x)) if_rm(true(),n,add(m,x)) -> rm(n,x) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) min(add(n,x)) -> minIter(add(n,x),add(n,x),0()) minIter(add(n,x),y,m) -> if_min(le(n,m),x,y,m) minIter(nil(),add(n,y),m) -> minIter(add(n,y),add(n,y),s(m)) rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x)) rm(n,nil()) -> nil() - Signature: {app/2,eq/2,head/1,if_min/4,if_minsort/3,if_rm/3,le/2,min/1,minIter/3,minsort/2,null/1,rm/2,tail/1,app#/2 ,eq#/2,head#/1,if_min#/4,if_minsort#/3,if_rm#/3,le#/2,min#/1,minIter#/3,minsort#/2,null#/1,rm#/2 ,tail#/1} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/1 ,c_11/3,c_12/1,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/0,c_19/2,c_20/1,c_21/3,c_22/0,c_23/0,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,eq#,head#,if_min#,if_minsort#,if_rm#,le#,min# ,minIter#,minsort#,null#,rm#,tail#} and constructors {0,add,false,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE