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:
  sub(z, 0) -> z
  ?1(x, z, y) -> x
  sub(s(z), s(y)) -> ?1(sub(z, y), z, y)

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