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

 DP Processor:
  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)
   lte(x,s(y)) -> tt()
   lte(x,s(y)) -> lte(x,y)
   s(x) -> x
   lte(x,y) -> x
   lte(x,y) -> 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)
     lte(x,s(y)) -> tt()
     lte(x,s(y)) -> lte(x,y)
     s(x) -> x
     lte(x,y) -> x
     lte(x,y) -> 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)
      lte(x,s(y)) -> tt()
      lte(x,s(y)) -> lte(x,y)
      s(x) -> x
      lte(x,y) -> x
      lte(x,y) -> y
    Qed