MAYBE Problem: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Proof: DP Processor: DPs: qsort#(xs) -> length#(xs) qsort#(xs) -> half#(length(xs)) qsort#(xs) -> qs#(half(length(xs)),xs) qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs)) qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) qs#(n,cons(x,xs)) -> get#(n,cons(x,xs)) qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs)) qs#(n,cons(x,xs)) -> half#(n) qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) 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))))) filterlow#(n,cons(x,xs)) -> ge#(n,x) filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) if1#(true(),n,x,xs) -> filterlow#(n,xs) if1#(false(),n,x,xs) -> filterlow#(n,xs) filterhigh#(n,cons(x,xs)) -> ge#(x,n) filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) if2#(true(),n,x,xs) -> filterhigh#(n,xs) if2#(false(),n,x,xs) -> filterhigh#(n,xs) ge#(s(x),s(y)) -> ge#(x,y) append#(cons(x,xs),ys()) -> append#(xs,ys()) length#(cons(x,xs)) -> length#(xs) half#(s(s(x))) -> half#(x) get#(s(n),cons(x,cons(y,xs))) -> get#(n,cons(y,xs)) TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) TDG Processor: DPs: qsort#(xs) -> length#(xs) qsort#(xs) -> half#(length(xs)) qsort#(xs) -> qs#(half(length(xs)),xs) qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs)) qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) qs#(n,cons(x,xs)) -> get#(n,cons(x,xs)) qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs)) qs#(n,cons(x,xs)) -> half#(n) qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) 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))))) filterlow#(n,cons(x,xs)) -> ge#(n,x) filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) if1#(true(),n,x,xs) -> filterlow#(n,xs) if1#(false(),n,x,xs) -> filterlow#(n,xs) filterhigh#(n,cons(x,xs)) -> ge#(x,n) filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) if2#(true(),n,x,xs) -> filterhigh#(n,xs) if2#(false(),n,x,xs) -> filterhigh#(n,xs) ge#(s(x),s(y)) -> ge#(x,y) append#(cons(x,xs),ys()) -> append#(xs,ys()) length#(cons(x,xs)) -> length#(xs) half#(s(s(x))) -> half#(x) get#(s(n),cons(x,cons(y,xs))) -> get#(n,cons(y,xs)) TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) graph: if2#(false(),n,x,xs) -> filterhigh#(n,xs) -> filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) if2#(false(),n,x,xs) -> filterhigh#(n,xs) -> filterhigh#(n,cons(x,xs)) -> ge#(x,n) if2#(true(),n,x,xs) -> filterhigh#(n,xs) -> filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) if2#(true(),n,x,xs) -> filterhigh#(n,xs) -> filterhigh#(n,cons(x,xs)) -> ge#(x,n) if1#(false(),n,x,xs) -> filterlow#(n,xs) -> filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) if1#(false(),n,x,xs) -> filterlow#(n,xs) -> filterlow#(n,cons(x,xs)) -> ge#(n,x) if1#(true(),n,x,xs) -> filterlow#(n,xs) -> filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) if1#(true(),n,x,xs) -> filterlow#(n,xs) -> filterlow#(n,cons(x,xs)) -> ge#(n,x) ge#(s(x),s(y)) -> ge#(x,y) -> ge#(s(x),s(y)) -> ge#(x,y) append#(cons(x,xs),ys()) -> append#(xs,ys()) -> append#(cons(x,xs),ys()) -> append#(xs,ys()) filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) -> if1#(false(),n,x,xs) -> filterlow#(n,xs) filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) -> if1#(true(),n,x,xs) -> filterlow#(n,xs) filterlow#(n,cons(x,xs)) -> ge#(n,x) -> ge#(s(x),s(y)) -> ge#(x,y) get#(s(n),cons(x,cons(y,xs))) -> get#(n,cons(y,xs)) -> get#(s(n),cons(x,cons(y,xs))) -> get#(n,cons(y,xs)) filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) -> if2#(false(),n,x,xs) -> filterhigh#(n,xs) filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) -> if2#(true(),n,x,xs) -> filterhigh#(n,xs) filterhigh#(n,cons(x,xs)) -> ge#(x,n) -> ge#(s(x),s(y)) -> ge#(x,y) 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))))) -> append#(cons(x,xs),ys()) -> append#(xs,ys()) qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs)) -> filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs)) -> filterlow#(n,cons(x,xs)) -> ge#(n,x) qs#(n,cons(x,xs)) -> get#(n,cons(x,xs)) -> get#(s(n),cons(x,cons(y,xs))) -> get#(n,cons(y,xs)) qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs)) -> filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs)) -> filterhigh#(n,cons(x,xs)) -> ge#(x,n) qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) -> 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,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) -> qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) -> qs#(n,cons(x,xs)) -> half#(n) qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) -> qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs)) qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) -> qs#(n,cons(x,xs)) -> get#(n,cons(x,xs)) qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) -> qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) -> qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs)) qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) -> 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,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) -> qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) -> qs#(n,cons(x,xs)) -> half#(n) qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) -> qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs)) qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) -> qs#(n,cons(x,xs)) -> get#(n,cons(x,xs)) qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) -> qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) -> qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs)) qs#(n,cons(x,xs)) -> half#(n) -> half#(s(s(x))) -> half#(x) half#(s(s(x))) -> half#(x) -> half#(s(s(x))) -> half#(x) length#(cons(x,xs)) -> length#(xs) -> length#(cons(x,xs)) -> length#(xs) qsort#(xs) -> qs#(half(length(xs)),xs) -> 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))))) qsort#(xs) -> qs#(half(length(xs)),xs) -> qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) qsort#(xs) -> qs#(half(length(xs)),xs) -> qs#(n,cons(x,xs)) -> half#(n) qsort#(xs) -> qs#(half(length(xs)),xs) -> qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs)) qsort#(xs) -> qs#(half(length(xs)),xs) -> qs#(n,cons(x,xs)) -> get#(n,cons(x,xs)) qsort#(xs) -> qs#(half(length(xs)),xs) -> qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) qsort#(xs) -> qs#(half(length(xs)),xs) -> qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs)) qsort#(xs) -> half#(length(xs)) -> half#(s(s(x))) -> half#(x) qsort#(xs) -> length#(xs) -> length#(cons(x,xs)) -> length#(xs) SCC Processor: #sccs: 8 #rules: 13 #arcs: 49/529 DPs: length#(cons(x,xs)) -> length#(xs) TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Subterm Criterion Processor: simple projection: pi(length#) = 0 problem: DPs: TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Qed DPs: qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Open DPs: half#(s(s(x))) -> half#(x) TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Subterm Criterion Processor: simple projection: pi(half#) = 0 problem: DPs: TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Qed DPs: get#(s(n),cons(x,cons(y,xs))) -> get#(n,cons(y,xs)) TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Subterm Criterion Processor: simple projection: pi(get#) = 1 problem: DPs: TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Qed DPs: append#(cons(x,xs),ys()) -> append#(xs,ys()) TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Subterm Criterion Processor: simple projection: pi(append#) = 0 problem: DPs: TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Qed DPs: if1#(false(),n,x,xs) -> filterlow#(n,xs) filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) if1#(true(),n,x,xs) -> filterlow#(n,xs) TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Subterm Criterion Processor: simple projection: pi(filterlow#) = 1 pi(if1#) = 3 problem: DPs: if1#(false(),n,x,xs) -> filterlow#(n,xs) if1#(true(),n,x,xs) -> filterlow#(n,xs) TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) SCC Processor: #sccs: 0 #rules: 0 #arcs: 4/4 DPs: if2#(false(),n,x,xs) -> filterhigh#(n,xs) filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) if2#(true(),n,x,xs) -> filterhigh#(n,xs) TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Subterm Criterion Processor: simple projection: pi(filterhigh#) = 1 pi(if2#) = 3 problem: DPs: if2#(false(),n,x,xs) -> filterhigh#(n,xs) if2#(true(),n,x,xs) -> filterhigh#(n,xs) TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) SCC Processor: #sccs: 0 #rules: 0 #arcs: 4/4 DPs: ge#(s(x),s(y)) -> ge#(x,y) TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Subterm Criterion Processor: simple projection: pi(ge#) = 1 problem: DPs: TRS: qsort(xs) -> qs(half(length(xs)),xs) qs(n,nil()) -> nil() 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))))) filterlow(n,nil()) -> nil() filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) if1(true(),n,x,xs) -> filterlow(n,xs) if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) filterhigh(n,nil()) -> nil() filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) if2(true(),n,x,xs) -> filterhigh(n,xs) if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) append(nil(),ys()) -> ys() append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) length(nil()) -> 0() length(cons(x,xs)) -> s(length(xs)) half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) get(n,nil()) -> 0() 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)) Qed