MAYBE Problem: qsort(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort(filterhigh (last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(cons(y,xs)) Proof: DP Processor: DPs: qsort#(cons(x,xs)) -> filterhigh#(last(cons(x,xs)),cons(x,xs)) qsort#(cons(x,xs)) -> qsort#(filterhigh(last(cons(x,xs)),cons(x,xs))) qsort#(cons(x,xs)) -> last#(cons(x,xs)) qsort#(cons(x,xs)) -> filterlow#(last(cons(x,xs)),cons(x,xs)) qsort#(cons(x,xs)) -> qsort#(filterlow(last(cons(x,xs)),cons(x,xs))) qsort#(cons(x,xs)) -> append#(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort(filterhigh ( last(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()) last#(cons(x,cons(y,xs))) -> last#(cons(y,xs)) TRS: qsort(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort(filterhigh (last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(cons(y,xs)) TDG Processor: DPs: qsort#(cons(x,xs)) -> filterhigh#(last(cons(x,xs)),cons(x,xs)) qsort#(cons(x,xs)) -> qsort#(filterhigh(last(cons(x,xs)),cons(x,xs))) qsort#(cons(x,xs)) -> last#(cons(x,xs)) qsort#(cons(x,xs)) -> filterlow#(last(cons(x,xs)),cons(x,xs)) qsort#(cons(x,xs)) -> qsort#(filterlow(last(cons(x,xs)),cons(x,xs))) qsort#(cons(x,xs)) -> append#(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort( filterhigh ( last(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()) last#(cons(x,cons(y,xs))) -> last#(cons(y,xs)) TRS: qsort(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort(filterhigh ( last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(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) last#(cons(x,cons(y,xs))) -> last#(cons(y,xs)) -> last#(cons(x,cons(y,xs))) -> last#(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) qsort#(cons(x,xs)) -> append#(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort( filterhigh ( last(cons(x,xs)),cons(x,xs))))) -> append#(cons(x,xs),ys()) -> append#(xs,ys()) qsort#(cons(x,xs)) -> filterlow#(last(cons(x,xs)),cons(x,xs)) -> filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) qsort#(cons(x,xs)) -> filterlow#(last(cons(x,xs)),cons(x,xs)) -> filterlow#(n,cons(x,xs)) -> ge#(n,x) qsort#(cons(x,xs)) -> last#(cons(x,xs)) -> last#(cons(x,cons(y,xs))) -> last#(cons(y,xs)) qsort#(cons(x,xs)) -> filterhigh#(last(cons(x,xs)),cons(x,xs)) -> filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) qsort#(cons(x,xs)) -> filterhigh#(last(cons(x,xs)),cons(x,xs)) -> filterhigh#(n,cons(x,xs)) -> ge#(x,n) qsort#(cons(x,xs)) -> qsort#(filterhigh(last(cons(x,xs)),cons(x,xs))) -> qsort#(cons(x,xs)) -> append#(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort( filterhigh ( last(cons(x,xs)),cons(x,xs))))) qsort#(cons(x,xs)) -> qsort#(filterhigh(last(cons(x,xs)),cons(x,xs))) -> qsort#(cons(x,xs)) -> qsort#(filterlow(last(cons(x,xs)),cons(x,xs))) qsort#(cons(x,xs)) -> qsort#(filterhigh(last(cons(x,xs)),cons(x,xs))) -> qsort#(cons(x,xs)) -> filterlow#(last(cons(x,xs)),cons(x,xs)) qsort#(cons(x,xs)) -> qsort#(filterhigh(last(cons(x,xs)),cons(x,xs))) -> qsort#(cons(x,xs)) -> last#(cons(x,xs)) qsort#(cons(x,xs)) -> qsort#(filterhigh(last(cons(x,xs)),cons(x,xs))) -> qsort#(cons(x,xs)) -> qsort#(filterhigh(last(cons(x,xs)),cons(x,xs))) qsort#(cons(x,xs)) -> qsort#(filterhigh(last(cons(x,xs)),cons(x,xs))) -> qsort#(cons(x,xs)) -> filterhigh#(last(cons(x,xs)),cons(x,xs)) qsort#(cons(x,xs)) -> qsort#(filterlow(last(cons(x,xs)),cons(x,xs))) -> qsort#(cons(x,xs)) -> append#(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort( filterhigh ( last(cons(x,xs)),cons(x,xs))))) qsort#(cons(x,xs)) -> qsort#(filterlow(last(cons(x,xs)),cons(x,xs))) -> qsort#(cons(x,xs)) -> qsort#(filterlow(last(cons(x,xs)),cons(x,xs))) qsort#(cons(x,xs)) -> qsort#(filterlow(last(cons(x,xs)),cons(x,xs))) -> qsort#(cons(x,xs)) -> filterlow#(last(cons(x,xs)),cons(x,xs)) qsort#(cons(x,xs)) -> qsort#(filterlow(last(cons(x,xs)),cons(x,xs))) -> qsort#(cons(x,xs)) -> last#(cons(x,xs)) qsort#(cons(x,xs)) -> qsort#(filterlow(last(cons(x,xs)),cons(x,xs))) -> qsort#(cons(x,xs)) -> qsort#(filterhigh(last(cons(x,xs)),cons(x,xs))) qsort#(cons(x,xs)) -> qsort#(filterlow(last(cons(x,xs)),cons(x,xs))) -> qsort#(cons(x,xs)) -> filterhigh#(last(cons(x,xs)),cons(x,xs)) SCC Processor: #sccs: 6 #rules: 11 #arcs: 35/289 DPs: qsort#(cons(x,xs)) -> qsort#(filterhigh(last(cons(x,xs)),cons(x,xs))) qsort#(cons(x,xs)) -> qsort#(filterlow(last(cons(x,xs)),cons(x,xs))) TRS: qsort(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort( filterhigh ( last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(cons(y,xs)) Open DPs: last#(cons(x,cons(y,xs))) -> last#(cons(y,xs)) TRS: qsort(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort( filterhigh ( last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(cons(y,xs)) Subterm Criterion Processor: simple projection: pi(last#) = 0 problem: DPs: TRS: qsort(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort (filterhigh (last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(cons(y,xs)) Qed DPs: append#(cons(x,xs),ys()) -> append#(xs,ys()) TRS: qsort(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort( filterhigh ( last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(cons(y,xs)) Subterm Criterion Processor: simple projection: pi(append#) = 0 problem: DPs: TRS: qsort(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort (filterhigh (last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(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(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort( filterhigh ( last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(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(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort (filterhigh (last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(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(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort( filterhigh ( last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(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(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort (filterhigh (last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(cons(y,xs)) SCC Processor: #sccs: 0 #rules: 0 #arcs: 4/4 DPs: ge#(s(x),s(y)) -> ge#(x,y) TRS: qsort(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort( filterhigh ( last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(cons(y,xs)) Subterm Criterion Processor: simple projection: pi(ge#) = 1 problem: DPs: TRS: qsort(nil()) -> nil() qsort(cons(x,xs)) -> append(qsort(filterlow(last(cons(x,xs)),cons(x,xs))),cons(last(cons(x,xs)), qsort (filterhigh (last(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())) last(nil()) -> 0() last(cons(x,nil())) -> x last(cons(x,cons(y,xs))) -> last(cons(y,xs)) Qed