YES

Proof:
This system is confluent.
By \cite{ALS94}, Theorem 4.1.
This system is of type 3 or smaller.
This system is strongly deterministic.
There are no critical pairs.
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:
  size(empty) -> 0
  size(push(x, y)) -> s(size(x))
  m -> s(s(s(s(0))))
  pop(empty) -> empty
  pop(push(x, y)) -> x
  pop(push(x, y)) -> le(size(x), m)
  top(empty) -> eentry
  top(push(x, y)) -> y
  top(push(x, y)) -> le(size(x), m)
  le(x, 0) -> false
  le(0, s(x)) -> true
  le(s(x), s(y)) -> le(x, y)
  size(x) -> x
  top(x) -> x
  s(x) -> x
  pop(x) -> x
  push(x, y) -> x
  push(x, y) -> y
  le(x, y) -> x
  le(x, y) -> y

 DP Processor:
  DPs:
   size#(push(x,y)) -> size#(x)
   size#(push(x,y)) -> s#(size(x))
   m#() -> s#(0())
   m#() -> s#(s(0()))
   m#() -> s#(s(s(0())))
   m#() -> s#(s(s(s(0()))))
   pop#(push(x,y)) -> m#()
   pop#(push(x,y)) -> size#(x)
   pop#(push(x,y)) -> le#(size(x),m())
   top#(push(x,y)) -> m#()
   top#(push(x,y)) -> size#(x)
   top#(push(x,y)) -> le#(size(x),m())
   le#(s(x),s(y)) -> le#(x,y)
  TRS:
   size(empty()) -> 0()
   size(push(x,y)) -> s(size(x))
   m() -> s(s(s(s(0()))))
   pop(empty()) -> empty()
   pop(push(x,y)) -> x
   pop(push(x,y)) -> le(size(x),m())
   top(empty()) -> eentry()
   top(push(x,y)) -> y
   top(push(x,y)) -> le(size(x),m())
   le(x,0()) -> false()
   le(0(),s(x)) -> true()
   le(s(x),s(y)) -> le(x,y)
   size(x) -> x
   top(x) -> x
   s(x) -> x
   pop(x) -> x
   push(x,y) -> x
   push(x,y) -> y
   le(x,y) -> x
   le(x,y) -> y
  TDG Processor:
   DPs:
    size#(push(x,y)) -> size#(x)
    size#(push(x,y)) -> s#(size(x))
    m#() -> s#(0())
    m#() -> s#(s(0()))
    m#() -> s#(s(s(0())))
    m#() -> s#(s(s(s(0()))))
    pop#(push(x,y)) -> m#()
    pop#(push(x,y)) -> size#(x)
    pop#(push(x,y)) -> le#(size(x),m())
    top#(push(x,y)) -> m#()
    top#(push(x,y)) -> size#(x)
    top#(push(x,y)) -> le#(size(x),m())
    le#(s(x),s(y)) -> le#(x,y)
   TRS:
    size(empty()) -> 0()
    size(push(x,y)) -> s(size(x))
    m() -> s(s(s(s(0()))))
    pop(empty()) -> empty()
    pop(push(x,y)) -> x
    pop(push(x,y)) -> le(size(x),m())
    top(empty()) -> eentry()
    top(push(x,y)) -> y
    top(push(x,y)) -> le(size(x),m())
    le(x,0()) -> false()
    le(0(),s(x)) -> true()
    le(s(x),s(y)) -> le(x,y)
    size(x) -> x
    top(x) -> x
    s(x) -> x
    pop(x) -> x
    push(x,y) -> x
    push(x,y) -> y
    le(x,y) -> x
    le(x,y) -> y
   graph:
    top#(push(x,y)) -> le#(size(x),m()) -> le#(s(x),s(y)) -> le#(x,y)
    top#(push(x,y)) -> m#() -> m#() -> s#(s(s(s(0()))))
    top#(push(x,y)) -> m#() -> m#() -> s#(s(s(0())))
    top#(push(x,y)) -> m#() -> m#() -> s#(s(0()))
    top#(push(x,y)) -> m#() -> m#() -> s#(0())
    top#(push(x,y)) -> size#(x) -> size#(push(x,y)) -> s#(size(x))
    top#(push(x,y)) -> size#(x) -> size#(push(x,y)) -> size#(x)
    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
    pop#(push(x,y)) -> le#(size(x),m()) -> le#(s(x),s(y)) -> le#(x,y)
    pop#(push(x,y)) -> m#() -> m#() -> s#(s(s(s(0()))))
    pop#(push(x,y)) -> m#() -> m#() -> s#(s(s(0())))
    pop#(push(x,y)) -> m#() -> m#() -> s#(s(0()))
    pop#(push(x,y)) -> m#() -> m#() -> s#(0())
    pop#(push(x,y)) -> size#(x) -> size#(push(x,y)) -> s#(size(x))
    pop#(push(x,y)) -> size#(x) -> size#(push(x,y)) -> size#(x)
    size#(push(x,y)) -> size#(x) -> size#(push(x,y)) -> s#(size(x))
    size#(push(x,y)) -> size#(x) -> size#(push(x,y)) -> size#(x)
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 17/169
    DPs:
     size#(push(x,y)) -> size#(x)
    TRS:
     size(empty()) -> 0()
     size(push(x,y)) -> s(size(x))
     m() -> s(s(s(s(0()))))
     pop(empty()) -> empty()
     pop(push(x,y)) -> x
     pop(push(x,y)) -> le(size(x),m())
     top(empty()) -> eentry()
     top(push(x,y)) -> y
     top(push(x,y)) -> le(size(x),m())
     le(x,0()) -> false()
     le(0(),s(x)) -> true()
     le(s(x),s(y)) -> le(x,y)
     size(x) -> x
     top(x) -> x
     s(x) -> x
     pop(x) -> x
     push(x,y) -> x
     push(x,y) -> y
     le(x,y) -> x
     le(x,y) -> y
    Subterm Criterion Processor:
     simple projection:
      pi(size#) = 0
     problem:
      DPs:
       
      TRS:
       size(empty()) -> 0()
       size(push(x,y)) -> s(size(x))
       m() -> s(s(s(s(0()))))
       pop(empty()) -> empty()
       pop(push(x,y)) -> x
       pop(push(x,y)) -> le(size(x),m())
       top(empty()) -> eentry()
       top(push(x,y)) -> y
       top(push(x,y)) -> le(size(x),m())
       le(x,0()) -> false()
       le(0(),s(x)) -> true()
       le(s(x),s(y)) -> le(x,y)
       size(x) -> x
       top(x) -> x
       s(x) -> x
       pop(x) -> x
       push(x,y) -> x
       push(x,y) -> y
       le(x,y) -> x
       le(x,y) -> y
     Qed
    
    DPs:
     le#(s(x),s(y)) -> le#(x,y)
    TRS:
     size(empty()) -> 0()
     size(push(x,y)) -> s(size(x))
     m() -> s(s(s(s(0()))))
     pop(empty()) -> empty()
     pop(push(x,y)) -> x
     pop(push(x,y)) -> le(size(x),m())
     top(empty()) -> eentry()
     top(push(x,y)) -> y
     top(push(x,y)) -> le(size(x),m())
     le(x,0()) -> false()
     le(0(),s(x)) -> true()
     le(s(x),s(y)) -> le(x,y)
     size(x) -> x
     top(x) -> x
     s(x) -> x
     pop(x) -> x
     push(x,y) -> x
     push(x,y) -> y
     le(x,y) -> x
     le(x,y) -> y
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 0
     problem:
      DPs:
       
      TRS:
       size(empty()) -> 0()
       size(push(x,y)) -> s(size(x))
       m() -> s(s(s(s(0()))))
       pop(empty()) -> empty()
       pop(push(x,y)) -> x
       pop(push(x,y)) -> le(size(x),m())
       top(empty()) -> eentry()
       top(push(x,y)) -> y
       top(push(x,y)) -> le(size(x),m())
       le(x,0()) -> false()
       le(0(),s(x)) -> true()
       le(s(x),s(y)) -> le(x,y)
       size(x) -> x
       top(x) -> x
       s(x) -> x
       pop(x) -> x
       push(x,y) -> x
       push(x,y) -> y
       le(x,y) -> x
       le(x,y) -> y
     Qed