YES

We show the termination of R/S, where R is

  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))

and S is:

  rand(x) -> x
  rand(x) -> rand(s(x))

Since R almost dominates S and S is non-duplicating,
it is enough to show finiteness of (P, Q).
Here P consists of the dependency pairs

  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))) -> if_min#(le(n,m),add(n,add(m,x)))
  min#(add(n,add(m,x))) -> le#(n,m)
  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)) -> if_rm#(eq(n,m),n,add(m,x))
  rm#(n,add(m,x)) -> eq#(n,m)
  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) -> if_minsort#(eq(n,min(add(n,x))),add(n,x),y)
  minsort#(add(n,x),y) -> eq#(n,min(add(n,x)))
  minsort#(add(n,x),y) -> min#(add(n,x))
  if_minsort#(true,add(n,x),y) -> minsort#(app(rm(n,x),y),nil)
  if_minsort#(true,add(n,x),y) -> app#(rm(n,x),y)
  if_minsort#(true,add(n,x),y) -> rm#(n,x)
  if_minsort#(false,add(n,x),y) -> minsort#(x,add(n,y))

and Q consists of the rules:

  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))
  rand(x) -> x
  rand(x) -> rand(s(x))

The weakly monotone algebra (N^3, >_lex) with

  eq#_A((x1,y1,z1),(x2,y2,z2)) = (x2, y2, z2 + 4)
  s_A((x1,y1,z1)) = (x1, y1 + 1, z1 + 1)
  le#_A((x1,y1,z1),(x2,y2,z2)) = (0, 0, 0)
  app#_A((x1,y1,z1),(x2,y2,z2)) = (0, 0, 0)
  add_A((x1,y1,z1),(x2,y2,z2)) = (x1 + x2 + 2, 2, 2)
  min#_A((x1,y1,z1)) = (1, 1, 1)
  if_min#_A((x1,y1,z1),(x2,y2,z2)) = (1, 1, 1)
  le_A((x1,y1,z1),(x2,y2,z2)) = (x1 + x2, y1 + y2 + 3, z2 + 2)
  true_A = (1, 3, 2)
  false_A = (0, 1, 4)
  rm#_A((x1,y1,z1),(x2,y2,z2)) = (x1 + x2 + 1, y1 + y2 + 3, 3)
  if_rm#_A((x1,y1,z1),(x2,y2,z2),(x3,y3,z3)) = (x2 + x3, y2 + y3, z2 + z3)
  eq_A((x1,y1,z1),(x2,y2,z2)) = (x2 + 1, 2, 1)
  minsort#_A((x1,y1,z1),(x2,y2,z2)) = (x1 + x2 + 2, 2, 4)
  if_minsort#_A((x1,y1,z1),(x2,y2,z2),(x3,y3,z3)) = (x2 + x3 + 2, 2, 4)
  min_A((x1,y1,z1)) = (x1 + 1, 1, 1)
  app_A((x1,y1,z1),(x2,y2,z2)) = (x1 + x2, y2 + 3, 1)
  rm_A((x1,y1,z1),(x2,y2,z2)) = (x2, y2 + 2, z2)
  nil_A = (0, 4, 3)
  0_A = (2, 1, 1)
  if_min_A((x1,y1,z1),(x2,y2,z2)) = (x2, 0, 2)
  if_rm_A((x1,y1,z1),(x2,y2,z2),(x3,y3,z3)) = (x3, 3, 2)
  minsort_A((x1,y1,z1),(x2,y2,z2)) = (x1 + x2 + 1, 3, 2)
  if_minsort_A((x1,y1,z1),(x2,y2,z2),(x3,y3,z3)) = (x2 + x3 + 1, 3, 2)
  rand_A((x1,y1,z1)) = (x1 + 1, 1, 0)

strictly orients the following dependency pairs:

  eq#(s(x),s(y)) -> eq#(x,y)
  min#(add(n,add(m,x))) -> le#(n,m)
  rm#(n,add(m,x)) -> if_rm#(eq(n,m),n,add(m,x))
  rm#(n,add(m,x)) -> eq#(n,m)
  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))
  if_minsort#(true,add(n,x),y) -> minsort#(app(rm(n,x),y),nil)
  if_minsort#(true,add(n,x),y) -> app#(rm(n,x),y)
  if_minsort#(true,add(n,x),y) -> rm#(n,x)

We remove them from the set of dependency pairs.

The weakly monotone algebra (N^3, >_lex) with

  le#_A((x1,y1,z1),(x2,y2,z2)) = (x1 + x2, y1, z1)
  s_A((x1,y1,z1)) = (x1, y1, z1 + 1)
  app#_A((x1,y1,z1),(x2,y2,z2)) = (x1 + x2, y2, z2)
  add_A((x1,y1,z1),(x2,y2,z2)) = (x1 + x2 + 3, y2 + 1, 1)
  min#_A((x1,y1,z1)) = (x1 + 3, 3, 2)
  if_min#_A((x1,y1,z1),(x2,y2,z2)) = (x1 + x2, y1, z1)
  le_A((x1,y1,z1),(x2,y2,z2)) = (2, 1, 1)
  true_A = (1, 4, 4)
  false_A = (1, 2, 3)
  minsort#_A((x1,y1,z1),(x2,y2,z2)) = (x1 + 3, 0, 2)
  if_minsort#_A((x1,y1,z1),(x2,y2,z2),(x3,y3,z3)) = (x2, y2, z2)
  eq_A((x1,y1,z1),(x2,y2,z2)) = (x1 + 2, 3, 3)
  min_A((x1,y1,z1)) = (x1 + 2, 1, 1)
  0_A = (1, 1, 1)
  app_A((x1,y1,z1),(x2,y2,z2)) = (x1 + x2, y1 + y2, z2 + 1)
  nil_A = (0, 0, 2)
  if_min_A((x1,y1,z1),(x2,y2,z2)) = (x2, 0, 0)
  rm_A((x1,y1,z1),(x2,y2,z2)) = (x2, y2, 2)
  if_rm_A((x1,y1,z1),(x2,y2,z2),(x3,y3,z3)) = (x3, y3, 2)
  minsort_A((x1,y1,z1),(x2,y2,z2)) = (x1 + x2 + 1, y1 + y2, 1)
  if_minsort_A((x1,y1,z1),(x2,y2,z2),(x3,y3,z3)) = (x2 + x3 + 1, y2 + y3, 1)
  rand_A((x1,y1,z1)) = (x1 + 1, y1 + 1, 0)

strictly orients the following dependency pairs:

  le#(s(x),s(y)) -> le#(x,y)
  app#(add(n,x),y) -> app#(x,y)
  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))
  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))

We remove them from the set of dependency pairs.

No dependency pair remains.