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

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