YES

Proof:
This system is quasi-decreasing.
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:
  add(x, 0) -> x
  add(x, s(y)) -> s(add(x, y))
  quad(x) -> add(add(x, x), add(x, x))
  quad(x) -> add(x, x)
  quad(x) -> x
  s(x) -> x
  add(x, y) -> x
  add(x, y) -> y

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