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