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:
  s(p(x)) -> x
  p(s(x)) -> x
  lte(s(x), y) -> lte(x, p(y))
  lte(p(x), y) -> lte(x, s(y))
  lte(0, 0) -> T
  lte(0, p(0)) -> F
  ?2(T, x) -> T
  lte(0, s(x)) -> ?2(lte(0, x), x)
  ?1(F, x) -> F
  lte(0, p(x)) -> ?1(lte(0, x), x)

 DP Processor:
  DPs:
   lte#(s(x),y) -> p#(y)
   lte#(s(x),y) -> lte#(x,p(y))
   lte#(p(x),y) -> s#(y)
   lte#(p(x),y) -> lte#(x,s(y))
   lte#(0(),s(x)) -> lte#(0(),x)
   lte#(0(),s(x)) -> ?2#(lte(0(),x),x)
   lte#(0(),p(x)) -> lte#(0(),x)
   lte#(0(),p(x)) -> ?1#(lte(0(),x),x)
  TRS:
   s(p(x)) -> x
   p(s(x)) -> x
   lte(s(x),y) -> lte(x,p(y))
   lte(p(x),y) -> lte(x,s(y))
   lte(0(),0()) -> T()
   lte(0(),p(0())) -> F()
   ?2(T(),x) -> T()
   lte(0(),s(x)) -> ?2(lte(0(),x),x)
   ?1(F(),x) -> F()
   lte(0(),p(x)) -> ?1(lte(0(),x),x)
  TDG Processor:
   DPs:
    lte#(s(x),y) -> p#(y)
    lte#(s(x),y) -> lte#(x,p(y))
    lte#(p(x),y) -> s#(y)
    lte#(p(x),y) -> lte#(x,s(y))
    lte#(0(),s(x)) -> lte#(0(),x)
    lte#(0(),s(x)) -> ?2#(lte(0(),x),x)
    lte#(0(),p(x)) -> lte#(0(),x)
    lte#(0(),p(x)) -> ?1#(lte(0(),x),x)
   TRS:
    s(p(x)) -> x
    p(s(x)) -> x
    lte(s(x),y) -> lte(x,p(y))
    lte(p(x),y) -> lte(x,s(y))
    lte(0(),0()) -> T()
    lte(0(),p(0())) -> F()
    ?2(T(),x) -> T()
    lte(0(),s(x)) -> ?2(lte(0(),x),x)
    ?1(F(),x) -> F()
    lte(0(),p(x)) -> ?1(lte(0(),x),x)
   graph:
    lte#(0(),s(x)) -> lte#(0(),x) ->
    lte#(0(),p(x)) -> ?1#(lte(0(),x),x)
    lte#(0(),s(x)) -> lte#(0(),x) -> lte#(0(),p(x)) -> lte#(0(),x)
    lte#(0(),s(x)) -> lte#(0(),x) ->
    lte#(0(),s(x)) -> ?2#(lte(0(),x),x)
    lte#(0(),s(x)) -> lte#(0(),x) -> lte#(0(),s(x)) -> lte#(0(),x)
    lte#(0(),s(x)) -> lte#(0(),x) -> lte#(p(x),y) -> lte#(x,s(y))
    lte#(0(),s(x)) -> lte#(0(),x) -> lte#(p(x),y) -> s#(y)
    lte#(0(),s(x)) -> lte#(0(),x) -> lte#(s(x),y) -> lte#(x,p(y))
    lte#(0(),s(x)) -> lte#(0(),x) -> lte#(s(x),y) -> p#(y)
    lte#(0(),p(x)) -> lte#(0(),x) ->
    lte#(0(),p(x)) -> ?1#(lte(0(),x),x)
    lte#(0(),p(x)) -> lte#(0(),x) -> lte#(0(),p(x)) -> lte#(0(),x)
    lte#(0(),p(x)) -> lte#(0(),x) ->
    lte#(0(),s(x)) -> ?2#(lte(0(),x),x)
    lte#(0(),p(x)) -> lte#(0(),x) -> lte#(0(),s(x)) -> lte#(0(),x)
    lte#(0(),p(x)) -> lte#(0(),x) -> lte#(p(x),y) -> lte#(x,s(y))
    lte#(0(),p(x)) -> lte#(0(),x) -> lte#(p(x),y) -> s#(y)
    lte#(0(),p(x)) -> lte#(0(),x) -> lte#(s(x),y) -> lte#(x,p(y))
    lte#(0(),p(x)) -> lte#(0(),x) -> lte#(s(x),y) -> p#(y)
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(0(),p(x)) -> ?1#(lte(0(),x),x)
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(0(),p(x)) -> lte#(0(),x)
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(0(),s(x)) -> ?2#(lte(0(),x),x)
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(0(),s(x)) -> lte#(0(),x)
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(p(x),y) -> lte#(x,s(y))
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(p(x),y) -> s#(y)
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(s(x),y) -> lte#(x,p(y))
    lte#(s(x),y) -> lte#(x,p(y)) -> lte#(s(x),y) -> p#(y)
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(0(),p(x)) -> ?1#(lte(0(),x),x)
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(0(),p(x)) -> lte#(0(),x)
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(0(),s(x)) -> ?2#(lte(0(),x),x)
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(0(),s(x)) -> lte#(0(),x)
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(p(x),y) -> lte#(x,s(y))
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(p(x),y) -> s#(y)
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(s(x),y) -> lte#(x,p(y))
    lte#(p(x),y) -> lte#(x,s(y)) -> lte#(s(x),y) -> p#(y)
   SCC Processor:
    #sccs: 1
    #rules: 4
    #arcs: 32/64
    DPs:
     lte#(0(),s(x)) -> lte#(0(),x)
     lte#(s(x),y) -> lte#(x,p(y))
     lte#(p(x),y) -> lte#(x,s(y))
     lte#(0(),p(x)) -> lte#(0(),x)
    TRS:
     s(p(x)) -> x
     p(s(x)) -> x
     lte(s(x),y) -> lte(x,p(y))
     lte(p(x),y) -> lte(x,s(y))
     lte(0(),0()) -> T()
     lte(0(),p(0())) -> F()
     ?2(T(),x) -> T()
     lte(0(),s(x)) -> ?2(lte(0(),x),x)
     ?1(F(),x) -> F()
     lte(0(),p(x)) -> ?1(lte(0(),x),x)
    Subterm Criterion Processor:
     simple projection:
      pi(lte#) = 0
     problem:
      DPs:
       lte#(0(),s(x)) -> lte#(0(),x)
       lte#(0(),p(x)) -> lte#(0(),x)
      TRS:
       s(p(x)) -> x
       p(s(x)) -> x
       lte(s(x),y) -> lte(x,p(y))
       lte(p(x),y) -> lte(x,s(y))
       lte(0(),0()) -> T()
       lte(0(),p(0())) -> F()
       ?2(T(),x) -> T()
       lte(0(),s(x)) -> ?2(lte(0(),x),x)
       ?1(F(),x) -> F()
       lte(0(),p(x)) -> ?1(lte(0(),x),x)
     Subterm Criterion Processor:
      simple projection:
       pi(lte#) = 1
      problem:
       DPs:
        
       TRS:
        s(p(x)) -> x
        p(s(x)) -> x
        lte(s(x),y) -> lte(x,p(y))
        lte(p(x),y) -> lte(x,s(y))
        lte(0(),0()) -> T()
        lte(0(),p(0())) -> F()
        ?2(T(),x) -> T()
        lte(0(),s(x)) -> ?2(lte(0(),x),x)
        ?1(F(),x) -> F()
        lte(0(),p(x)) -> ?1(lte(0(),x),x)
      Qed