YES Problem: msort(nil()) -> nil() msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y)))) min(x,nil()) -> x min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z)) del(x,nil()) -> nil() del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z))) Proof: DP Processor: DPs: msort#(.(x,y)) -> del#(min(x,y),.(x,y)) msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y))) msort#(.(x,y)) -> min#(x,y) min#(x,.(y,z)) -> min#(y,z) min#(x,.(y,z)) -> min#(x,z) del#(x,.(y,z)) -> del#(x,z) TRS: msort(nil()) -> nil() msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y)))) min(x,nil()) -> x min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z)) del(x,nil()) -> nil() del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z))) EDG Processor: DPs: msort#(.(x,y)) -> del#(min(x,y),.(x,y)) msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y))) msort#(.(x,y)) -> min#(x,y) min#(x,.(y,z)) -> min#(y,z) min#(x,.(y,z)) -> min#(x,z) del#(x,.(y,z)) -> del#(x,z) TRS: msort(nil()) -> nil() msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y)))) min(x,nil()) -> x min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z)) del(x,nil()) -> nil() del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z))) graph: min#(x,.(y,z)) -> min#(y,z) -> min#(x,.(y,z)) -> min#(y,z) min#(x,.(y,z)) -> min#(y,z) -> min#(x,.(y,z)) -> min#(x,z) min#(x,.(y,z)) -> min#(x,z) -> min#(x,.(y,z)) -> min#(y,z) min#(x,.(y,z)) -> min#(x,z) -> min#(x,.(y,z)) -> min#(x,z) del#(x,.(y,z)) -> del#(x,z) -> del#(x,.(y,z)) -> del#(x,z) msort#(.(x,y)) -> min#(x,y) -> min#(x,.(y,z)) -> min#(y,z) msort#(.(x,y)) -> min#(x,y) -> min#(x,.(y,z)) -> min#(x,z) msort#(.(x,y)) -> del#(min(x,y),.(x,y)) -> del#(x,.(y,z)) -> del#(x,z) msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y))) -> msort#(.(x,y)) -> del#(min(x,y),.(x,y)) msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y))) -> msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y))) msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y))) -> msort#(.(x,y)) -> min#(x,y) SCC Processor: #sccs: 3 #rules: 4 #arcs: 11/36 DPs: msort#(.(x,y)) -> msort#(del(min(x,y),.(x,y))) TRS: msort(nil()) -> nil() msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y)))) min(x,nil()) -> x min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z)) del(x,nil()) -> nil() del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z))) Matrix Interpretation Processor: dimension: 1 interpretation: [msort#](x0) = x0, [=](x0, x1) = 0, [if](x0, x1, x2) = x0, [<=](x0, x1) = x0, [del](x0, x1) = 0, [min](x0, x1) = x0, [.](x0, x1) = 1, [msort](x0) = x0, [nil] = 0 orientation: msort#(.(x,y)) = 1 >= 0 = msort#(del(min(x,y),.(x,y))) msort(nil()) = 0 >= 0 = nil() msort(.(x,y)) = 1 >= 1 = .(min(x,y),msort(del(min(x,y),.(x,y)))) min(x,nil()) = x >= x = x min(x,.(y,z)) = x >= x = if(<=(x,y),min(x,z),min(y,z)) del(x,nil()) = 0 >= 0 = nil() del(x,.(y,z)) = 0 >= 0 = if(=(x,y),z,.(y,del(x,z))) problem: DPs: TRS: msort(nil()) -> nil() msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y)))) min(x,nil()) -> x min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z)) del(x,nil()) -> nil() del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z))) Qed DPs: del#(x,.(y,z)) -> del#(x,z) TRS: msort(nil()) -> nil() msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y)))) min(x,nil()) -> x min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z)) del(x,nil()) -> nil() del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z))) Subterm Criterion Processor: simple projection: pi(del#) = 1 problem: DPs: TRS: msort(nil()) -> nil() msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y)))) min(x,nil()) -> x min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z)) del(x,nil()) -> nil() del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z))) Qed DPs: min#(x,.(y,z)) -> min#(y,z) min#(x,.(y,z)) -> min#(x,z) TRS: msort(nil()) -> nil() msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y)))) min(x,nil()) -> x min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z)) del(x,nil()) -> nil() del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z))) Subterm Criterion Processor: simple projection: pi(min#) = 1 problem: DPs: TRS: msort(nil()) -> nil() msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y)))) min(x,nil()) -> x min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z)) del(x,nil()) -> nil() del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z))) Qed