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:
  lte(0, 0) -> tt
  lte(s(x), 0) -> ff
  lte(s(x), s(y)) -> lte(x, y)
  ?1(tt, x, y) -> tt
  lte(x, s(y)) -> ?1(lte(x, y), x, y)

 DP Processor:
  DPs:
   lte#(s(x),s(y)) -> lte#(x,y)
   lte#(x,s(y)) -> lte#(x,y)
   lte#(x,s(y)) -> ?1#(lte(x,y),x,y)
  TRS:
   lte(0(),0()) -> tt()
   lte(s(x),0()) -> ff()
   lte(s(x),s(y)) -> lte(x,y)
   ?1(tt(),x,y) -> tt()
   lte(x,s(y)) -> ?1(lte(x,y),x,y)
  TDG Processor:
   DPs:
    lte#(s(x),s(y)) -> lte#(x,y)
    lte#(x,s(y)) -> lte#(x,y)
    lte#(x,s(y)) -> ?1#(lte(x,y),x,y)
   TRS:
    lte(0(),0()) -> tt()
    lte(s(x),0()) -> ff()
    lte(s(x),s(y)) -> lte(x,y)
    ?1(tt(),x,y) -> tt()
    lte(x,s(y)) -> ?1(lte(x,y),x,y)
   graph:
    lte#(s(x),s(y)) -> lte#(x,y) -> lte#(x,s(y)) -> ?1#(lte(x,y),x,y)
    lte#(s(x),s(y)) -> lte#(x,y) -> lte#(x,s(y)) -> lte#(x,y)
    lte#(s(x),s(y)) -> lte#(x,y) -> lte#(s(x),s(y)) -> lte#(x,y)
    lte#(x,s(y)) -> lte#(x,y) -> lte#(x,s(y)) -> ?1#(lte(x,y),x,y)
    lte#(x,s(y)) -> lte#(x,y) -> lte#(x,s(y)) -> lte#(x,y)
    lte#(x,s(y)) -> lte#(x,y) -> lte#(s(x),s(y)) -> lte#(x,y)
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 6/9
    DPs:
     lte#(s(x),s(y)) -> lte#(x,y)
     lte#(x,s(y)) -> lte#(x,y)
    TRS:
     lte(0(),0()) -> tt()
     lte(s(x),0()) -> ff()
     lte(s(x),s(y)) -> lte(x,y)
     ?1(tt(),x,y) -> tt()
     lte(x,s(y)) -> ?1(lte(x,y),x,y)
    Subterm Criterion Processor:
     simple projection:
      pi(lte#) = 0
     problem:
      DPs:
       lte#(x,s(y)) -> lte#(x,y)
      TRS:
       lte(0(),0()) -> tt()
       lte(s(x),0()) -> ff()
       lte(s(x),s(y)) -> lte(x,y)
       ?1(tt(),x,y) -> tt()
       lte(x,s(y)) -> ?1(lte(x,y),x,y)
     Subterm Criterion Processor:
      simple projection:
       pi(lte#) = 1
      problem:
       DPs:
        
       TRS:
        lte(0(),0()) -> tt()
        lte(s(x),0()) -> ff()
        lte(s(x),s(y)) -> lte(x,y)
        ?1(tt(),x,y) -> tt()
        lte(x,s(y)) -> ?1(lte(x,y),x,y)
      Qed