YES
TRS:
 {                      sort(nil()) -> nil(),
                   sort(cons(x, y)) -> insert(x, sort(y)),
                   insert(x, nil()) -> cons(x, nil()),
              insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v),
      choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)),
   choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)),
  choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
 DP:
  Strict:
   {                 sort#(cons(x, y)) -> sort#(y),
                     sort#(cons(x, y)) -> insert#(x, sort(y)),
                insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v),
     choose#(x, cons(v, w), 0(), s(z)) -> insert#(x, w),
    choose#(x, cons(v, w), s(y), s(z)) -> choose#(x, cons(v, w), y, z)}
  Weak:
  {                      sort(nil()) -> nil(),
                    sort(cons(x, y)) -> insert(x, sort(y)),
                    insert(x, nil()) -> cons(x, nil()),
               insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v),
       choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)),
    choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)),
   choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
  EDG:
   {(sort#(cons(x, y)) -> sort#(y), sort#(cons(x, y)) -> insert#(x, sort(y)))
    (sort#(cons(x, y)) -> sort#(y), sort#(cons(x, y)) -> sort#(y))
    (choose#(x, cons(v, w), s(y), s(z)) -> choose#(x, cons(v, w), y, z), choose#(x, cons(v, w), s(y), s(z)) -> choose#(x, cons(v, w), y, z))
    (choose#(x, cons(v, w), s(y), s(z)) -> choose#(x, cons(v, w), y, z), choose#(x, cons(v, w), 0(), s(z)) -> insert#(x, w))
    (choose#(x, cons(v, w), 0(), s(z)) -> insert#(x, w), insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v))
    (sort#(cons(x, y)) -> insert#(x, sort(y)), insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v))
    (insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v), choose#(x, cons(v, w), 0(), s(z)) -> insert#(x, w))
    (insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v), choose#(x, cons(v, w), s(y), s(z)) -> choose#(x, cons(v, w), y, z))}
   SCCS:
    Scc:
     {            insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v),
       choose#(x, cons(v, w), 0(), s(z)) -> insert#(x, w),
      choose#(x, cons(v, w), s(y), s(z)) -> choose#(x, cons(v, w), y, z)}
    Scc:
     {sort#(cons(x, y)) -> sort#(y)}
    SCC:
     Strict:
      {            insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v),
        choose#(x, cons(v, w), 0(), s(z)) -> insert#(x, w),
       choose#(x, cons(v, w), s(y), s(z)) -> choose#(x, cons(v, w), y, z)}
     Weak:
     {                      sort(nil()) -> nil(),
                       sort(cons(x, y)) -> insert(x, sort(y)),
                       insert(x, nil()) -> cons(x, nil()),
                  insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v),
          choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)),
       choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)),
      choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
     SPSC:
      Simple Projection:
       pi(choose#) = 1, pi(insert#) = 1
      Strict:
       {            insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v),
        choose#(x, cons(v, w), s(y), s(z)) -> choose#(x, cons(v, w), y, z)}
      EDG:
       {(insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v), choose#(x, cons(v, w), s(y), s(z)) -> choose#(x, cons(v, w), y, z))
        (choose#(x, cons(v, w), s(y), s(z)) -> choose#(x, cons(v, w), y, z), choose#(x, cons(v, w), s(y), s(z)) -> choose#(x, cons(v, w), y, z))}
       SCCS:
        Scc:
         {choose#(x, cons(v, w), s(y), s(z)) -> choose#(x, cons(v, w), y, z)}
        SCC:
         Strict:
          {choose#(x, cons(v, w), s(y), s(z)) -> choose#(x, cons(v, w), y, z)}
         Weak:
         {                      sort(nil()) -> nil(),
                           sort(cons(x, y)) -> insert(x, sort(y)),
                           insert(x, nil()) -> cons(x, nil()),
                      insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v),
              choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)),
           choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)),
          choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
         SPSC:
          Simple Projection:
           pi(choose#) = 3
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {sort#(cons(x, y)) -> sort#(y)}
     Weak:
     {                      sort(nil()) -> nil(),
                       sort(cons(x, y)) -> insert(x, sort(y)),
                       insert(x, nil()) -> cons(x, nil()),
                  insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v),
          choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)),
       choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)),
      choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
     SPSC:
      Simple Projection:
       pi(sort#) = 0
      Strict:
       {}
      Qed