YES

Problem:
 gcd(x,0()) -> x
 gcd(0(),y) -> y
 gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y)))

Proof:
 DP Processor:
  DPs:
   gcd#(s(x),s(y)) -> gcd#(-(x,y),s(y))
   gcd#(s(x),s(y)) -> gcd#(s(x),-(y,x))
  TRS:
   gcd(x,0()) -> x
   gcd(0(),y) -> y
   gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y)))
  Usable Rule Processor:
   DPs:
    gcd#(s(x),s(y)) -> gcd#(-(x,y),s(y))
    gcd#(s(x),s(y)) -> gcd#(s(x),-(y,x))
   TRS:
    
   Matrix Interpretation Processor: dim=4
    
    usable rules:
     
    interpretation:
     [gcd#](x0, x1) = [0 0 1 1]x0 + [1 1 0 1]x1,
     
                   [0 0 1 0]  
                   [0 0 0 0]  
     [-](x0, x1) = [0 1 0 0]x0
                   [0 1 0 0]  ,
     
               [0 0 1 1]     [0]
               [0 0 1 0]     [0]
     [s](x0) = [0 1 0 1]x0 + [1]
               [0 1 0 1]     [1]
    orientation:
     gcd#(s(x),s(y)) = [0 2 0 2]x + [0 1 2 2]y + [3] >= [0 2 0 0]x + [0 1 2 2]y + [1] = gcd#(-(x,y),s(y))
     
     gcd#(s(x),s(y)) = [0 2 0 2]x + [0 1 2 2]y + [3] >= [0 2 0 2]x + [0 1 1 0]y + [2] = gcd#(s(x),-(y,x))
    problem:
     DPs:
      
     TRS:
      
    Qed