YES
Time: 0.011937
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)))}
 DP:
  DP:
   {  msort# .(x, y) -> msort# del(min(x, y), .(x, y)),
      msort# .(x, y) -> min#(x, y),
      msort# .(x, y) -> del#(min(x, y), .(x, y)),
    min#(x, .(y, z)) -> min#(x, z),
    min#(x, .(y, z)) -> min#(y, 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:
   {(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) -> 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) -> min#(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), min#(x, .(y, z)) -> min#(x, z))
    (msort# .(x, y) -> min#(x, y), 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#(y, z), min#(x, .(y, z)) -> min#(y, z))
    (msort# .(x, y) -> del#(min(x, y), .(x, y)), del#(x, .(y, z)) -> del#(x, z))}
   SCCS (3):
    Scc:
     {del#(x, .(y, z)) -> del#(x, z)}
    Scc:
     {min#(x, .(y, z)) -> min#(x, z),
      min#(x, .(y, z)) -> min#(y, z)}
    Scc:
     {msort# .(x, y) -> msort# del(min(x, y), .(x, y))}
    SCC (1):
     Strict:
      {del#(x, .(y, z)) -> del#(x, z)}
     Weak:
     {    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)))}
     SPSC:
      Simple Projection:
       pi(del#) = 1
      Strict:
       {}
      Qed
    SCC (2):
     Strict:
      {min#(x, .(y, z)) -> min#(x, z),
       min#(x, .(y, z)) -> min#(y, z)}
     Weak:
     {    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)))}
     SPSC:
      Simple Projection:
       pi(min#) = 1
      Strict:
       {min#(x, .(y, z)) -> min#(y, z)}
      EDG:
       {(min#(x, .(y, z)) -> min#(y, z), min#(x, .(y, z)) -> min#(y, z))}
       SCCS (1):
        Scc:
         {min#(x, .(y, z)) -> min#(y, z)}
        SCC (1):
         Strict:
          {min#(x, .(y, z)) -> min#(y, z)}
         Weak:
         {    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)))}
         SPSC:
          Simple Projection:
           pi(min#) = 1
          Strict:
           {}
          Qed
    SCC (1):
     Strict:
      {msort# .(x, y) -> msort# del(min(x, y), .(x, y))}
     Weak:
     {    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)))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if](x0, x1, x2) = 0,
       
       [.](x0, x1) = 1,
       
       [min](x0, x1) = x0,
       
       [del](x0, x1) = 0,
       
       [<=](x0, x1) = 0,
       
       [=](x0, x1) = 0,
       
       [msort](x0) = x0 + 1,
       
       [nil] = 0,
       
       [msort#](x0) = x0
      Strict:
       msort# .(x, y) -> msort# del(min(x, y), .(x, y))
       1 + 0x + 0y >= 0 + 0x + 0y
      Weak:
       
     Qed