MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) append(nil(),ys()) -> ys() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) filterhigh(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) filterlow(n,nil()) -> nil() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) get(n,cons(x,nil())) -> x get(n,nil()) -> 0() get(0(),cons(x,cons(y,xs))) -> x get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) if1(true(),n,x,xs) -> filterlow(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) if2(true(),n,x,xs) -> filterhigh(n,xs) length(cons(x,xs)) -> s(length(xs)) length(nil()) -> 0() qs(n,cons(x,xs)) -> append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)),qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) qs(n,nil()) -> nil() qsort(xs) -> qs(half(length(xs)),xs) - Signature: {append/2,filterhigh/2,filterlow/2,ge/2,get/2,half/1,if1/4,if2/4,length/1,qs/2,qsort/1} / {0/0,cons/2 ,false/0,nil/0,s/1,true/0,ys/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,filterhigh,filterlow,ge,get,half,if1,if2,length,qs ,qsort} and constructors {0,cons,false,nil,s,true,ys} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())) append#(nil(),ys()) -> c_2() filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) filterhigh#(n,nil()) -> c_4() filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) filterlow#(n,nil()) -> c_6() ge#(x,0()) -> c_7() ge#(0(),s(x)) -> c_8() ge#(s(x),s(y)) -> c_9(ge#(x,y)) get#(n,cons(x,nil())) -> c_10() get#(n,nil()) -> c_11() get#(0(),cons(x,cons(y,xs))) -> c_12() get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))) half#(0()) -> c_14() half#(s(0())) -> c_15() half#(s(s(x))) -> c_16(half#(x)) if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)) if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)) if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)) if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)) length#(cons(x,xs)) -> c_21(length#(xs)) length#(nil()) -> c_22() qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) qs#(n,nil()) -> c_24() qsort#(xs) -> c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())) append#(nil(),ys()) -> c_2() filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) filterhigh#(n,nil()) -> c_4() filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) filterlow#(n,nil()) -> c_6() ge#(x,0()) -> c_7() ge#(0(),s(x)) -> c_8() ge#(s(x),s(y)) -> c_9(ge#(x,y)) get#(n,cons(x,nil())) -> c_10() get#(n,nil()) -> c_11() get#(0(),cons(x,cons(y,xs))) -> c_12() get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))) half#(0()) -> c_14() half#(s(0())) -> c_15() half#(s(s(x))) -> c_16(half#(x)) if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)) if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)) if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)) if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)) length#(cons(x,xs)) -> c_21(length#(xs)) length#(nil()) -> c_22() qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) qs#(n,nil()) -> c_24() qsort#(xs) -> c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) - Weak TRS: append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) append(nil(),ys()) -> ys() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) filterhigh(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) filterlow(n,nil()) -> nil() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) get(n,cons(x,nil())) -> x get(n,nil()) -> 0() get(0(),cons(x,cons(y,xs))) -> x get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) if1(true(),n,x,xs) -> filterlow(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) if2(true(),n,x,xs) -> filterhigh(n,xs) length(cons(x,xs)) -> s(length(xs)) length(nil()) -> 0() qs(n,cons(x,xs)) -> append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)),qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) qs(n,nil()) -> nil() qsort(xs) -> qs(half(length(xs)),xs) - Signature: {append/2,filterhigh/2,filterlow/2,ge/2,get/2,half/1,if1/4,if2/4,length/1,qs/2,qsort/1,append#/2 ,filterhigh#/2,filterlow#/2,ge#/2,get#/2,half#/1,if1#/4,if2#/4,length#/1,qs#/2,qsort#/1} / {0/0,cons/2 ,false/0,nil/0,s/1,true/0,ys/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/1,c_22/0,c_23/10,c_24/0,c_25/3} - Obligation: innermost runtime complexity wrt. defined symbols {append#,filterhigh#,filterlow#,ge#,get#,half#,if1#,if2# ,length#,qs#,qsort#} and constructors {0,cons,false,nil,s,true,ys} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) filterhigh(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) filterlow(n,nil()) -> nil() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) get(n,cons(x,nil())) -> x get(0(),cons(x,cons(y,xs))) -> x get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) if1(true(),n,x,xs) -> filterlow(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) if2(true(),n,x,xs) -> filterhigh(n,xs) length(cons(x,xs)) -> s(length(xs)) length(nil()) -> 0() qs(n,cons(x,xs)) -> append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)),qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) qs(n,nil()) -> nil() append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())) append#(nil(),ys()) -> c_2() filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) filterhigh#(n,nil()) -> c_4() filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) filterlow#(n,nil()) -> c_6() ge#(x,0()) -> c_7() ge#(0(),s(x)) -> c_8() ge#(s(x),s(y)) -> c_9(ge#(x,y)) get#(n,cons(x,nil())) -> c_10() get#(n,nil()) -> c_11() get#(0(),cons(x,cons(y,xs))) -> c_12() get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))) half#(0()) -> c_14() half#(s(0())) -> c_15() half#(s(s(x))) -> c_16(half#(x)) if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)) if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)) if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)) if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)) length#(cons(x,xs)) -> c_21(length#(xs)) length#(nil()) -> c_22() qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) qs#(n,nil()) -> c_24() qsort#(xs) -> c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())) append#(nil(),ys()) -> c_2() filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) filterhigh#(n,nil()) -> c_4() filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) filterlow#(n,nil()) -> c_6() ge#(x,0()) -> c_7() ge#(0(),s(x)) -> c_8() ge#(s(x),s(y)) -> c_9(ge#(x,y)) get#(n,cons(x,nil())) -> c_10() get#(n,nil()) -> c_11() get#(0(),cons(x,cons(y,xs))) -> c_12() get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))) half#(0()) -> c_14() half#(s(0())) -> c_15() half#(s(s(x))) -> c_16(half#(x)) if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)) if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)) if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)) if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)) length#(cons(x,xs)) -> c_21(length#(xs)) length#(nil()) -> c_22() qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) qs#(n,nil()) -> c_24() qsort#(xs) -> c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) - Weak TRS: filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) filterhigh(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) filterlow(n,nil()) -> nil() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) get(n,cons(x,nil())) -> x get(0(),cons(x,cons(y,xs))) -> x get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) if1(true(),n,x,xs) -> filterlow(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) if2(true(),n,x,xs) -> filterhigh(n,xs) length(cons(x,xs)) -> s(length(xs)) length(nil()) -> 0() qs(n,cons(x,xs)) -> append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)),qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) qs(n,nil()) -> nil() - Signature: {append/2,filterhigh/2,filterlow/2,ge/2,get/2,half/1,if1/4,if2/4,length/1,qs/2,qsort/1,append#/2 ,filterhigh#/2,filterlow#/2,ge#/2,get#/2,half#/1,if1#/4,if2#/4,length#/1,qs#/2,qsort#/1} / {0/0,cons/2 ,false/0,nil/0,s/1,true/0,ys/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/1,c_22/0,c_23/10,c_24/0,c_25/3} - Obligation: innermost runtime complexity wrt. defined symbols {append#,filterhigh#,filterlow#,ge#,get#,half#,if1#,if2# ,length#,qs#,qsort#} and constructors {0,cons,false,nil,s,true,ys} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,4,6,7,8,10,11,12,14,15,22,24} by application of Pre({2,4,6,7,8,10,11,12,14,15,22,24}) = {1,3,5,9,13,16,17,18,19,20,21,23,25}. Here rules are labelled as follows: 1: append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())) 2: append#(nil(),ys()) -> c_2() 3: filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) 4: filterhigh#(n,nil()) -> c_4() 5: filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) 6: filterlow#(n,nil()) -> c_6() 7: ge#(x,0()) -> c_7() 8: ge#(0(),s(x)) -> c_8() 9: ge#(s(x),s(y)) -> c_9(ge#(x,y)) 10: get#(n,cons(x,nil())) -> c_10() 11: get#(n,nil()) -> c_11() 12: get#(0(),cons(x,cons(y,xs))) -> c_12() 13: get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))) 14: half#(0()) -> c_14() 15: half#(s(0())) -> c_15() 16: half#(s(s(x))) -> c_16(half#(x)) 17: if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)) 18: if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)) 19: if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)) 20: if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)) 21: length#(cons(x,xs)) -> c_21(length#(xs)) 22: length#(nil()) -> c_22() 23: qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) 24: qs#(n,nil()) -> c_24() 25: qsort#(xs) -> c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())) filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) ge#(s(x),s(y)) -> c_9(ge#(x,y)) get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))) half#(s(s(x))) -> c_16(half#(x)) if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)) if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)) if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)) if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)) length#(cons(x,xs)) -> c_21(length#(xs)) qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) qsort#(xs) -> c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) - Weak DPs: append#(nil(),ys()) -> c_2() filterhigh#(n,nil()) -> c_4() filterlow#(n,nil()) -> c_6() ge#(x,0()) -> c_7() ge#(0(),s(x)) -> c_8() get#(n,cons(x,nil())) -> c_10() get#(n,nil()) -> c_11() get#(0(),cons(x,cons(y,xs))) -> c_12() half#(0()) -> c_14() half#(s(0())) -> c_15() length#(nil()) -> c_22() qs#(n,nil()) -> c_24() - Weak TRS: filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) filterhigh(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) filterlow(n,nil()) -> nil() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) get(n,cons(x,nil())) -> x get(0(),cons(x,cons(y,xs))) -> x get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) if1(true(),n,x,xs) -> filterlow(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) if2(true(),n,x,xs) -> filterhigh(n,xs) length(cons(x,xs)) -> s(length(xs)) length(nil()) -> 0() qs(n,cons(x,xs)) -> append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)),qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) qs(n,nil()) -> nil() - Signature: {append/2,filterhigh/2,filterlow/2,ge/2,get/2,half/1,if1/4,if2/4,length/1,qs/2,qsort/1,append#/2 ,filterhigh#/2,filterlow#/2,ge#/2,get#/2,half#/1,if1#/4,if2#/4,length#/1,qs#/2,qsort#/1} / {0/0,cons/2 ,false/0,nil/0,s/1,true/0,ys/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/1,c_22/0,c_23/10,c_24/0,c_25/3} - Obligation: innermost runtime complexity wrt. defined symbols {append#,filterhigh#,filterlow#,ge#,get#,half#,if1#,if2# ,length#,qs#,qsort#} and constructors {0,cons,false,nil,s,true,ys} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())) -->_1 append#(nil(),ys()) -> c_2():14 -->_1 append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())):1 2:S:filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) -->_1 if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)):10 -->_1 if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)):9 -->_2 ge#(s(x),s(y)) -> c_9(ge#(x,y)):4 -->_2 ge#(0(),s(x)) -> c_8():18 -->_2 ge#(x,0()) -> c_7():17 3:S:filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) -->_1 if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)):8 -->_1 if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)):7 -->_2 ge#(s(x),s(y)) -> c_9(ge#(x,y)):4 -->_2 ge#(0(),s(x)) -> c_8():18 -->_2 ge#(x,0()) -> c_7():17 4:S:ge#(s(x),s(y)) -> c_9(ge#(x,y)) -->_1 ge#(0(),s(x)) -> c_8():18 -->_1 ge#(x,0()) -> c_7():17 -->_1 ge#(s(x),s(y)) -> c_9(ge#(x,y)):4 5:S:get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))) -->_1 get#(0(),cons(x,cons(y,xs))) -> c_12():21 -->_1 get#(n,cons(x,nil())) -> c_10():19 -->_1 get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))):5 6:S:half#(s(s(x))) -> c_16(half#(x)) -->_1 half#(s(0())) -> c_15():23 -->_1 half#(0()) -> c_14():22 -->_1 half#(s(s(x))) -> c_16(half#(x)):6 7:S:if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)) -->_1 filterlow#(n,nil()) -> c_6():16 -->_1 filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)):3 8:S:if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)) -->_1 filterlow#(n,nil()) -> c_6():16 -->_1 filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)):3 9:S:if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)) -->_1 filterhigh#(n,nil()) -> c_4():15 -->_1 filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)):2 10:S:if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)) -->_1 filterhigh#(n,nil()) -> c_4():15 -->_1 filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)):2 11:S:length#(cons(x,xs)) -> c_21(length#(xs)) -->_1 length#(nil()) -> c_22():24 -->_1 length#(cons(x,xs)) -> c_21(length#(xs)):11 12:S:qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) -->_7 qs#(n,nil()) -> c_24():25 -->_2 qs#(n,nil()) -> c_24():25 -->_8 half#(s(0())) -> c_15():23 -->_3 half#(s(0())) -> c_15():23 -->_8 half#(0()) -> c_14():22 -->_3 half#(0()) -> c_14():22 -->_10 get#(0(),cons(x,cons(y,xs))) -> c_12():21 -->_6 get#(0(),cons(x,cons(y,xs))) -> c_12():21 -->_5 get#(0(),cons(x,cons(y,xs))) -> c_12():21 -->_10 get#(n,cons(x,nil())) -> c_10():19 -->_6 get#(n,cons(x,nil())) -> c_10():19 -->_5 get#(n,cons(x,nil())) -> c_10():19 -->_7 qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))):12 -->_2 qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))):12 -->_8 half#(s(s(x))) -> c_16(half#(x)):6 -->_3 half#(s(s(x))) -> c_16(half#(x)):6 -->_10 get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))):5 -->_6 get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))):5 -->_5 get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))):5 -->_4 filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)):3 -->_9 filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)):2 13:S:qsort#(xs) -> c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) -->_1 qs#(n,nil()) -> c_24():25 -->_3 length#(nil()) -> c_22():24 -->_2 half#(s(0())) -> c_15():23 -->_2 half#(0()) -> c_14():22 -->_1 qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))):12 -->_3 length#(cons(x,xs)) -> c_21(length#(xs)):11 -->_2 half#(s(s(x))) -> c_16(half#(x)):6 14:W:append#(nil(),ys()) -> c_2() 15:W:filterhigh#(n,nil()) -> c_4() 16:W:filterlow#(n,nil()) -> c_6() 17:W:ge#(x,0()) -> c_7() 18:W:ge#(0(),s(x)) -> c_8() 19:W:get#(n,cons(x,nil())) -> c_10() 20:W:get#(n,nil()) -> c_11() 21:W:get#(0(),cons(x,cons(y,xs))) -> c_12() 22:W:half#(0()) -> c_14() 23:W:half#(s(0())) -> c_15() 24:W:length#(nil()) -> c_22() 25:W:qs#(n,nil()) -> c_24() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 20: get#(n,nil()) -> c_11() 25: qs#(n,nil()) -> c_24() 24: length#(nil()) -> c_22() 22: half#(0()) -> c_14() 23: half#(s(0())) -> c_15() 19: get#(n,cons(x,nil())) -> c_10() 21: get#(0(),cons(x,cons(y,xs))) -> c_12() 16: filterlow#(n,nil()) -> c_6() 17: ge#(x,0()) -> c_7() 18: ge#(0(),s(x)) -> c_8() 15: filterhigh#(n,nil()) -> c_4() 14: append#(nil(),ys()) -> c_2() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())) filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) ge#(s(x),s(y)) -> c_9(ge#(x,y)) get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))) half#(s(s(x))) -> c_16(half#(x)) if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)) if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)) if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)) if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)) length#(cons(x,xs)) -> c_21(length#(xs)) qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) qsort#(xs) -> c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) - Weak TRS: filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) filterhigh(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) filterlow(n,nil()) -> nil() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) get(n,cons(x,nil())) -> x get(0(),cons(x,cons(y,xs))) -> x get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) if1(true(),n,x,xs) -> filterlow(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) if2(true(),n,x,xs) -> filterhigh(n,xs) length(cons(x,xs)) -> s(length(xs)) length(nil()) -> 0() qs(n,cons(x,xs)) -> append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)),qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) qs(n,nil()) -> nil() - Signature: {append/2,filterhigh/2,filterlow/2,ge/2,get/2,half/1,if1/4,if2/4,length/1,qs/2,qsort/1,append#/2 ,filterhigh#/2,filterlow#/2,ge#/2,get#/2,half#/1,if1#/4,if2#/4,length#/1,qs#/2,qsort#/1} / {0/0,cons/2 ,false/0,nil/0,s/1,true/0,ys/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/1,c_22/0,c_23/10,c_24/0,c_25/3} - Obligation: innermost runtime complexity wrt. defined symbols {append#,filterhigh#,filterlow#,ge#,get#,half#,if1#,if2# ,length#,qs#,qsort#} and constructors {0,cons,false,nil,s,true,ys} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())) -->_1 append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())):1 2:S:filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) -->_1 if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)):10 -->_1 if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)):9 -->_2 ge#(s(x),s(y)) -> c_9(ge#(x,y)):4 3:S:filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) -->_1 if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)):8 -->_1 if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)):7 -->_2 ge#(s(x),s(y)) -> c_9(ge#(x,y)):4 4:S:ge#(s(x),s(y)) -> c_9(ge#(x,y)) -->_1 ge#(s(x),s(y)) -> c_9(ge#(x,y)):4 5:S:get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))) -->_1 get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))):5 6:S:half#(s(s(x))) -> c_16(half#(x)) -->_1 half#(s(s(x))) -> c_16(half#(x)):6 7:S:if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)) -->_1 filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)):3 8:S:if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)) -->_1 filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)):3 9:S:if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)) -->_1 filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)):2 10:S:if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)) -->_1 filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)):2 11:S:length#(cons(x,xs)) -> c_21(length#(xs)) -->_1 length#(cons(x,xs)) -> c_21(length#(xs)):11 12:S:qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) -->_7 qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))):12 -->_2 qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))):12 -->_8 half#(s(s(x))) -> c_16(half#(x)):6 -->_3 half#(s(s(x))) -> c_16(half#(x)):6 -->_10 get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))):5 -->_6 get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))):5 -->_5 get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))):5 -->_4 filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)):3 -->_9 filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)):2 13:S:qsort#(xs) -> c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) -->_1 qs#(n,cons(x,xs)) -> c_23(append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)) ,qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) ,qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))):12 -->_3 length#(cons(x,xs)) -> c_21(length#(xs)):11 -->_2 half#(s(s(x))) -> c_16(half#(x)):6 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: qs#(n,cons(x,xs)) -> c_23(qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) * Step 6: UsableRules MAYBE + Considered Problem: - Strict DPs: append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())) filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) ge#(s(x),s(y)) -> c_9(ge#(x,y)) get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))) half#(s(s(x))) -> c_16(half#(x)) if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)) if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)) if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)) if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)) length#(cons(x,xs)) -> c_21(length#(xs)) qs#(n,cons(x,xs)) -> c_23(qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) qsort#(xs) -> c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) - Weak TRS: filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) filterhigh(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) filterlow(n,nil()) -> nil() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) get(n,cons(x,nil())) -> x get(0(),cons(x,cons(y,xs))) -> x get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) if1(true(),n,x,xs) -> filterlow(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) if2(true(),n,x,xs) -> filterhigh(n,xs) length(cons(x,xs)) -> s(length(xs)) length(nil()) -> 0() qs(n,cons(x,xs)) -> append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,cons(get(n,cons(x,xs)),qs(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))))) qs(n,nil()) -> nil() - Signature: {append/2,filterhigh/2,filterlow/2,ge/2,get/2,half/1,if1/4,if2/4,length/1,qs/2,qsort/1,append#/2 ,filterhigh#/2,filterlow#/2,ge#/2,get#/2,half#/1,if1#/4,if2#/4,length#/1,qs#/2,qsort#/1} / {0/0,cons/2 ,false/0,nil/0,s/1,true/0,ys/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/1,c_22/0,c_23/9,c_24/0,c_25/3} - Obligation: innermost runtime complexity wrt. defined symbols {append#,filterhigh#,filterlow#,ge#,get#,half#,if1#,if2# ,length#,qs#,qsort#} and constructors {0,cons,false,nil,s,true,ys} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) filterhigh(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) filterlow(n,nil()) -> nil() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) get(n,cons(x,nil())) -> x get(0(),cons(x,cons(y,xs))) -> x get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) if1(true(),n,x,xs) -> filterlow(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) if2(true(),n,x,xs) -> filterhigh(n,xs) length(cons(x,xs)) -> s(length(xs)) length(nil()) -> 0() append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())) filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) ge#(s(x),s(y)) -> c_9(ge#(x,y)) get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))) half#(s(s(x))) -> c_16(half#(x)) if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)) if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)) if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)) if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)) length#(cons(x,xs)) -> c_21(length#(xs)) qs#(n,cons(x,xs)) -> c_23(qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) qsort#(xs) -> c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) * Step 7: NaturalMI MAYBE + Considered Problem: - Strict DPs: append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())) filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) ge#(s(x),s(y)) -> c_9(ge#(x,y)) get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))) half#(s(s(x))) -> c_16(half#(x)) if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)) if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)) if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)) if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)) length#(cons(x,xs)) -> c_21(length#(xs)) qs#(n,cons(x,xs)) -> c_23(qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) qsort#(xs) -> c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) - Weak TRS: filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) filterhigh(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) filterlow(n,nil()) -> nil() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) get(n,cons(x,nil())) -> x get(0(),cons(x,cons(y,xs))) -> x get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) if1(true(),n,x,xs) -> filterlow(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) if2(true(),n,x,xs) -> filterhigh(n,xs) length(cons(x,xs)) -> s(length(xs)) length(nil()) -> 0() - Signature: {append/2,filterhigh/2,filterlow/2,ge/2,get/2,half/1,if1/4,if2/4,length/1,qs/2,qsort/1,append#/2 ,filterhigh#/2,filterlow#/2,ge#/2,get#/2,half#/1,if1#/4,if2#/4,length#/1,qs#/2,qsort#/1} / {0/0,cons/2 ,false/0,nil/0,s/1,true/0,ys/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/1,c_22/0,c_23/9,c_24/0,c_25/3} - Obligation: innermost runtime complexity wrt. defined symbols {append#,filterhigh#,filterlow#,ge#,get#,half#,if1#,if2# ,length#,qs#,qsort#} and constructors {0,cons,false,nil,s,true,ys} + 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}, uargs(c_3) = {1,2}, uargs(c_5) = {1,2}, uargs(c_9) = {1}, uargs(c_13) = {1}, uargs(c_16) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_19) = {1}, uargs(c_20) = {1}, uargs(c_21) = {1}, uargs(c_23) = {1,2,3,4,5,6,7,8,9}, uargs(c_25) = {1,2,3} Following symbols are considered usable: {append#,filterhigh#,filterlow#,ge#,get#,half#,if1#,if2#,length#,qs#,qsort#} TcT has computed the following interpretation: p(0) = [0] p(append) = [4] x1 + [0] p(cons) = [0] p(false) = [2] p(filterhigh) = [1] x1 + [0] p(filterlow) = [0] p(ge) = [0] p(get) = [1] x2 + [0] p(half) = [4] p(if1) = [2] x2 + [0] p(if2) = [4] x1 + [1] x2 + [2] x3 + [0] p(length) = [5] x1 + [1] p(nil) = [1] p(qs) = [1] p(qsort) = [1] x1 + [0] p(s) = [4] p(true) = [0] p(ys) = [1] p(append#) = [4] x2 + [4] p(filterhigh#) = [0] p(filterlow#) = [0] p(ge#) = [0] p(get#) = [0] p(half#) = [0] p(if1#) = [0] p(if2#) = [0] p(length#) = [0] p(qs#) = [0] p(qsort#) = [5] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [1] x1 + [2] x2 + [0] p(c_4) = [0] p(c_5) = [1] x1 + [1] x2 + [0] p(c_6) = [4] p(c_7) = [0] p(c_8) = [0] p(c_9) = [4] x1 + [0] p(c_10) = [2] p(c_11) = [1] p(c_12) = [1] p(c_13) = [1] x1 + [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [4] x1 + [0] p(c_17) = [2] x1 + [0] p(c_18) = [4] x1 + [0] p(c_19) = [1] x1 + [0] p(c_20) = [4] x1 + [0] p(c_21) = [4] x1 + [0] p(c_22) = [4] p(c_23) = [4] x1 + [4] x2 + [4] x3 + [4] x4 + [4] x5 + [4] x6 + [2] x7 + [4] x8 + [4] x9 + [0] p(c_24) = [0] p(c_25) = [1] x1 + [1] x2 + [4] x3 + [1] Following rules are strictly oriented: qsort#(xs) = [5] > [1] = c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) Following rules are (at-least) weakly oriented: append#(cons(x,xs),ys()) = [8] >= [8] = c_1(append#(xs,ys())) filterhigh#(n,cons(x,xs)) = [0] >= [0] = c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) filterlow#(n,cons(x,xs)) = [0] >= [0] = c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) ge#(s(x),s(y)) = [0] >= [0] = c_9(ge#(x,y)) get#(s(n),cons(x,cons(y,xs))) = [0] >= [0] = c_13(get#(n,cons(y,xs))) half#(s(s(x))) = [0] >= [0] = c_16(half#(x)) if1#(false(),n,x,xs) = [0] >= [0] = c_17(filterlow#(n,xs)) if1#(true(),n,x,xs) = [0] >= [0] = c_18(filterlow#(n,xs)) if2#(false(),n,x,xs) = [0] >= [0] = c_19(filterhigh#(n,xs)) if2#(true(),n,x,xs) = [0] >= [0] = c_20(filterhigh#(n,xs)) length#(cons(x,xs)) = [0] >= [0] = c_21(length#(xs)) qs#(n,cons(x,xs)) = [0] >= [0] = c_23(qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) * Step 8: Failure MAYBE + Considered Problem: - Strict DPs: append#(cons(x,xs),ys()) -> c_1(append#(xs,ys())) filterhigh#(n,cons(x,xs)) -> c_3(if2#(ge(x,n),n,x,xs),ge#(x,n)) filterlow#(n,cons(x,xs)) -> c_5(if1#(ge(n,x),n,x,xs),ge#(n,x)) ge#(s(x),s(y)) -> c_9(ge#(x,y)) get#(s(n),cons(x,cons(y,xs))) -> c_13(get#(n,cons(y,xs))) half#(s(s(x))) -> c_16(half#(x)) if1#(false(),n,x,xs) -> c_17(filterlow#(n,xs)) if1#(true(),n,x,xs) -> c_18(filterlow#(n,xs)) if2#(false(),n,x,xs) -> c_19(filterhigh#(n,xs)) if2#(true(),n,x,xs) -> c_20(filterhigh#(n,xs)) length#(cons(x,xs)) -> c_21(length#(xs)) qs#(n,cons(x,xs)) -> c_23(qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterlow#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs)) ,get#(n,cons(x,xs)) ,qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ,half#(n) ,filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ,get#(n,cons(x,xs))) - Weak DPs: qsort#(xs) -> c_25(qs#(half(length(xs)),xs),half#(length(xs)),length#(xs)) - Weak TRS: filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) filterhigh(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) filterlow(n,nil()) -> nil() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) get(n,cons(x,nil())) -> x get(0(),cons(x,cons(y,xs))) -> x get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) if1(true(),n,x,xs) -> filterlow(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) if2(true(),n,x,xs) -> filterhigh(n,xs) length(cons(x,xs)) -> s(length(xs)) length(nil()) -> 0() - Signature: {append/2,filterhigh/2,filterlow/2,ge/2,get/2,half/1,if1/4,if2/4,length/1,qs/2,qsort/1,append#/2 ,filterhigh#/2,filterlow#/2,ge#/2,get#/2,half#/1,if1#/4,if2#/4,length#/1,qs#/2,qsort#/1} / {0/0,cons/2 ,false/0,nil/0,s/1,true/0,ys/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/1,c_21/1,c_22/0,c_23/9,c_24/0,c_25/3} - Obligation: innermost runtime complexity wrt. defined symbols {append#,filterhigh#,filterlow#,ge#,get#,half#,if1#,if2# ,length#,qs#,qsort#} and constructors {0,cons,false,nil,s,true,ys} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE