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(false(),x,y,z) -> if2(eq(head(x),min(x)),x,y,z) if(true(),x,y,z) -> z if2(false(),x,y,z) -> mins(tail(x),add(head(x),y),z) if2(true(),x,y,z) -> mins(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) if_min(false(),add(n,add(m,x))) -> min(add(m,x)) if_min(true(),add(n,add(m,x))) -> min(add(n,x)) 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,add(m,x))) -> if_min(le(n,m),add(n,add(m,x))) min(add(n,nil())) -> n mins(x,y,z) -> if(null(x),x,y,z) minsort(x) -> mins(x,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/4,if2/4,if_min/2,if_rm/3,le/2,min/1,mins/3,minsort/1,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,if2,if_min,if_rm,le,min,mins,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#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),head#(x),min#(x)) if#(true(),x,y,z) -> c_9() if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z),tail#(x),head#(x)) if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,head#(x) ,tail#(x) ,app#(z,add(head(x),nil())) ,head#(x)) if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))) if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))) if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)) le#(0(),y) -> c_16() le#(s(x),0()) -> c_17() le#(s(x),s(y)) -> c_18(le#(x,y)) min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)) min#(add(n,nil())) -> c_20() mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)) minsort#(x) -> c_22(mins#(x,nil(),nil())) 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#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),head#(x),min#(x)) if#(true(),x,y,z) -> c_9() if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z),tail#(x),head#(x)) if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,head#(x) ,tail#(x) ,app#(z,add(head(x),nil())) ,head#(x)) if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))) if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))) if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)) le#(0(),y) -> c_16() le#(s(x),0()) -> c_17() le#(s(x),s(y)) -> c_18(le#(x,y)) min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)) min#(add(n,nil())) -> c_20() mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)) minsort#(x) -> c_22(mins#(x,nil(),nil())) 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(false(),x,y,z) -> if2(eq(head(x),min(x)),x,y,z) if(true(),x,y,z) -> z if2(false(),x,y,z) -> mins(tail(x),add(head(x),y),z) if2(true(),x,y,z) -> mins(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) if_min(false(),add(n,add(m,x))) -> min(add(m,x)) if_min(true(),add(n,add(m,x))) -> min(add(n,x)) 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,add(m,x))) -> if_min(le(n,m),add(n,add(m,x))) min(add(n,nil())) -> n mins(x,y,z) -> if(null(x),x,y,z) minsort(x) -> mins(x,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/4,if2/4,if_min/2,if_rm/3,le/2,min/1,mins/3,minsort/1,null/1,rm/2,tail/1,app#/2,eq#/2 ,head#/1,if#/4,if2#/4,if_min#/2,if_rm#/3,le#/2,min#/1,mins#/3,minsort#/1,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/4,c_9/0,c_10/3,c_11/7,c_12/1,c_13/1 ,c_14/1,c_15/1,c_16/0,c_17/0,c_18/1,c_19/2,c_20/0,c_21/2,c_22/1,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#,if2#,if_min#,if_rm#,le#,min#,mins# ,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) head(add(n,x)) -> n if_min(false(),add(n,add(m,x))) -> min(add(m,x)) if_min(true(),add(n,add(m,x))) -> min(add(n,x)) 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,add(m,x))) -> if_min(le(n,m),add(n,add(m,x))) min(add(n,nil())) -> n 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() 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#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),head#(x),min#(x)) if#(true(),x,y,z) -> c_9() if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z),tail#(x),head#(x)) if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,head#(x) ,tail#(x) ,app#(z,add(head(x),nil())) ,head#(x)) if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))) if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))) if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)) le#(0(),y) -> c_16() le#(s(x),0()) -> c_17() le#(s(x),s(y)) -> c_18(le#(x,y)) min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)) min#(add(n,nil())) -> c_20() mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)) minsort#(x) -> c_22(mins#(x,nil(),nil())) 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#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),head#(x),min#(x)) if#(true(),x,y,z) -> c_9() if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z),tail#(x),head#(x)) if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,head#(x) ,tail#(x) ,app#(z,add(head(x),nil())) ,head#(x)) if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))) if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))) if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)) le#(0(),y) -> c_16() le#(s(x),0()) -> c_17() le#(s(x),s(y)) -> c_18(le#(x,y)) min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)) min#(add(n,nil())) -> c_20() mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)) minsort#(x) -> c_22(mins#(x,nil(),nil())) 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(),add(n,add(m,x))) -> min(add(m,x)) if_min(true(),add(n,add(m,x))) -> min(add(n,x)) 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,add(m,x))) -> if_min(le(n,m),add(n,add(m,x))) min(add(n,nil())) -> n 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/4,if2/4,if_min/2,if_rm/3,le/2,min/1,mins/3,minsort/1,null/1,rm/2,tail/1,app#/2,eq#/2 ,head#/1,if#/4,if2#/4,if_min#/2,if_rm#/3,le#/2,min#/1,mins#/3,minsort#/1,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/4,c_9/0,c_10/3,c_11/7,c_12/1,c_13/1 ,c_14/1,c_15/1,c_16/0,c_17/0,c_18/1,c_19/2,c_20/0,c_21/2,c_22/1,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#,if2#,if_min#,if_rm#,le#,min#,mins# ,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,16,17,20,23,24,26,27,28} by application of Pre({2,3,4,5,7,9,16,17,20,23,24,26,27,28}) = {1,6,8,10,11,12,13,14,15,18,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#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),head#(x),min#(x)) 9: if#(true(),x,y,z) -> c_9() 10: if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z),tail#(x),head#(x)) 11: if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,head#(x) ,tail#(x) ,app#(z,add(head(x),nil())) ,head#(x)) 12: if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))) 13: if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))) 14: if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)) 15: if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)) 16: le#(0(),y) -> c_16() 17: le#(s(x),0()) -> c_17() 18: le#(s(x),s(y)) -> c_18(le#(x,y)) 19: min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)) 20: min#(add(n,nil())) -> c_20() 21: mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)) 22: minsort#(x) -> c_22(mins#(x,nil(),nil())) 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#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),head#(x),min#(x)) if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z),tail#(x),head#(x)) if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,head#(x) ,tail#(x) ,app#(z,add(head(x),nil())) ,head#(x)) if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))) if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))) if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)) le#(s(x),s(y)) -> c_18(le#(x,y)) min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)) mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)) minsort#(x) -> c_22(mins#(x,nil(),nil())) 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#(true(),x,y,z) -> c_9() le#(0(),y) -> c_16() le#(s(x),0()) -> c_17() min#(add(n,nil())) -> c_20() 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) head(add(n,x)) -> n if_min(false(),add(n,add(m,x))) -> min(add(m,x)) if_min(true(),add(n,add(m,x))) -> min(add(n,x)) 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,add(m,x))) -> if_min(le(n,m),add(n,add(m,x))) min(add(n,nil())) -> n 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/4,if2/4,if_min/2,if_rm/3,le/2,min/1,mins/3,minsort/1,null/1,rm/2,tail/1,app#/2,eq#/2 ,head#/1,if#/4,if2#/4,if_min#/2,if_rm#/3,le#/2,min#/1,mins#/3,minsort#/1,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/4,c_9/0,c_10/3,c_11/7,c_12/1,c_13/1 ,c_14/1,c_15/1,c_16/0,c_17/0,c_18/1,c_19/2,c_20/0,c_21/2,c_22/1,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#,if2#,if_min#,if_rm#,le#,min#,mins# ,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():15 -->_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():18 -->_1 eq#(0(),s(x)) -> c_4():17 -->_1 eq#(0(),0()) -> c_3():16 -->_1 eq#(s(x),s(y)) -> c_6(eq#(x,y)):2 3:S:if#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),head#(x),min#(x)) -->_4 min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)):11 -->_1 if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,head#(x) ,tail#(x) ,app#(z,add(head(x),nil())) ,head#(x)):5 -->_1 if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z),tail#(x),head#(x)):4 -->_4 min#(add(n,nil())) -> c_20():23 -->_3 head#(add(n,x)) -> c_7():19 -->_2 eq#(s(x),0()) -> c_5():18 -->_2 eq#(0(),s(x)) -> c_4():17 -->_2 eq#(0(),0()) -> c_3():16 -->_2 eq#(s(x),s(y)) -> c_6(eq#(x,y)):2 4:S:if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z),tail#(x),head#(x)) -->_1 mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)):12 -->_2 tail#(nil()) -> c_28():28 -->_2 tail#(add(n,x)) -> c_27():27 -->_3 head#(add(n,x)) -> c_7():19 5:S:if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,head#(x) ,tail#(x) ,app#(z,add(head(x),nil())) ,head#(x)) -->_3 rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)):14 -->_1 mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)):12 -->_5 tail#(nil()) -> c_28():28 -->_5 tail#(add(n,x)) -> c_27():27 -->_3 rm#(n,nil()) -> c_26():26 -->_7 head#(add(n,x)) -> c_7():19 -->_4 head#(add(n,x)) -> c_7():19 -->_6 app#(nil(),y) -> c_2():15 -->_2 app#(nil(),y) -> c_2():15 -->_6 app#(add(n,x),y) -> c_1(app#(x,y)):1 -->_2 app#(add(n,x),y) -> c_1(app#(x,y)):1 6:S:if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))) -->_1 min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)):11 -->_1 min#(add(n,nil())) -> c_20():23 7:S:if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))) -->_1 min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)):11 -->_1 min#(add(n,nil())) -> c_20():23 8:S:if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)) -->_1 rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)):14 -->_1 rm#(n,nil()) -> c_26():26 9:S:if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)) -->_1 rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)):14 -->_1 rm#(n,nil()) -> c_26():26 10:S:le#(s(x),s(y)) -> c_18(le#(x,y)) -->_1 le#(s(x),0()) -> c_17():22 -->_1 le#(0(),y) -> c_16():21 -->_1 le#(s(x),s(y)) -> c_18(le#(x,y)):10 11:S:min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)) -->_2 le#(s(x),0()) -> c_17():22 -->_2 le#(0(),y) -> c_16():21 -->_2 le#(s(x),s(y)) -> c_18(le#(x,y)):10 -->_1 if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))):7 -->_1 if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))):6 12:S:mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)) -->_2 null#(nil()) -> c_24():25 -->_2 null#(add(n,x)) -> c_23():24 -->_1 if#(true(),x,y,z) -> c_9():20 -->_1 if#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),head#(x),min#(x)):3 13:S:minsort#(x) -> c_22(mins#(x,nil(),nil())) -->_1 mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)):12 14: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():18 -->_2 eq#(0(),s(x)) -> c_4():17 -->_2 eq#(0(),0()) -> c_3():16 -->_1 if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)):9 -->_1 if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)):8 -->_2 eq#(s(x),s(y)) -> c_6(eq#(x,y)):2 15:W:app#(nil(),y) -> c_2() 16:W:eq#(0(),0()) -> c_3() 17:W:eq#(0(),s(x)) -> c_4() 18:W:eq#(s(x),0()) -> c_5() 19:W:head#(add(n,x)) -> c_7() 20:W:if#(true(),x,y,z) -> c_9() 21:W:le#(0(),y) -> c_16() 22:W:le#(s(x),0()) -> c_17() 23:W:min#(add(n,nil())) -> c_20() 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. 19: head#(add(n,x)) -> c_7() 27: tail#(add(n,x)) -> c_27() 28: tail#(nil()) -> c_28() 20: if#(true(),x,y,z) -> c_9() 24: null#(add(n,x)) -> c_23() 25: null#(nil()) -> c_24() 26: rm#(n,nil()) -> c_26() 23: min#(add(n,nil())) -> c_20() 21: le#(0(),y) -> c_16() 22: le#(s(x),0()) -> c_17() 16: eq#(0(),0()) -> c_3() 17: eq#(0(),s(x)) -> c_4() 18: eq#(s(x),0()) -> c_5() 15: app#(nil(),y) -> c_2() * Step 5: SimplifyRHS 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#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),head#(x),min#(x)) if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z),tail#(x),head#(x)) if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,head#(x) ,tail#(x) ,app#(z,add(head(x),nil())) ,head#(x)) if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))) if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))) if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)) le#(s(x),s(y)) -> c_18(le#(x,y)) min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)) mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)) minsort#(x) -> c_22(mins#(x,nil(),nil())) 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) head(add(n,x)) -> n if_min(false(),add(n,add(m,x))) -> min(add(m,x)) if_min(true(),add(n,add(m,x))) -> min(add(n,x)) 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,add(m,x))) -> if_min(le(n,m),add(n,add(m,x))) min(add(n,nil())) -> n 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/4,if2/4,if_min/2,if_rm/3,le/2,min/1,mins/3,minsort/1,null/1,rm/2,tail/1,app#/2,eq#/2 ,head#/1,if#/4,if2#/4,if_min#/2,if_rm#/3,le#/2,min#/1,mins#/3,minsort#/1,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/4,c_9/0,c_10/3,c_11/7,c_12/1,c_13/1 ,c_14/1,c_15/1,c_16/0,c_17/0,c_18/1,c_19/2,c_20/0,c_21/2,c_22/1,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#,if2#,if_min#,if_rm#,le#,min#,mins# ,minsort#,null#,rm#,tail#} and constructors {0,add,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:app#(add(n,x),y) -> c_1(app#(x,y)) -->_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),s(y)) -> c_6(eq#(x,y)):2 3:S:if#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),head#(x),min#(x)) -->_4 min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)):11 -->_1 if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,head#(x) ,tail#(x) ,app#(z,add(head(x),nil())) ,head#(x)):5 -->_1 if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z),tail#(x),head#(x)):4 -->_2 eq#(s(x),s(y)) -> c_6(eq#(x,y)):2 4:S:if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z),tail#(x),head#(x)) -->_1 mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)):12 5:S:if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,head#(x) ,tail#(x) ,app#(z,add(head(x),nil())) ,head#(x)) -->_3 rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)):14 -->_1 mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)):12 -->_6 app#(add(n,x),y) -> c_1(app#(x,y)):1 -->_2 app#(add(n,x),y) -> c_1(app#(x,y)):1 6:S:if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))) -->_1 min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)):11 7:S:if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))) -->_1 min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)):11 8:S:if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)) -->_1 rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)):14 9:S:if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)) -->_1 rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)):14 10:S:le#(s(x),s(y)) -> c_18(le#(x,y)) -->_1 le#(s(x),s(y)) -> c_18(le#(x,y)):10 11:S:min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)) -->_2 le#(s(x),s(y)) -> c_18(le#(x,y)):10 -->_1 if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))):7 -->_1 if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))):6 12:S:mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)) -->_1 if#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),head#(x),min#(x)):3 13:S:minsort#(x) -> c_22(mins#(x,nil(),nil())) -->_1 mins#(x,y,z) -> c_21(if#(null(x),x,y,z),null#(x)):12 14:S:rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)) -->_1 if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)):9 -->_1 if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)):8 -->_2 eq#(s(x),s(y)) -> c_6(eq#(x,y)):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(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),min#(x)) if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z)) if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,app#(z,add(head(x),nil()))) mins#(x,y,z) -> c_21(if#(null(x),x,y,z)) * Step 6: RemoveHeads 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#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),min#(x)) if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z)) if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,app#(z,add(head(x),nil()))) if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))) if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))) if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)) le#(s(x),s(y)) -> c_18(le#(x,y)) min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)) mins#(x,y,z) -> c_21(if#(null(x),x,y,z)) minsort#(x) -> c_22(mins#(x,nil(),nil())) 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) head(add(n,x)) -> n if_min(false(),add(n,add(m,x))) -> min(add(m,x)) if_min(true(),add(n,add(m,x))) -> min(add(n,x)) 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,add(m,x))) -> if_min(le(n,m),add(n,add(m,x))) min(add(n,nil())) -> n 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/4,if2/4,if_min/2,if_rm/3,le/2,min/1,mins/3,minsort/1,null/1,rm/2,tail/1,app#/2,eq#/2 ,head#/1,if#/4,if2#/4,if_min#/2,if_rm#/3,le#/2,min#/1,mins#/3,minsort#/1,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/3,c_9/0,c_10/1,c_11/4,c_12/1,c_13/1 ,c_14/1,c_15/1,c_16/0,c_17/0,c_18/1,c_19/2,c_20/0,c_21/1,c_22/1,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#,if2#,if_min#,if_rm#,le#,min#,mins# ,minsort#,null#,rm#,tail#} and constructors {0,add,false,nil,s,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:app#(add(n,x),y) -> c_1(app#(x,y)) -->_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),s(y)) -> c_6(eq#(x,y)):2 3:S:if#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),min#(x)) -->_3 min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)):11 -->_1 if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,app#(z,add(head(x),nil()))):5 -->_1 if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z)):4 -->_2 eq#(s(x),s(y)) -> c_6(eq#(x,y)):2 4:S:if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z)) -->_1 mins#(x,y,z) -> c_21(if#(null(x),x,y,z)):12 5:S:if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,app#(z,add(head(x),nil()))) -->_3 rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)):14 -->_1 mins#(x,y,z) -> c_21(if#(null(x),x,y,z)):12 -->_4 app#(add(n,x),y) -> c_1(app#(x,y)):1 -->_2 app#(add(n,x),y) -> c_1(app#(x,y)):1 6:S:if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))) -->_1 min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)):11 7:S:if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))) -->_1 min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)):11 8:S:if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)) -->_1 rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)):14 9:S:if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)) -->_1 rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)):14 10:S:le#(s(x),s(y)) -> c_18(le#(x,y)) -->_1 le#(s(x),s(y)) -> c_18(le#(x,y)):10 11:S:min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)) -->_2 le#(s(x),s(y)) -> c_18(le#(x,y)):10 -->_1 if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))):7 -->_1 if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))):6 12:S:mins#(x,y,z) -> c_21(if#(null(x),x,y,z)) -->_1 if#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),min#(x)):3 13:S:minsort#(x) -> c_22(mins#(x,nil(),nil())) -->_1 mins#(x,y,z) -> c_21(if#(null(x),x,y,z)):12 14:S:rm#(n,add(m,x)) -> c_25(if_rm#(eq(n,m),n,add(m,x)),eq#(n,m)) -->_1 if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)):9 -->_1 if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)):8 -->_2 eq#(s(x),s(y)) -> c_6(eq#(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). [(13,minsort#(x) -> c_22(mins#(x,nil(),nil())))] * Step 7: 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#(false(),x,y,z) -> c_8(if2#(eq(head(x),min(x)),x,y,z),eq#(head(x),min(x)),min#(x)) if2#(false(),x,y,z) -> c_10(mins#(tail(x),add(head(x),y),z)) if2#(true(),x,y,z) -> c_11(mins#(app(rm(head(x),tail(x)),y),nil(),app(z,add(head(x),nil()))) ,app#(rm(head(x),tail(x)),y) ,rm#(head(x),tail(x)) ,app#(z,add(head(x),nil()))) if_min#(false(),add(n,add(m,x))) -> c_12(min#(add(m,x))) if_min#(true(),add(n,add(m,x))) -> c_13(min#(add(n,x))) if_rm#(false(),n,add(m,x)) -> c_14(rm#(n,x)) if_rm#(true(),n,add(m,x)) -> c_15(rm#(n,x)) le#(s(x),s(y)) -> c_18(le#(x,y)) min#(add(n,add(m,x))) -> c_19(if_min#(le(n,m),add(n,add(m,x))),le#(n,m)) mins#(x,y,z) -> c_21(if#(null(x),x,y,z)) 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) head(add(n,x)) -> n if_min(false(),add(n,add(m,x))) -> min(add(m,x)) if_min(true(),add(n,add(m,x))) -> min(add(n,x)) 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,add(m,x))) -> if_min(le(n,m),add(n,add(m,x))) min(add(n,nil())) -> n 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/4,if2/4,if_min/2,if_rm/3,le/2,min/1,mins/3,minsort/1,null/1,rm/2,tail/1,app#/2,eq#/2 ,head#/1,if#/4,if2#/4,if_min#/2,if_rm#/3,le#/2,min#/1,mins#/3,minsort#/1,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/3,c_9/0,c_10/1,c_11/4,c_12/1,c_13/1 ,c_14/1,c_15/1,c_16/0,c_17/0,c_18/1,c_19/2,c_20/0,c_21/1,c_22/1,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#,if2#,if_min#,if_rm#,le#,min#,mins# ,minsort#,null#,rm#,tail#} and constructors {0,add,false,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE