YES
TRS:
 {                      eq(0(), 0()) -> true(),
                       eq(0(), s(x)) -> false(),
                       eq(s(x), 0()) -> false(),
                      eq(s(x), s(y)) -> eq(x, y),
                          le(0(), y) -> true(),
                       le(s(x), 0()) -> false(),
                      le(s(x), s(y)) -> le(x, y),
                       app(nil(), y) -> y,
                   app(add(n, x), y) -> add(n, app(x, y)),
                  min(add(n, nil())) -> n,
              min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x))),
   if_min(true(), add(n, add(m, x))) -> min(add(n, x)),
  if_min(false(), add(n, add(m, x))) -> min(add(m, x)),
                        rm(n, nil()) -> nil(),
                    rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
         if_rm(true(), n, add(m, x)) -> rm(n, x),
        if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
               minsort(nil(), nil()) -> nil(),
               minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y),
    if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
   if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
 DP:
  Strict:
   {                    eq#(s(x), s(y)) -> eq#(x, y),
                        le#(s(x), s(y)) -> le#(x, y),
                     app#(add(n, x), y) -> app#(x, y),
                min#(add(n, add(m, x))) -> le#(n, m),
                min#(add(n, add(m, x))) -> if_min#(le(n, m), add(n, add(m, x))),
     if_min#(true(), add(n, add(m, x))) -> min#(add(n, x)),
    if_min#(false(), add(n, add(m, x))) -> min#(add(m, x)),
                      rm#(n, add(m, x)) -> eq#(n, m),
                      rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)),
           if_rm#(true(), n, add(m, x)) -> rm#(n, x),
          if_rm#(false(), n, add(m, x)) -> rm#(n, x),
                 minsort#(add(n, x), y) -> eq#(n, min(add(n, x))),
                 minsort#(add(n, x), y) -> min#(add(n, x)),
                 minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y),
      if_minsort#(true(), add(n, x), y) -> app#(rm(n, x), y),
      if_minsort#(true(), add(n, x), y) -> rm#(n, x),
      if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()),
     if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))}
  Weak:
  {                      eq(0(), 0()) -> true(),
                        eq(0(), s(x)) -> false(),
                        eq(s(x), 0()) -> false(),
                       eq(s(x), s(y)) -> eq(x, y),
                           le(0(), y) -> true(),
                        le(s(x), 0()) -> false(),
                       le(s(x), s(y)) -> le(x, y),
                        app(nil(), y) -> y,
                    app(add(n, x), y) -> add(n, app(x, y)),
                   min(add(n, nil())) -> n,
               min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x))),
    if_min(true(), add(n, add(m, x))) -> min(add(n, x)),
   if_min(false(), add(n, add(m, x))) -> min(add(m, x)),
                         rm(n, nil()) -> nil(),
                     rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
          if_rm(true(), n, add(m, x)) -> rm(n, x),
         if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                minsort(nil(), nil()) -> nil(),
                minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y),
     if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
    if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
  EDG:
   {(if_minsort#(true(), add(n, x), y) -> app#(rm(n, x), y), app#(add(n, x), y) -> app#(x, y))
    (if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y))
    (if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> min#(add(n, x)))
    (if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> eq#(n, min(add(n, x))))
    (if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y))
    (if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), minsort#(add(n, x), y) -> min#(add(n, x)))
    (if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), minsort#(add(n, x), y) -> eq#(n, min(add(n, x))))
    (rm#(n, add(m, x)) -> eq#(n, m), eq#(s(x), s(y)) -> eq#(x, y))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))
    (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
    (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m))
    (if_minsort#(true(), add(n, x), y) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
    (if_minsort#(true(), add(n, x), y) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m))
    (if_min#(true(), add(n, add(m, x))) -> min#(add(n, x)), min#(add(n, add(m, x))) -> if_min#(le(n, m), add(n, add(m, x))))
    (if_min#(true(), add(n, add(m, x))) -> min#(add(n, x)), min#(add(n, add(m, x))) -> le#(n, m))
    (minsort#(add(n, x), y) -> min#(add(n, x)), min#(add(n, add(m, x))) -> if_min#(le(n, m), add(n, add(m, x))))
    (minsort#(add(n, x), y) -> min#(add(n, x)), min#(add(n, add(m, x))) -> le#(n, m))
    (if_min#(false(), add(n, add(m, x))) -> min#(add(m, x)), min#(add(n, add(m, x))) -> le#(n, m))
    (if_min#(false(), add(n, add(m, x))) -> min#(add(m, x)), min#(add(n, add(m, x))) -> if_min#(le(n, m), add(n, add(m, x))))
    (min#(add(n, add(m, x))) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(true(), add(n, add(m, x))) -> min#(add(n, x)))
    (min#(add(n, add(m, x))) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(false(), add(n, add(m, x))) -> min#(add(m, x)))
    (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m))
    (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
    (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y))
    (eq#(s(x), s(y)) -> eq#(x, y), eq#(s(x), s(y)) -> eq#(x, y))
    (min#(add(n, add(m, x))) -> le#(n, m), le#(s(x), s(y)) -> le#(x, y))
    (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x))
    (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(false(), n, add(m, x)) -> rm#(n, x))
    (minsort#(add(n, x), y) -> eq#(n, min(add(n, x))), eq#(s(x), s(y)) -> eq#(x, y))
    (minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y), if_minsort#(true(), add(n, x), y) -> app#(rm(n, x), y))
    (minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y), if_minsort#(true(), add(n, x), y) -> rm#(n, x))
    (minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y), if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()))
    (minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)))}
   SCCS:
    Scc:
     {            minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y),
       if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()),
      if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))}
    Scc:
     {            rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)),
       if_rm#(true(), n, add(m, x)) -> rm#(n, x),
      if_rm#(false(), n, add(m, x)) -> rm#(n, x)}
    Scc:
     {            min#(add(n, add(m, x))) -> if_min#(le(n, m), add(n, add(m, x))),
       if_min#(true(), add(n, add(m, x))) -> min#(add(n, x)),
      if_min#(false(), add(n, add(m, x))) -> min#(add(m, x))}
    Scc:
     {app#(add(n, x), y) -> app#(x, y)}
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    Scc:
     {eq#(s(x), s(y)) -> eq#(x, y)}
    SCC:
     Strict:
      {            minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y),
        if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()),
       if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))}
     Weak:
     {                      eq(0(), 0()) -> true(),
                           eq(0(), s(x)) -> false(),
                           eq(s(x), 0()) -> false(),
                          eq(s(x), s(y)) -> eq(x, y),
                              le(0(), y) -> true(),
                           le(s(x), 0()) -> false(),
                          le(s(x), s(y)) -> le(x, y),
                           app(nil(), y) -> y,
                       app(add(n, x), y) -> add(n, app(x, y)),
                      min(add(n, nil())) -> n,
                  min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x))),
       if_min(true(), add(n, add(m, x))) -> min(add(n, x)),
      if_min(false(), add(n, add(m, x))) -> min(add(m, x)),
                            rm(n, nil()) -> nil(),
                        rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
             if_rm(true(), n, add(m, x)) -> rm(n, x),
            if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                   minsort(nil(), nil()) -> nil(),
                   minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y),
        if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
       if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
     POLY:
      Argument Filtering:
       pi(if_minsort#) = [1,2], pi(if_minsort) = [], pi(minsort#) = [0,1], pi(minsort) = [], pi(if_rm) = 2, pi(rm) = 1, pi(if_min) = [], pi(min) = [], pi(add) = [1], pi(nil) = [], pi(app) = [0,1], pi(le) = [], pi(s) = [], pi(false) = [], pi(0) = [], pi(eq) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [if_minsort#](x0, x1) = x0 + x1,
       [minsort#](x0, x1) = x0 + x1,
       [add](x0) = x0 + 1,
       [app](x0, x1) = x0 + x1,
       [nil] = 0
      Strict:
       {            minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y),
        if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))}
      Weak:
       {                      eq(0(), 0()) -> true(),
                             eq(0(), s(x)) -> false(),
                             eq(s(x), 0()) -> false(),
                            eq(s(x), s(y)) -> eq(x, y),
                                le(0(), y) -> true(),
                             le(s(x), 0()) -> false(),
                            le(s(x), s(y)) -> le(x, y),
                             app(nil(), y) -> y,
                         app(add(n, x), y) -> add(n, app(x, y)),
                        min(add(n, nil())) -> n,
                    min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x))),
         if_min(true(), add(n, add(m, x))) -> min(add(n, x)),
        if_min(false(), add(n, add(m, x))) -> min(add(m, x)),
                              rm(n, nil()) -> nil(),
                          rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
               if_rm(true(), n, add(m, x)) -> rm(n, x),
              if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                     minsort(nil(), nil()) -> nil(),
                     minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y),
          if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
         if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
      EDG:
       {(if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y))
        (minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)))}
       SCCS:
        Scc:
         {            minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y),
          if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))}
        SCC:
         Strict:
          {            minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y),
           if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))}
         Weak:
         {                      eq(0(), 0()) -> true(),
                               eq(0(), s(x)) -> false(),
                               eq(s(x), 0()) -> false(),
                              eq(s(x), s(y)) -> eq(x, y),
                                  le(0(), y) -> true(),
                               le(s(x), 0()) -> false(),
                              le(s(x), s(y)) -> le(x, y),
                               app(nil(), y) -> y,
                           app(add(n, x), y) -> add(n, app(x, y)),
                          min(add(n, nil())) -> n,
                      min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x))),
           if_min(true(), add(n, add(m, x))) -> min(add(n, x)),
          if_min(false(), add(n, add(m, x))) -> min(add(m, x)),
                                rm(n, nil()) -> nil(),
                            rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
                 if_rm(true(), n, add(m, x)) -> rm(n, x),
                if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                       minsort(nil(), nil()) -> nil(),
                       minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y),
            if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
           if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
         SPSC:
          Simple Projection:
           pi(if_minsort#) = 1, pi(minsort#) = 0
          Strict:
           {minsort#(add(n, x), y) -> if_minsort#(eq(n, min(add(n, x))), add(n, x), y)}
          EDG:
           {}
           SCCS:
            
            Qed
    SCC:
     Strict:
      {            rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)),
        if_rm#(true(), n, add(m, x)) -> rm#(n, x),
       if_rm#(false(), n, add(m, x)) -> rm#(n, x)}
     Weak:
     {                      eq(0(), 0()) -> true(),
                           eq(0(), s(x)) -> false(),
                           eq(s(x), 0()) -> false(),
                          eq(s(x), s(y)) -> eq(x, y),
                              le(0(), y) -> true(),
                           le(s(x), 0()) -> false(),
                          le(s(x), s(y)) -> le(x, y),
                           app(nil(), y) -> y,
                       app(add(n, x), y) -> add(n, app(x, y)),
                      min(add(n, nil())) -> n,
                  min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x))),
       if_min(true(), add(n, add(m, x))) -> min(add(n, x)),
      if_min(false(), add(n, add(m, x))) -> min(add(m, x)),
                            rm(n, nil()) -> nil(),
                        rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
             if_rm(true(), n, add(m, x)) -> rm(n, x),
            if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                   minsort(nil(), nil()) -> nil(),
                   minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y),
        if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
       if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
     SPSC:
      Simple Projection:
       pi(if_rm#) = 2, pi(rm#) = 1
      Strict:
       {           rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)),
        if_rm#(true(), n, add(m, x)) -> rm#(n, x)}
      EDG:
       {(rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x))
        (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))}
       SCCS:
        Scc:
         {           rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)),
          if_rm#(true(), n, add(m, x)) -> rm#(n, x)}
        SCC:
         Strict:
          {           rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)),
           if_rm#(true(), n, add(m, x)) -> rm#(n, x)}
         Weak:
         {                      eq(0(), 0()) -> true(),
                               eq(0(), s(x)) -> false(),
                               eq(s(x), 0()) -> false(),
                              eq(s(x), s(y)) -> eq(x, y),
                                  le(0(), y) -> true(),
                               le(s(x), 0()) -> false(),
                              le(s(x), s(y)) -> le(x, y),
                               app(nil(), y) -> y,
                           app(add(n, x), y) -> add(n, app(x, y)),
                          min(add(n, nil())) -> n,
                      min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x))),
           if_min(true(), add(n, add(m, x))) -> min(add(n, x)),
          if_min(false(), add(n, add(m, x))) -> min(add(m, x)),
                                rm(n, nil()) -> nil(),
                            rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
                 if_rm(true(), n, add(m, x)) -> rm(n, x),
                if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                       minsort(nil(), nil()) -> nil(),
                       minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y),
            if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
           if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
         SPSC:
          Simple Projection:
           pi(if_rm#) = 2, pi(rm#) = 1
          Strict:
           {rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x))}
          EDG:
           {}
           SCCS:
            
            Qed
    SCC:
     Strict:
      {            min#(add(n, add(m, x))) -> if_min#(le(n, m), add(n, add(m, x))),
        if_min#(true(), add(n, add(m, x))) -> min#(add(n, x)),
       if_min#(false(), add(n, add(m, x))) -> min#(add(m, x))}
     Weak:
     {                      eq(0(), 0()) -> true(),
                           eq(0(), s(x)) -> false(),
                           eq(s(x), 0()) -> false(),
                          eq(s(x), s(y)) -> eq(x, y),
                              le(0(), y) -> true(),
                           le(s(x), 0()) -> false(),
                          le(s(x), s(y)) -> le(x, y),
                           app(nil(), y) -> y,
                       app(add(n, x), y) -> add(n, app(x, y)),
                      min(add(n, nil())) -> n,
                  min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x))),
       if_min(true(), add(n, add(m, x))) -> min(add(n, x)),
      if_min(false(), add(n, add(m, x))) -> min(add(m, x)),
                            rm(n, nil()) -> nil(),
                        rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
             if_rm(true(), n, add(m, x)) -> rm(n, x),
            if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                   minsort(nil(), nil()) -> nil(),
                   minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y),
        if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
       if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
     POLY:
      Argument Filtering:
       pi(if_minsort) = [], pi(minsort) = [], pi(if_rm) = [], pi(rm) = [], pi(if_min#) = 1, pi(if_min) = [], pi(min#) = 0, pi(min) = [], pi(add) = [1], pi(nil) = [], pi(app) = [], pi(le) = [], pi(s) = [], pi(false) = [], pi(0) = [], pi(eq) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [add](x0) = x0 + 1
      Strict:
       {min#(add(n, add(m, x))) -> if_min#(le(n, m), add(n, add(m, x)))}
      Weak:
       {                      eq(0(), 0()) -> true(),
                             eq(0(), s(x)) -> false(),
                             eq(s(x), 0()) -> false(),
                            eq(s(x), s(y)) -> eq(x, y),
                                le(0(), y) -> true(),
                             le(s(x), 0()) -> false(),
                            le(s(x), s(y)) -> le(x, y),
                             app(nil(), y) -> y,
                         app(add(n, x), y) -> add(n, app(x, y)),
                        min(add(n, nil())) -> n,
                    min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x))),
         if_min(true(), add(n, add(m, x))) -> min(add(n, x)),
        if_min(false(), add(n, add(m, x))) -> min(add(m, x)),
                              rm(n, nil()) -> nil(),
                          rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
               if_rm(true(), n, add(m, x)) -> rm(n, x),
              if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                     minsort(nil(), nil()) -> nil(),
                     minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y),
          if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
         if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {app#(add(n, x), y) -> app#(x, y)}
     Weak:
     {                      eq(0(), 0()) -> true(),
                           eq(0(), s(x)) -> false(),
                           eq(s(x), 0()) -> false(),
                          eq(s(x), s(y)) -> eq(x, y),
                              le(0(), y) -> true(),
                           le(s(x), 0()) -> false(),
                          le(s(x), s(y)) -> le(x, y),
                           app(nil(), y) -> y,
                       app(add(n, x), y) -> add(n, app(x, y)),
                      min(add(n, nil())) -> n,
                  min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x))),
       if_min(true(), add(n, add(m, x))) -> min(add(n, x)),
      if_min(false(), add(n, add(m, x))) -> min(add(m, x)),
                            rm(n, nil()) -> nil(),
                        rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
             if_rm(true(), n, add(m, x)) -> rm(n, x),
            if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                   minsort(nil(), nil()) -> nil(),
                   minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y),
        if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
       if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
     SPSC:
      Simple Projection:
       pi(app#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {le#(s(x), s(y)) -> le#(x, y)}
     Weak:
     {                      eq(0(), 0()) -> true(),
                           eq(0(), s(x)) -> false(),
                           eq(s(x), 0()) -> false(),
                          eq(s(x), s(y)) -> eq(x, y),
                              le(0(), y) -> true(),
                           le(s(x), 0()) -> false(),
                          le(s(x), s(y)) -> le(x, y),
                           app(nil(), y) -> y,
                       app(add(n, x), y) -> add(n, app(x, y)),
                      min(add(n, nil())) -> n,
                  min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x))),
       if_min(true(), add(n, add(m, x))) -> min(add(n, x)),
      if_min(false(), add(n, add(m, x))) -> min(add(m, x)),
                            rm(n, nil()) -> nil(),
                        rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
             if_rm(true(), n, add(m, x)) -> rm(n, x),
            if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                   minsort(nil(), nil()) -> nil(),
                   minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y),
        if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
       if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {eq#(s(x), s(y)) -> eq#(x, y)}
     Weak:
     {                      eq(0(), 0()) -> true(),
                           eq(0(), s(x)) -> false(),
                           eq(s(x), 0()) -> false(),
                          eq(s(x), s(y)) -> eq(x, y),
                              le(0(), y) -> true(),
                           le(s(x), 0()) -> false(),
                          le(s(x), s(y)) -> le(x, y),
                           app(nil(), y) -> y,
                       app(add(n, x), y) -> add(n, app(x, y)),
                      min(add(n, nil())) -> n,
                  min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x))),
       if_min(true(), add(n, add(m, x))) -> min(add(n, x)),
      if_min(false(), add(n, add(m, x))) -> min(add(m, x)),
                            rm(n, nil()) -> nil(),
                        rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
             if_rm(true(), n, add(m, x)) -> rm(n, x),
            if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                   minsort(nil(), nil()) -> nil(),
                   minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y),
        if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
       if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
     SPSC:
      Simple Projection:
       pi(eq#) = 0
      Strict:
       {}
      Qed