YES

Proof:
This system is quasi-decreasing.
By \cite{O02}, p. 214, Proposition 7.2.50.
This system is of type 3 or smaller.
This system is deterministic.
System R transformed to U(R).
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
  ?3(true, x, l) -> x
  min(cons(x, l)) -> ?3(le(x, min(l)), x, l)
  ?1(false, x, l) -> min(l)
  min(cons(x, l)) -> ?1(le(x, min(l)), x, l)
  ?2(x, x, l) -> min(l)
  min(cons(x, l)) -> ?2(min(l), x, l)

 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))
   min#(cons(x,l)) -> ?3#(le(x,min(l)),x,l)
   ?1#(false(),x,l) -> min#(l)
   min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l)
   ?2#(x,x,l) -> min#(l)
   min#(cons(x,l)) -> ?2#(min(l),x,l)
  TRS:
   le(0(),s(x)) -> true()
   le(x,0()) -> false()
   le(s(x),s(y)) -> le(x,y)
   min(cons(x,nil())) -> x
   ?3(true(),x,l) -> x
   min(cons(x,l)) -> ?3(le(x,min(l)),x,l)
   ?1(false(),x,l) -> min(l)
   min(cons(x,l)) -> ?1(le(x,min(l)),x,l)
   ?2(x,x,l) -> min(l)
   min(cons(x,l)) -> ?2(min(l),x,l)
  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))
    min#(cons(x,l)) -> ?3#(le(x,min(l)),x,l)
    ?1#(false(),x,l) -> min#(l)
    min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l)
    ?2#(x,x,l) -> min#(l)
    min#(cons(x,l)) -> ?2#(min(l),x,l)
   TRS:
    le(0(),s(x)) -> true()
    le(x,0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    min(cons(x,nil())) -> x
    ?3(true(),x,l) -> x
    min(cons(x,l)) -> ?3(le(x,min(l)),x,l)
    ?1(false(),x,l) -> min(l)
    min(cons(x,l)) -> ?1(le(x,min(l)),x,l)
    ?2(x,x,l) -> min(l)
    min(cons(x,l)) -> ?2(min(l),x,l)
   graph:
    ?2#(x,x,l) -> min#(l) -> min#(cons(x,l)) -> ?2#(min(l),x,l)
    ?2#(x,x,l) -> min#(l) -> min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l)
    ?2#(x,x,l) -> min#(l) -> min#(cons(x,l)) -> ?3#(le(x,min(l)),x,l)
    ?2#(x,x,l) -> min#(l) -> min#(cons(x,l)) -> le#(x,min(l))
    ?2#(x,x,l) -> min#(l) -> min#(cons(x,l)) -> min#(l)
    ?1#(false(),x,l) -> min#(l) -> min#(cons(x,l)) -> ?2#(min(l),x,l)
    ?1#(false(),x,l) -> min#(l) ->
    min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l)
    ?1#(false(),x,l) -> min#(l) ->
    min#(cons(x,l)) -> ?3#(le(x,min(l)),x,l)
    ?1#(false(),x,l) -> min#(l) -> min#(cons(x,l)) -> le#(x,min(l))
    ?1#(false(),x,l) -> min#(l) -> min#(cons(x,l)) -> min#(l)
    min#(cons(x,l)) -> ?2#(min(l),x,l) ->
    ?2#(x,x,l) -> min#(l)
    min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l) ->
    ?1#(false(),x,l) -> min#(l)
    min#(cons(x,l)) -> min#(l) -> min#(cons(x,l)) -> ?2#(min(l),x,l)
    min#(cons(x,l)) -> min#(l) ->
    min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l)
    min#(cons(x,l)) -> min#(l) ->
    min#(cons(x,l)) -> ?3#(le(x,min(l)),x,l)
    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: 6
    #arcs: 19/64
    DPs:
     ?2#(x,x,l) -> min#(l)
     min#(cons(x,l)) -> min#(l)
     min#(cons(x,l)) -> ?1#(le(x,min(l)),x,l)
     ?1#(false(),x,l) -> min#(l)
     min#(cons(x,l)) -> ?2#(min(l),x,l)
    TRS:
     le(0(),s(x)) -> true()
     le(x,0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     min(cons(x,nil())) -> x
     ?3(true(),x,l) -> x
     min(cons(x,l)) -> ?3(le(x,min(l)),x,l)
     ?1(false(),x,l) -> min(l)
     min(cons(x,l)) -> ?1(le(x,min(l)),x,l)
     ?2(x,x,l) -> min(l)
     min(cons(x,l)) -> ?2(min(l),x,l)
    Subterm Criterion Processor:
     simple projection:
      pi(min#) = 0
      pi(?1#) = 2
      pi(?2#) = 2
     problem:
      DPs:
       ?2#(x,x,l) -> min#(l)
       ?1#(false(),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
       ?3(true(),x,l) -> x
       min(cons(x,l)) -> ?3(le(x,min(l)),x,l)
       ?1(false(),x,l) -> min(l)
       min(cons(x,l)) -> ?1(le(x,min(l)),x,l)
       ?2(x,x,l) -> min(l)
       min(cons(x,l)) -> ?2(min(l),x,l)
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 11/4
      
    
    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
     ?3(true(),x,l) -> x
     min(cons(x,l)) -> ?3(le(x,min(l)),x,l)
     ?1(false(),x,l) -> min(l)
     min(cons(x,l)) -> ?1(le(x,min(l)),x,l)
     ?2(x,x,l) -> min(l)
     min(cons(x,l)) -> ?2(min(l),x,l)
    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
       ?3(true(),x,l) -> x
       min(cons(x,l)) -> ?3(le(x,min(l)),x,l)
       ?1(false(),x,l) -> min(l)
       min(cons(x,l)) -> ?1(le(x,min(l)),x,l)
       ?2(x,x,l) -> min(l)
       min(cons(x,l)) -> ?2(min(l),x,l)
     Qed