YES

Proof:
This system is quasi-decreasing.
By \cite{A14}, Theorem 11.5.9.
This system is of type 3 or smaller.
This system is deterministic.
System R transformed to V(R) + Emb.
Call external tool:
ttt2 - trs 30
Input:
  le(0, s(x)) -> true
  le(x, 0) -> false
  le(s(x), s(y)) -> le(x, y)
  min(cons(x, nil)) -> x
  min(cons(x, l)) -> x
  min(cons(x, l)) -> le(x, min(l))
  min(cons(x, l)) -> min(l)
  s(x) -> x
  min(x) -> x
  le(x, y) -> x
  le(x, y) -> y
  cons(x, y) -> x
  cons(x, y) -> y

 DP Processor:
  DPs:
   le#(s(x),s(y)) -> le#(x,y)
   min#(cons(x,l)) -> min#(l)
   min#(cons(x,l)) -> le#(x,min(l))
  TRS:
   le(0(),s(x)) -> true()
   le(x,0()) -> false()
   le(s(x),s(y)) -> le(x,y)
   min(cons(x,nil())) -> x
   min(cons(x,l)) -> x
   min(cons(x,l)) -> le(x,min(l))
   min(cons(x,l)) -> min(l)
   s(x) -> x
   min(x) -> x
   le(x,y) -> x
   le(x,y) -> y
   cons(x,y) -> x
   cons(x,y) -> y
  TDG Processor:
   DPs:
    le#(s(x),s(y)) -> le#(x,y)
    min#(cons(x,l)) -> min#(l)
    min#(cons(x,l)) -> le#(x,min(l))
   TRS:
    le(0(),s(x)) -> true()
    le(x,0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    min(cons(x,nil())) -> x
    min(cons(x,l)) -> x
    min(cons(x,l)) -> le(x,min(l))
    min(cons(x,l)) -> min(l)
    s(x) -> x
    min(x) -> x
    le(x,y) -> x
    le(x,y) -> y
    cons(x,y) -> x
    cons(x,y) -> y
   graph:
    min#(cons(x,l)) -> min#(l) -> min#(cons(x,l)) -> le#(x,min(l))
    min#(cons(x,l)) -> min#(l) -> min#(cons(x,l)) -> min#(l)
    min#(cons(x,l)) -> le#(x,min(l)) -> le#(s(x),s(y)) -> le#(x,y)
    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 4/9
    DPs:
     min#(cons(x,l)) -> min#(l)
    TRS:
     le(0(),s(x)) -> true()
     le(x,0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     min(cons(x,nil())) -> x
     min(cons(x,l)) -> x
     min(cons(x,l)) -> le(x,min(l))
     min(cons(x,l)) -> min(l)
     s(x) -> x
     min(x) -> x
     le(x,y) -> x
     le(x,y) -> y
     cons(x,y) -> x
     cons(x,y) -> y
    Subterm Criterion Processor:
     simple projection:
      pi(min#) = 0
     problem:
      DPs:
       
      TRS:
       le(0(),s(x)) -> true()
       le(x,0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       min(cons(x,nil())) -> x
       min(cons(x,l)) -> x
       min(cons(x,l)) -> le(x,min(l))
       min(cons(x,l)) -> min(l)
       s(x) -> x
       min(x) -> x
       le(x,y) -> x
       le(x,y) -> y
       cons(x,y) -> x
       cons(x,y) -> y
     Qed
    
    DPs:
     le#(s(x),s(y)) -> le#(x,y)
    TRS:
     le(0(),s(x)) -> true()
     le(x,0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     min(cons(x,nil())) -> x
     min(cons(x,l)) -> x
     min(cons(x,l)) -> le(x,min(l))
     min(cons(x,l)) -> min(l)
     s(x) -> x
     min(x) -> x
     le(x,y) -> x
     le(x,y) -> y
     cons(x,y) -> x
     cons(x,y) -> y
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 0
     problem:
      DPs:
       
      TRS:
       le(0(),s(x)) -> true()
       le(x,0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       min(cons(x,nil())) -> x
       min(cons(x,l)) -> x
       min(cons(x,l)) -> le(x,min(l))
       min(cons(x,l)) -> min(l)
       s(x) -> x
       min(x) -> x
       le(x,y) -> x
       le(x,y) -> y
       cons(x,y) -> x
       cons(x,y) -> y
     Qed