YES Problem: qsort(nil()) -> nil() qsort(.(x,y)) -> ++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y)))) lowers(x,nil()) -> nil() lowers(x,.(y,z)) -> if(<=(y,x),.(y,lowers(x,z)),lowers(x,z)) greaters(x,nil()) -> nil() greaters(x,.(y,z)) -> if(<=(y,x),greaters(x,z),.(y,greaters(x,z))) Proof: DP Processor: DPs: qsort#(.(x,y)) -> greaters#(x,y) qsort#(.(x,y)) -> qsort#(greaters(x,y)) qsort#(.(x,y)) -> lowers#(x,y) qsort#(.(x,y)) -> qsort#(lowers(x,y)) lowers#(x,.(y,z)) -> lowers#(x,z) greaters#(x,.(y,z)) -> greaters#(x,z) TRS: qsort(nil()) -> nil() qsort(.(x,y)) -> ++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y)))) lowers(x,nil()) -> nil() lowers(x,.(y,z)) -> if(<=(y,x),.(y,lowers(x,z)),lowers(x,z)) greaters(x,nil()) -> nil() greaters(x,.(y,z)) -> if(<=(y,x),greaters(x,z),.(y,greaters(x,z))) KBO Processor: argument filtering: pi(nil) = [] pi(qsort) = [0] pi(.) = [1] pi(lowers) = 1 pi(greaters) = 1 pi(++) = [] pi(<=) = [] pi(if) = 2 pi(qsort#) = 0 pi(greaters#) = 1 pi(lowers#) = 1 weight function: w0 = 1 w(greaters#) = w(qsort#) = w(if) = w(<=) = w(++) = w(lowers) = w( qsort) = w(nil) = 1 w(lowers#) = w(greaters) = w(.) = 0 precedence: if > lowers# ~ greaters# ~ qsort# ~ <= ~ ++ ~ greaters ~ lowers ~ . ~ qsort ~ nil problem: DPs: TRS: qsort(nil()) -> nil() qsort(.(x,y)) -> ++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y)))) lowers(x,nil()) -> nil() lowers(x,.(y,z)) -> if(<=(y,x),.(y,lowers(x,z)),lowers(x,z)) greaters(x,nil()) -> nil() greaters(x,.(y,z)) -> if(<=(y,x),greaters(x,z),.(y,greaters(x,z))) Qed