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

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