YES
TRS:
 {                         eq(0(), 0()) -> true(),
                          eq(0(), s(m)) -> false(),
                          eq(s(n), 0()) -> false(),
                         eq(s(n), s(m)) -> eq(n, m),
                             le(0(), m) -> true(),
                          le(s(n), 0()) -> false(),
                         le(s(n), s(m)) -> le(n, m),
               min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))),
                  min(cons(0(), nil())) -> 0(),
                 min(cons(s(n), nil())) -> s(n),
    if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x)),
   if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x)),
              replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                   replace(n, m, nil()) -> nil(),
   if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
  if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                       sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))),
                            sort(nil()) -> nil()}
 DP:
  Strict:
   {                       eq#(s(n), s(m)) -> eq#(n, m),
                           le#(s(n), s(m)) -> le#(n, m),
                 min#(cons(n, cons(m, x))) -> le#(n, m),
                 min#(cons(n, cons(m, x))) -> if_min#(le(n, m), cons(n, cons(m, x))),
      if_min#(true(), cons(n, cons(m, x))) -> min#(cons(n, x)),
     if_min#(false(), cons(n, cons(m, x))) -> min#(cons(m, x)),
                replace#(n, m, cons(k, x)) -> eq#(n, k),
                replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)),
    if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x),
                         sort#(cons(n, x)) -> min#(cons(n, x)),
                         sort#(cons(n, x)) -> replace#(min(cons(n, x)), n, x),
                         sort#(cons(n, x)) -> sort#(replace(min(cons(n, x)), n, x))}
  Weak:
  {                         eq(0(), 0()) -> true(),
                           eq(0(), s(m)) -> false(),
                           eq(s(n), 0()) -> false(),
                          eq(s(n), s(m)) -> eq(n, m),
                              le(0(), m) -> true(),
                           le(s(n), 0()) -> false(),
                          le(s(n), s(m)) -> le(n, m),
                min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))),
                   min(cons(0(), nil())) -> 0(),
                  min(cons(s(n), nil())) -> s(n),
     if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x)),
    if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x)),
               replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                    replace(n, m, nil()) -> nil(),
    if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
   if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                        sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))),
                             sort(nil()) -> nil()}
  EDG:
   {(sort#(cons(n, x)) -> replace#(min(cons(n, x)), n, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)))
    (sort#(cons(n, x)) -> replace#(min(cons(n, x)), n, x), replace#(n, m, cons(k, x)) -> eq#(n, k))
    (if_min#(true(), cons(n, cons(m, x))) -> min#(cons(n, x)), min#(cons(n, cons(m, x))) -> if_min#(le(n, m), cons(n, cons(m, x))))
    (if_min#(true(), cons(n, cons(m, x))) -> min#(cons(n, x)), min#(cons(n, cons(m, x))) -> le#(n, m))
    (sort#(cons(n, x)) -> min#(cons(n, x)), min#(cons(n, cons(m, x))) -> if_min#(le(n, m), cons(n, cons(m, x))))
    (sort#(cons(n, x)) -> min#(cons(n, x)), min#(cons(n, cons(m, x))) -> le#(n, m))
    (replace#(n, m, cons(k, x)) -> eq#(n, k), eq#(s(n), s(m)) -> eq#(n, m))
    (le#(s(n), s(m)) -> le#(n, m), le#(s(n), s(m)) -> le#(n, m))
    (min#(cons(n, cons(m, x))) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(false(), cons(n, cons(m, x))) -> min#(cons(m, x)))
    (min#(cons(n, cons(m, x))) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(true(), cons(n, cons(m, x))) -> min#(cons(n, x)))
    (min#(cons(n, cons(m, x))) -> le#(n, m), le#(s(n), s(m)) -> le#(n, m))
    (eq#(s(n), s(m)) -> eq#(n, m), eq#(s(n), s(m)) -> eq#(n, m))
    (sort#(cons(n, x)) -> sort#(replace(min(cons(n, x)), n, x)), sort#(cons(n, x)) -> min#(cons(n, x)))
    (sort#(cons(n, x)) -> sort#(replace(min(cons(n, x)), n, x)), sort#(cons(n, x)) -> replace#(min(cons(n, x)), n, x))
    (sort#(cons(n, x)) -> sort#(replace(min(cons(n, x)), n, x)), sort#(cons(n, x)) -> sort#(replace(min(cons(n, x)), n, x)))
    (if_min#(false(), cons(n, cons(m, x))) -> min#(cons(m, x)), min#(cons(n, cons(m, x))) -> le#(n, m))
    (if_min#(false(), cons(n, cons(m, x))) -> min#(cons(m, x)), min#(cons(n, cons(m, x))) -> if_min#(le(n, m), cons(n, cons(m, x))))
    (replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)), if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x))
    (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> eq#(n, k))
    (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)))}
   SCCS:
    Scc:
     {sort#(cons(n, x)) -> sort#(replace(min(cons(n, x)), n, x))}
    Scc:
     {            replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)),
      if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x)}
    Scc:
     {            min#(cons(n, cons(m, x))) -> if_min#(le(n, m), cons(n, cons(m, x))),
       if_min#(true(), cons(n, cons(m, x))) -> min#(cons(n, x)),
      if_min#(false(), cons(n, cons(m, x))) -> min#(cons(m, x))}
    Scc:
     {le#(s(n), s(m)) -> le#(n, m)}
    Scc:
     {eq#(s(n), s(m)) -> eq#(n, m)}
    SCC:
     Strict:
      {sort#(cons(n, x)) -> sort#(replace(min(cons(n, x)), n, x))}
     Weak:
     {                         eq(0(), 0()) -> true(),
                              eq(0(), s(m)) -> false(),
                              eq(s(n), 0()) -> false(),
                             eq(s(n), s(m)) -> eq(n, m),
                                 le(0(), m) -> true(),
                              le(s(n), 0()) -> false(),
                             le(s(n), s(m)) -> le(n, m),
                   min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))),
                      min(cons(0(), nil())) -> 0(),
                     min(cons(s(n), nil())) -> s(n),
        if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x)),
       if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x)),
                  replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                       replace(n, m, nil()) -> nil(),
       if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
      if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                           sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))),
                                sort(nil()) -> nil()}
     POLY:
      Argument Filtering:
       pi(sort#) = 0, pi(sort) = [], pi(if_replace) = 3, pi(replace) = 2, pi(if_min) = [], pi(nil) = [], pi(cons) = [1], pi(min) = [], pi(le) = [], pi(s) = [], pi(false) = [], pi(0) = [], pi(eq) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [cons](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {                         eq(0(), 0()) -> true(),
                                eq(0(), s(m)) -> false(),
                                eq(s(n), 0()) -> false(),
                               eq(s(n), s(m)) -> eq(n, m),
                                   le(0(), m) -> true(),
                                le(s(n), 0()) -> false(),
                               le(s(n), s(m)) -> le(n, m),
                     min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))),
                        min(cons(0(), nil())) -> 0(),
                       min(cons(s(n), nil())) -> s(n),
          if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x)),
         if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x)),
                    replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                         replace(n, m, nil()) -> nil(),
         if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
        if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                             sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))),
                                  sort(nil()) -> nil()}
      Qed
    SCC:
     Strict:
      {            replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)),
       if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x)}
     Weak:
     {                         eq(0(), 0()) -> true(),
                              eq(0(), s(m)) -> false(),
                              eq(s(n), 0()) -> false(),
                             eq(s(n), s(m)) -> eq(n, m),
                                 le(0(), m) -> true(),
                              le(s(n), 0()) -> false(),
                             le(s(n), s(m)) -> le(n, m),
                   min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))),
                      min(cons(0(), nil())) -> 0(),
                     min(cons(s(n), nil())) -> s(n),
        if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x)),
       if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x)),
                  replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                       replace(n, m, nil()) -> nil(),
       if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
      if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                           sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))),
                                sort(nil()) -> nil()}
     SPSC:
      Simple Projection:
       pi(if_replace#) = 3, pi(replace#) = 2
      Strict:
       {replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x))}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {            min#(cons(n, cons(m, x))) -> if_min#(le(n, m), cons(n, cons(m, x))),
        if_min#(true(), cons(n, cons(m, x))) -> min#(cons(n, x)),
       if_min#(false(), cons(n, cons(m, x))) -> min#(cons(m, x))}
     Weak:
     {                         eq(0(), 0()) -> true(),
                              eq(0(), s(m)) -> false(),
                              eq(s(n), 0()) -> false(),
                             eq(s(n), s(m)) -> eq(n, m),
                                 le(0(), m) -> true(),
                              le(s(n), 0()) -> false(),
                             le(s(n), s(m)) -> le(n, m),
                   min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))),
                      min(cons(0(), nil())) -> 0(),
                     min(cons(s(n), nil())) -> s(n),
        if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x)),
       if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x)),
                  replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                       replace(n, m, nil()) -> nil(),
       if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
      if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                           sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))),
                                sort(nil()) -> nil()}
     POLY:
      Argument Filtering:
       pi(sort) = [], pi(if_replace) = [], pi(replace) = [], pi(if_min#) = 1, pi(if_min) = [], pi(nil) = [], pi(cons) = [1], pi(min#) = 0, pi(min) = [], pi(le) = [], pi(s) = [], pi(false) = [], pi(0) = [], pi(eq) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [cons](x0) = x0 + 1
      Strict:
       {min#(cons(n, cons(m, x))) -> if_min#(le(n, m), cons(n, cons(m, x)))}
      Weak:
       {                         eq(0(), 0()) -> true(),
                                eq(0(), s(m)) -> false(),
                                eq(s(n), 0()) -> false(),
                               eq(s(n), s(m)) -> eq(n, m),
                                   le(0(), m) -> true(),
                                le(s(n), 0()) -> false(),
                               le(s(n), s(m)) -> le(n, m),
                     min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))),
                        min(cons(0(), nil())) -> 0(),
                       min(cons(s(n), nil())) -> s(n),
          if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x)),
         if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x)),
                    replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                         replace(n, m, nil()) -> nil(),
         if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
        if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                             sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))),
                                  sort(nil()) -> nil()}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {le#(s(n), s(m)) -> le#(n, m)}
     Weak:
     {                         eq(0(), 0()) -> true(),
                              eq(0(), s(m)) -> false(),
                              eq(s(n), 0()) -> false(),
                             eq(s(n), s(m)) -> eq(n, m),
                                 le(0(), m) -> true(),
                              le(s(n), 0()) -> false(),
                             le(s(n), s(m)) -> le(n, m),
                   min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))),
                      min(cons(0(), nil())) -> 0(),
                     min(cons(s(n), nil())) -> s(n),
        if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x)),
       if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x)),
                  replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                       replace(n, m, nil()) -> nil(),
       if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
      if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                           sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))),
                                sort(nil()) -> nil()}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {eq#(s(n), s(m)) -> eq#(n, m)}
     Weak:
     {                         eq(0(), 0()) -> true(),
                              eq(0(), s(m)) -> false(),
                              eq(s(n), 0()) -> false(),
                             eq(s(n), s(m)) -> eq(n, m),
                                 le(0(), m) -> true(),
                              le(s(n), 0()) -> false(),
                             le(s(n), s(m)) -> le(n, m),
                   min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))),
                      min(cons(0(), nil())) -> 0(),
                     min(cons(s(n), nil())) -> s(n),
        if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x)),
       if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x)),
                  replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                       replace(n, m, nil()) -> nil(),
       if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
      if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                           sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))),
                                sort(nil()) -> nil()}
     SPSC:
      Simple Projection:
       pi(eq#) = 1
      Strict:
       {}
      Qed