MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) len(cons(x,xs)) -> s(len(xs)) len(nil()) -> 0() min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) - Signature: {addList/2,if/5,le/2,len/1,min/2,sum/2,take/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {addList,if,le,len,min,sum,take} and constructors {0,cons ,false,nil,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs addList#(x,y) -> c_1(if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) ,le#(0(),min(len(x),len(y))) ,min#(len(x),len(y)) ,len#(x) ,len#(y)) if#(false(),c,x,y,z) -> c_2() if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)) le#(0(),x) -> c_4() le#(s(x),0()) -> c_5() le#(s(x),s(y)) -> c_6(le#(x,y)) len#(cons(x,xs)) -> c_7(len#(xs)) len#(nil()) -> c_8() min#(0(),y) -> c_9() min#(s(x),0()) -> c_10() min#(s(x),s(y)) -> c_11(min#(x,y)) sum#(x,0()) -> c_12() sum#(x,s(y)) -> c_13(sum#(x,y)) take#(0(),cons(y,ys)) -> c_14() take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: addList#(x,y) -> c_1(if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) ,le#(0(),min(len(x),len(y))) ,min#(len(x),len(y)) ,len#(x) ,len#(y)) if#(false(),c,x,y,z) -> c_2() if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)) le#(0(),x) -> c_4() le#(s(x),0()) -> c_5() le#(s(x),s(y)) -> c_6(le#(x,y)) len#(cons(x,xs)) -> c_7(len#(xs)) len#(nil()) -> c_8() min#(0(),y) -> c_9() min#(s(x),0()) -> c_10() min#(s(x),s(y)) -> c_11(min#(x,y)) sum#(x,0()) -> c_12() sum#(x,s(y)) -> c_13(sum#(x,y)) take#(0(),cons(y,ys)) -> c_14() take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)) - Weak TRS: addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) len(cons(x,xs)) -> s(len(xs)) len(nil()) -> 0() min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) - Signature: {addList/2,if/5,le/2,len/1,min/2,sum/2,take/2,addList#/2,if#/5,le#/2,len#/1,min#/2,sum#/2,take#/2} / {0/0 ,cons/2,false/0,nil/0,s/1,true/0,c_1/5,c_2/0,c_3/8,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/1} - Obligation: innermost runtime complexity wrt. defined symbols {addList#,if#,le#,len#,min#,sum# ,take#} and constructors {0,cons,false,nil,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) len(cons(x,xs)) -> s(len(xs)) len(nil()) -> 0() min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList#(x,y) -> c_1(if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) ,le#(0(),min(len(x),len(y))) ,min#(len(x),len(y)) ,len#(x) ,len#(y)) if#(false(),c,x,y,z) -> c_2() if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)) le#(0(),x) -> c_4() le#(s(x),0()) -> c_5() le#(s(x),s(y)) -> c_6(le#(x,y)) len#(cons(x,xs)) -> c_7(len#(xs)) len#(nil()) -> c_8() min#(0(),y) -> c_9() min#(s(x),0()) -> c_10() min#(s(x),s(y)) -> c_11(min#(x,y)) sum#(x,0()) -> c_12() sum#(x,s(y)) -> c_13(sum#(x,y)) take#(0(),cons(y,ys)) -> c_14() take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: addList#(x,y) -> c_1(if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) ,le#(0(),min(len(x),len(y))) ,min#(len(x),len(y)) ,len#(x) ,len#(y)) if#(false(),c,x,y,z) -> c_2() if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)) le#(0(),x) -> c_4() le#(s(x),0()) -> c_5() le#(s(x),s(y)) -> c_6(le#(x,y)) len#(cons(x,xs)) -> c_7(len#(xs)) len#(nil()) -> c_8() min#(0(),y) -> c_9() min#(s(x),0()) -> c_10() min#(s(x),s(y)) -> c_11(min#(x,y)) sum#(x,0()) -> c_12() sum#(x,s(y)) -> c_13(sum#(x,y)) take#(0(),cons(y,ys)) -> c_14() take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)) - Weak TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) len(cons(x,xs)) -> s(len(xs)) len(nil()) -> 0() min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) - Signature: {addList/2,if/5,le/2,len/1,min/2,sum/2,take/2,addList#/2,if#/5,le#/2,len#/1,min#/2,sum#/2,take#/2} / {0/0 ,cons/2,false/0,nil/0,s/1,true/0,c_1/5,c_2/0,c_3/8,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/1} - Obligation: innermost runtime complexity wrt. defined symbols {addList#,if#,le#,len#,min#,sum# ,take#} 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,4,5,8,9,10,12,14} by application of Pre({2,4,5,8,9,10,12,14}) = {1,3,6,7,11,13,15}. Here rules are labelled as follows: 1: addList#(x,y) -> c_1(if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) ,le#(0(),min(len(x),len(y))) ,min#(len(x),len(y)) ,len#(x) ,len#(y)) 2: if#(false(),c,x,y,z) -> c_2() 3: if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)) 4: le#(0(),x) -> c_4() 5: le#(s(x),0()) -> c_5() 6: le#(s(x),s(y)) -> c_6(le#(x,y)) 7: len#(cons(x,xs)) -> c_7(len#(xs)) 8: len#(nil()) -> c_8() 9: min#(0(),y) -> c_9() 10: min#(s(x),0()) -> c_10() 11: min#(s(x),s(y)) -> c_11(min#(x,y)) 12: sum#(x,0()) -> c_12() 13: sum#(x,s(y)) -> c_13(sum#(x,y)) 14: take#(0(),cons(y,ys)) -> c_14() 15: take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: addList#(x,y) -> c_1(if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) ,le#(0(),min(len(x),len(y))) ,min#(len(x),len(y)) ,len#(x) ,len#(y)) if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)) le#(s(x),s(y)) -> c_6(le#(x,y)) len#(cons(x,xs)) -> c_7(len#(xs)) min#(s(x),s(y)) -> c_11(min#(x,y)) sum#(x,s(y)) -> c_13(sum#(x,y)) take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)) - Weak DPs: if#(false(),c,x,y,z) -> c_2() le#(0(),x) -> c_4() le#(s(x),0()) -> c_5() len#(nil()) -> c_8() min#(0(),y) -> c_9() min#(s(x),0()) -> c_10() sum#(x,0()) -> c_12() take#(0(),cons(y,ys)) -> c_14() - Weak TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) len(cons(x,xs)) -> s(len(xs)) len(nil()) -> 0() min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) - Signature: {addList/2,if/5,le/2,len/1,min/2,sum/2,take/2,addList#/2,if#/5,le#/2,len#/1,min#/2,sum#/2,take#/2} / {0/0 ,cons/2,false/0,nil/0,s/1,true/0,c_1/5,c_2/0,c_3/8,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/1} - Obligation: innermost runtime complexity wrt. defined symbols {addList#,if#,le#,len#,min#,sum# ,take#} and constructors {0,cons,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:addList#(x,y) -> c_1(if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) ,le#(0(),min(len(x),len(y))) ,min#(len(x),len(y)) ,len#(x) ,len#(y)) -->_3 min#(s(x),s(y)) -> c_11(min#(x,y)):5 -->_5 len#(cons(x,xs)) -> c_7(len#(xs)):4 -->_4 len#(cons(x,xs)) -> c_7(len#(xs)):4 -->_1 if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)):2 -->_3 min#(s(x),0()) -> c_10():13 -->_3 min#(0(),y) -> c_9():12 -->_5 len#(nil()) -> c_8():11 -->_4 len#(nil()) -> c_8():11 -->_2 le#(0(),x) -> c_4():9 -->_1 if#(false(),c,x,y,z) -> c_2():8 2:S:if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)) -->_8 take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)):7 -->_7 take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)):7 -->_6 sum#(x,s(y)) -> c_13(sum#(x,y)):6 -->_3 min#(s(x),s(y)) -> c_11(min#(x,y)):5 -->_5 len#(cons(x,xs)) -> c_7(len#(xs)):4 -->_4 len#(cons(x,xs)) -> c_7(len#(xs)):4 -->_2 le#(s(x),s(y)) -> c_6(le#(x,y)):3 -->_8 take#(0(),cons(y,ys)) -> c_14():15 -->_7 take#(0(),cons(y,ys)) -> c_14():15 -->_6 sum#(x,0()) -> c_12():14 -->_3 min#(s(x),0()) -> c_10():13 -->_3 min#(0(),y) -> c_9():12 -->_5 len#(nil()) -> c_8():11 -->_4 len#(nil()) -> c_8():11 -->_2 le#(s(x),0()) -> c_5():10 -->_1 if#(false(),c,x,y,z) -> c_2():8 -->_1 if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)):2 3:S:le#(s(x),s(y)) -> c_6(le#(x,y)) -->_1 le#(s(x),0()) -> c_5():10 -->_1 le#(0(),x) -> c_4():9 -->_1 le#(s(x),s(y)) -> c_6(le#(x,y)):3 4:S:len#(cons(x,xs)) -> c_7(len#(xs)) -->_1 len#(nil()) -> c_8():11 -->_1 len#(cons(x,xs)) -> c_7(len#(xs)):4 5:S:min#(s(x),s(y)) -> c_11(min#(x,y)) -->_1 min#(s(x),0()) -> c_10():13 -->_1 min#(0(),y) -> c_9():12 -->_1 min#(s(x),s(y)) -> c_11(min#(x,y)):5 6:S:sum#(x,s(y)) -> c_13(sum#(x,y)) -->_1 sum#(x,0()) -> c_12():14 -->_1 sum#(x,s(y)) -> c_13(sum#(x,y)):6 7:S:take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)) -->_1 take#(0(),cons(y,ys)) -> c_14():15 -->_1 take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)):7 8:W:if#(false(),c,x,y,z) -> c_2() 9:W:le#(0(),x) -> c_4() 10:W:le#(s(x),0()) -> c_5() 11:W:len#(nil()) -> c_8() 12:W:min#(0(),y) -> c_9() 13:W:min#(s(x),0()) -> c_10() 14:W:sum#(x,0()) -> c_12() 15:W:take#(0(),cons(y,ys)) -> c_14() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 8: if#(false(),c,x,y,z) -> c_2() 9: le#(0(),x) -> c_4() 10: le#(s(x),0()) -> c_5() 14: sum#(x,0()) -> c_12() 15: take#(0(),cons(y,ys)) -> c_14() 11: len#(nil()) -> c_8() 12: min#(0(),y) -> c_9() 13: min#(s(x),0()) -> c_10() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: addList#(x,y) -> c_1(if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) ,le#(0(),min(len(x),len(y))) ,min#(len(x),len(y)) ,len#(x) ,len#(y)) if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)) le#(s(x),s(y)) -> c_6(le#(x,y)) len#(cons(x,xs)) -> c_7(len#(xs)) min#(s(x),s(y)) -> c_11(min#(x,y)) sum#(x,s(y)) -> c_13(sum#(x,y)) take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)) - Weak TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) len(cons(x,xs)) -> s(len(xs)) len(nil()) -> 0() min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) - Signature: {addList/2,if/5,le/2,len/1,min/2,sum/2,take/2,addList#/2,if#/5,le#/2,len#/1,min#/2,sum#/2,take#/2} / {0/0 ,cons/2,false/0,nil/0,s/1,true/0,c_1/5,c_2/0,c_3/8,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/1} - Obligation: innermost runtime complexity wrt. defined symbols {addList#,if#,le#,len#,min#,sum# ,take#} and constructors {0,cons,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:addList#(x,y) -> c_1(if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) ,le#(0(),min(len(x),len(y))) ,min#(len(x),len(y)) ,len#(x) ,len#(y)) -->_3 min#(s(x),s(y)) -> c_11(min#(x,y)):5 -->_5 len#(cons(x,xs)) -> c_7(len#(xs)):4 -->_4 len#(cons(x,xs)) -> c_7(len#(xs)):4 -->_1 if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)):2 2:S:if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)) -->_8 take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)):7 -->_7 take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)):7 -->_6 sum#(x,s(y)) -> c_13(sum#(x,y)):6 -->_3 min#(s(x),s(y)) -> c_11(min#(x,y)):5 -->_5 len#(cons(x,xs)) -> c_7(len#(xs)):4 -->_4 len#(cons(x,xs)) -> c_7(len#(xs)):4 -->_2 le#(s(x),s(y)) -> c_6(le#(x,y)):3 -->_1 if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)):2 3:S:le#(s(x),s(y)) -> c_6(le#(x,y)) -->_1 le#(s(x),s(y)) -> c_6(le#(x,y)):3 4:S:len#(cons(x,xs)) -> c_7(len#(xs)) -->_1 len#(cons(x,xs)) -> c_7(len#(xs)):4 5:S:min#(s(x),s(y)) -> c_11(min#(x,y)) -->_1 min#(s(x),s(y)) -> c_11(min#(x,y)):5 6:S:sum#(x,s(y)) -> c_13(sum#(x,y)) -->_1 sum#(x,s(y)) -> c_13(sum#(x,y)):6 7:S:take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)) -->_1 take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)):7 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: addList#(x,y) -> c_1(if#(le(0(),min(len(x),len(y))),0(),x,y,nil()),min#(len(x),len(y)),len#(x),len#(y)) * Step 6: NaturalMI MAYBE + Considered Problem: - Strict DPs: addList#(x,y) -> c_1(if#(le(0(),min(len(x),len(y))),0(),x,y,nil()),min#(len(x),len(y)),len#(x),len#(y)) if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)) le#(s(x),s(y)) -> c_6(le#(x,y)) len#(cons(x,xs)) -> c_7(len#(xs)) min#(s(x),s(y)) -> c_11(min#(x,y)) sum#(x,s(y)) -> c_13(sum#(x,y)) take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)) - Weak TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) len(cons(x,xs)) -> s(len(xs)) len(nil()) -> 0() min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) - Signature: {addList/2,if/5,le/2,len/1,min/2,sum/2,take/2,addList#/2,if#/5,le#/2,len#/1,min#/2,sum#/2,take#/2} / {0/0 ,cons/2,false/0,nil/0,s/1,true/0,c_1/4,c_2/0,c_3/8,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/1} - Obligation: innermost runtime complexity wrt. defined symbols {addList#,if#,le#,len#,min#,sum# ,take#} and constructors {0,cons,false,nil,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_1) = {1,2,3,4}, uargs(c_3) = {1,2,3,4,5,6,7,8}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_11) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1} Following symbols are considered usable: {addList#,if#,le#,len#,min#,sum#,take#} TcT has computed the following interpretation: p(0) = [0] p(addList) = [0] p(cons) = [0] p(false) = [0] p(if) = [0] p(le) = [0] p(len) = [0] p(min) = [0] p(nil) = [0] p(s) = [0] p(sum) = [0] p(take) = [0] p(true) = [0] p(addList#) = [3] p(if#) = [1] p(le#) = [0] p(len#) = [0] p(min#) = [0] p(sum#) = [0] p(take#) = [0] p(c_1) = [1] x1 + [1] x2 + [2] x3 + [1] x4 + [0] p(c_2) = [0] p(c_3) = [1] x1 + [1] x2 + [2] x3 + [4] x4 + [1] x5 + [1] x6 + [4] x7 + [1] x8 + [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [4] x1 + [0] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [2] x1 + [0] p(c_12) = [0] p(c_13) = [4] x1 + [0] p(c_14) = [0] p(c_15) = [4] x1 + [0] Following rules are strictly oriented: addList#(x,y) = [3] > [1] = c_1(if#(le(0(),min(len(x),len(y))),0(),x,y,nil()),min#(len(x),len(y)),len#(x),len#(y)) Following rules are (at-least) weakly oriented: if#(true(),c,xs,ys,z) = [1] >= [1] = c_3(if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)) le#(s(x),s(y)) = [0] >= [0] = c_6(le#(x,y)) len#(cons(x,xs)) = [0] >= [0] = c_7(len#(xs)) min#(s(x),s(y)) = [0] >= [0] = c_11(min#(x,y)) sum#(x,s(y)) = [0] >= [0] = c_13(sum#(x,y)) take#(s(x),cons(y,ys)) = [0] >= [0] = c_15(take#(x,ys)) * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: if#(true(),c,xs,ys,z) -> c_3(if#(le(s(c),min(len(xs),len(ys))) ,s(c) ,xs ,ys ,cons(sum(take(c,xs),take(c,ys)),z)) ,le#(s(c),min(len(xs),len(ys))) ,min#(len(xs),len(ys)) ,len#(xs) ,len#(ys) ,sum#(take(c,xs),take(c,ys)) ,take#(c,xs) ,take#(c,ys)) le#(s(x),s(y)) -> c_6(le#(x,y)) len#(cons(x,xs)) -> c_7(len#(xs)) min#(s(x),s(y)) -> c_11(min#(x,y)) sum#(x,s(y)) -> c_13(sum#(x,y)) take#(s(x),cons(y,ys)) -> c_15(take#(x,ys)) - Weak DPs: addList#(x,y) -> c_1(if#(le(0(),min(len(x),len(y))),0(),x,y,nil()),min#(len(x),len(y)),len#(x),len#(y)) - Weak TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) len(cons(x,xs)) -> s(len(xs)) len(nil()) -> 0() min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) - Signature: {addList/2,if/5,le/2,len/1,min/2,sum/2,take/2,addList#/2,if#/5,le#/2,len#/1,min#/2,sum#/2,take#/2} / {0/0 ,cons/2,false/0,nil/0,s/1,true/0,c_1/4,c_2/0,c_3/8,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/1} - Obligation: innermost runtime complexity wrt. defined symbols {addList#,if#,le#,len#,min#,sum# ,take#} and constructors {0,cons,false,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE