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

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