MAYBE

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)))
  Usable Rule 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:
    f11(x,y) -> x
    f11(x,y) -> y
    min(x,nil()) -> x
    min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z))
    del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z)))
    del(x,nil()) -> nil()
   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:
     f11(x,y) -> x
     f11(x,y) -> y
     min(x,nil()) -> x
     min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z))
     del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z)))
     del(x,nil()) -> nil()
    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)
    Restore Modifier:
     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)))
     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)))
      Open
      
      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)))
      Open
      
      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)))
      Open