YES

Problem:
 minus(X,s(Y)) -> pred(minus(X,Y))
 minus(X,0()) -> X
 pred(s(X)) -> X
 le(s(X),s(Y)) -> le(X,Y)
 le(s(X),0()) -> false()
 le(0(),Y) -> true()
 gcd(0(),Y) -> 0()
 gcd(s(X),0()) -> s(X)
 gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
 if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
 if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))

Proof:
 DP Processor:
  DPs:
   minus#(X,s(Y)) -> minus#(X,Y)
   minus#(X,s(Y)) -> pred#(minus(X,Y))
   le#(s(X),s(Y)) -> le#(X,Y)
   gcd#(s(X),s(Y)) -> le#(Y,X)
   gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y))
   if#(true(),s(X),s(Y)) -> minus#(X,Y)
   if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y))
   if#(false(),s(X),s(Y)) -> minus#(Y,X)
   if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X))
  TRS:
   minus(X,s(Y)) -> pred(minus(X,Y))
   minus(X,0()) -> X
   pred(s(X)) -> X
   le(s(X),s(Y)) -> le(X,Y)
   le(s(X),0()) -> false()
   le(0(),Y) -> true()
   gcd(0(),Y) -> 0()
   gcd(s(X),0()) -> s(X)
   gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
   if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
   if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
  Usable Rule Processor:
   DPs:
    minus#(X,s(Y)) -> minus#(X,Y)
    minus#(X,s(Y)) -> pred#(minus(X,Y))
    le#(s(X),s(Y)) -> le#(X,Y)
    gcd#(s(X),s(Y)) -> le#(Y,X)
    gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y))
    if#(true(),s(X),s(Y)) -> minus#(X,Y)
    if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y))
    if#(false(),s(X),s(Y)) -> minus#(Y,X)
    if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X))
   TRS:
    f14(x,y) -> x
    f14(x,y) -> y
    minus(X,s(Y)) -> pred(minus(X,Y))
    minus(X,0()) -> X
    pred(s(X)) -> X
    le(s(X),s(Y)) -> le(X,Y)
    le(s(X),0()) -> false()
    le(0(),Y) -> true()
   TDG Processor:
    DPs:
     minus#(X,s(Y)) -> minus#(X,Y)
     minus#(X,s(Y)) -> pred#(minus(X,Y))
     le#(s(X),s(Y)) -> le#(X,Y)
     gcd#(s(X),s(Y)) -> le#(Y,X)
     gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y))
     if#(true(),s(X),s(Y)) -> minus#(X,Y)
     if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y))
     if#(false(),s(X),s(Y)) -> minus#(Y,X)
     if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X))
    TRS:
     f14(x,y) -> x
     f14(x,y) -> y
     minus(X,s(Y)) -> pred(minus(X,Y))
     minus(X,0()) -> X
     pred(s(X)) -> X
     le(s(X),s(Y)) -> le(X,Y)
     le(s(X),0()) -> false()
     le(0(),Y) -> true()
    graph:
     if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y)) ->
     gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y))
     if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y)) ->
     gcd#(s(X),s(Y)) -> le#(Y,X)
     if#(true(),s(X),s(Y)) -> minus#(X,Y) ->
     minus#(X,s(Y)) -> pred#(minus(X,Y))
     if#(true(),s(X),s(Y)) -> minus#(X,Y) ->
     minus#(X,s(Y)) -> minus#(X,Y)
     if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X)) ->
     gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y))
     if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X)) ->
     gcd#(s(X),s(Y)) -> le#(Y,X)
     if#(false(),s(X),s(Y)) -> minus#(Y,X) ->
     minus#(X,s(Y)) -> pred#(minus(X,Y))
     if#(false(),s(X),s(Y)) -> minus#(Y,X) ->
     minus#(X,s(Y)) -> minus#(X,Y)
     gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) ->
     if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X))
     gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) ->
     if#(false(),s(X),s(Y)) -> minus#(Y,X)
     gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) ->
     if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y))
     gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) ->
     if#(true(),s(X),s(Y)) -> minus#(X,Y)
     gcd#(s(X),s(Y)) -> le#(Y,X) -> le#(s(X),s(Y)) -> le#(X,Y)
     le#(s(X),s(Y)) -> le#(X,Y) -> le#(s(X),s(Y)) -> le#(X,Y)
     minus#(X,s(Y)) -> minus#(X,Y) ->
     minus#(X,s(Y)) -> pred#(minus(X,Y))
     minus#(X,s(Y)) -> minus#(X,Y) -> minus#(X,s(Y)) -> minus#(X,Y)
    Restore Modifier:
     DPs:
      minus#(X,s(Y)) -> minus#(X,Y)
      minus#(X,s(Y)) -> pred#(minus(X,Y))
      le#(s(X),s(Y)) -> le#(X,Y)
      gcd#(s(X),s(Y)) -> le#(Y,X)
      gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y))
      if#(true(),s(X),s(Y)) -> minus#(X,Y)
      if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y))
      if#(false(),s(X),s(Y)) -> minus#(Y,X)
      if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X))
     TRS:
      minus(X,s(Y)) -> pred(minus(X,Y))
      minus(X,0()) -> X
      pred(s(X)) -> X
      le(s(X),s(Y)) -> le(X,Y)
      le(s(X),0()) -> false()
      le(0(),Y) -> true()
      gcd(0(),Y) -> 0()
      gcd(s(X),0()) -> s(X)
      gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
      if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
      if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
     SCC Processor:
      #sccs: 3
      #rules: 5
      #arcs: 16/81
      DPs:
       if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y))
       gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y))
       if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X))
      TRS:
       minus(X,s(Y)) -> pred(minus(X,Y))
       minus(X,0()) -> X
       pred(s(X)) -> X
       le(s(X),s(Y)) -> le(X,Y)
       le(s(X),0()) -> false()
       le(0(),Y) -> true()
       gcd(0(),Y) -> 0()
       gcd(s(X),0()) -> s(X)
       gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
       if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
       if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [if#](x0, x1, x2) = x1 + x2,
        
        [gcd#](x0, x1) = x0 + x1 + 1,
        
        [if](x0, x1, x2) = x1 + x2 + 1,
        
        [gcd](x0, x1) = x0 + x1 + 1,
        
        [true] = 0,
        
        [false] = 0,
        
        [le](x0, x1) = 0,
        
        [0] = 1,
        
        [pred](x0) = x0,
        
        [minus](x0, x1) = x0,
        
        [s](x0) = x0 + 1
       orientation:
        if#(true(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd#(minus(X,Y),s(Y))
        
        gcd#(s(X),s(Y)) = X + Y + 3 >= X + Y + 2 = if#(le(Y,X),s(X),s(Y))
        
        if#(false(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd#(minus(Y,X),s(X))
        
        minus(X,s(Y)) = X >= X = pred(minus(X,Y))
        
        minus(X,0()) = X >= X = X
        
        pred(s(X)) = X + 1 >= X = X
        
        le(s(X),s(Y)) = 0 >= 0 = le(X,Y)
        
        le(s(X),0()) = 0 >= 0 = false()
        
        le(0(),Y) = 0 >= 0 = true()
        
        gcd(0(),Y) = Y + 2 >= 1 = 0()
        
        gcd(s(X),0()) = X + 3 >= X + 1 = s(X)
        
        gcd(s(X),s(Y)) = X + Y + 3 >= X + Y + 3 = if(le(Y,X),s(X),s(Y))
        
        if(true(),s(X),s(Y)) = X + Y + 3 >= X + Y + 2 = gcd(minus(X,Y),s(Y))
        
        if(false(),s(X),s(Y)) = X + Y + 3 >= X + Y + 2 = gcd(minus(Y,X),s(X))
       problem:
        DPs:
         if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y))
         if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X))
        TRS:
         minus(X,s(Y)) -> pred(minus(X,Y))
         minus(X,0()) -> X
         pred(s(X)) -> X
         le(s(X),s(Y)) -> le(X,Y)
         le(s(X),0()) -> false()
         le(0(),Y) -> true()
         gcd(0(),Y) -> 0()
         gcd(s(X),0()) -> s(X)
         gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
         if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
         if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [if#](x0, x1, x2) = x0,
         
         [gcd#](x0, x1) = 0,
         
         [if](x0, x1, x2) = x1 + x2,
         
         [gcd](x0, x1) = x0 + x1,
         
         [true] = 0,
         
         [false] = 1,
         
         [le](x0, x1) = 1,
         
         [0] = 0,
         
         [pred](x0) = x0,
         
         [minus](x0, x1) = x0 + 1,
         
         [s](x0) = x0 + 1
        orientation:
         if#(true(),s(X),s(Y)) = 0 >= 0 = gcd#(minus(X,Y),s(Y))
         
         if#(false(),s(X),s(Y)) = 1 >= 0 = gcd#(minus(Y,X),s(X))
         
         minus(X,s(Y)) = X + 1 >= X + 1 = pred(minus(X,Y))
         
         minus(X,0()) = X + 1 >= X = X
         
         pred(s(X)) = X + 1 >= X = X
         
         le(s(X),s(Y)) = 1 >= 1 = le(X,Y)
         
         le(s(X),0()) = 1 >= 1 = false()
         
         le(0(),Y) = 1 >= 0 = true()
         
         gcd(0(),Y) = Y >= 0 = 0()
         
         gcd(s(X),0()) = X + 1 >= X + 1 = s(X)
         
         gcd(s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = if(le(Y,X),s(X),s(Y))
         
         if(true(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd(minus(X,Y),s(Y))
         
         if(false(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd(minus(Y,X),s(X))
        problem:
         DPs:
          if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y))
         TRS:
          minus(X,s(Y)) -> pred(minus(X,Y))
          minus(X,0()) -> X
          pred(s(X)) -> X
          le(s(X),s(Y)) -> le(X,Y)
          le(s(X),0()) -> false()
          le(0(),Y) -> true()
          gcd(0(),Y) -> 0()
          gcd(s(X),0()) -> s(X)
          gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
          if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
          if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
        Matrix Interpretation Processor:
         dimension: 1
         interpretation:
          [if#](x0, x1, x2) = x2,
          
          [gcd#](x0, x1) = 0,
          
          [if](x0, x1, x2) = x1 + x2 + 1,
          
          [gcd](x0, x1) = x0 + x1 + 1,
          
          [true] = 1,
          
          [false] = 1,
          
          [le](x0, x1) = 1,
          
          [0] = 0,
          
          [pred](x0) = x0,
          
          [minus](x0, x1) = x0,
          
          [s](x0) = x0 + 1
         orientation:
          if#(true(),s(X),s(Y)) = Y + 1 >= 0 = gcd#(minus(X,Y),s(Y))
          
          minus(X,s(Y)) = X >= X = pred(minus(X,Y))
          
          minus(X,0()) = X >= X = X
          
          pred(s(X)) = X + 1 >= X = X
          
          le(s(X),s(Y)) = 1 >= 1 = le(X,Y)
          
          le(s(X),0()) = 1 >= 1 = false()
          
          le(0(),Y) = 1 >= 1 = true()
          
          gcd(0(),Y) = Y + 1 >= 0 = 0()
          
          gcd(s(X),0()) = X + 2 >= X + 1 = s(X)
          
          gcd(s(X),s(Y)) = X + Y + 3 >= X + Y + 3 = if(le(Y,X),s(X),s(Y))
          
          if(true(),s(X),s(Y)) = X + Y + 3 >= X + Y + 2 = gcd(minus(X,Y),s(Y))
          
          if(false(),s(X),s(Y)) = X + Y + 3 >= X + Y + 2 = gcd(minus(Y,X),s(X))
         problem:
          DPs:
           
          TRS:
           minus(X,s(Y)) -> pred(minus(X,Y))
           minus(X,0()) -> X
           pred(s(X)) -> X
           le(s(X),s(Y)) -> le(X,Y)
           le(s(X),0()) -> false()
           le(0(),Y) -> true()
           gcd(0(),Y) -> 0()
           gcd(s(X),0()) -> s(X)
           gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
           if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
           if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
         Qed
      
      DPs:
       minus#(X,s(Y)) -> minus#(X,Y)
      TRS:
       minus(X,s(Y)) -> pred(minus(X,Y))
       minus(X,0()) -> X
       pred(s(X)) -> X
       le(s(X),s(Y)) -> le(X,Y)
       le(s(X),0()) -> false()
       le(0(),Y) -> true()
       gcd(0(),Y) -> 0()
       gcd(s(X),0()) -> s(X)
       gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
       if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
       if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [minus#](x0, x1) = x1 + 1,
        
        [if](x0, x1, x2) = x1 + x2,
        
        [gcd](x0, x1) = x0 + x1,
        
        [true] = 0,
        
        [false] = 0,
        
        [le](x0, x1) = 0,
        
        [0] = 0,
        
        [pred](x0) = x0,
        
        [minus](x0, x1) = x0 + 1,
        
        [s](x0) = x0 + 1
       orientation:
        minus#(X,s(Y)) = Y + 2 >= Y + 1 = minus#(X,Y)
        
        minus(X,s(Y)) = X + 1 >= X + 1 = pred(minus(X,Y))
        
        minus(X,0()) = X + 1 >= X = X
        
        pred(s(X)) = X + 1 >= X = X
        
        le(s(X),s(Y)) = 0 >= 0 = le(X,Y)
        
        le(s(X),0()) = 0 >= 0 = false()
        
        le(0(),Y) = 0 >= 0 = true()
        
        gcd(0(),Y) = Y >= 0 = 0()
        
        gcd(s(X),0()) = X + 1 >= X + 1 = s(X)
        
        gcd(s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = if(le(Y,X),s(X),s(Y))
        
        if(true(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd(minus(X,Y),s(Y))
        
        if(false(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd(minus(Y,X),s(X))
       problem:
        DPs:
         
        TRS:
         minus(X,s(Y)) -> pred(minus(X,Y))
         minus(X,0()) -> X
         pred(s(X)) -> X
         le(s(X),s(Y)) -> le(X,Y)
         le(s(X),0()) -> false()
         le(0(),Y) -> true()
         gcd(0(),Y) -> 0()
         gcd(s(X),0()) -> s(X)
         gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
         if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
         if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
       Qed
      
      DPs:
       le#(s(X),s(Y)) -> le#(X,Y)
      TRS:
       minus(X,s(Y)) -> pred(minus(X,Y))
       minus(X,0()) -> X
       pred(s(X)) -> X
       le(s(X),s(Y)) -> le(X,Y)
       le(s(X),0()) -> false()
       le(0(),Y) -> true()
       gcd(0(),Y) -> 0()
       gcd(s(X),0()) -> s(X)
       gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
       if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
       if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [le#](x0, x1) = x1 + 1,
        
        [if](x0, x1, x2) = x1 + x2,
        
        [gcd](x0, x1) = x0 + x1,
        
        [true] = 0,
        
        [false] = 0,
        
        [le](x0, x1) = 0,
        
        [0] = 0,
        
        [pred](x0) = x0,
        
        [minus](x0, x1) = x0 + 1,
        
        [s](x0) = x0 + 1
       orientation:
        le#(s(X),s(Y)) = Y + 2 >= Y + 1 = le#(X,Y)
        
        minus(X,s(Y)) = X + 1 >= X + 1 = pred(minus(X,Y))
        
        minus(X,0()) = X + 1 >= X = X
        
        pred(s(X)) = X + 1 >= X = X
        
        le(s(X),s(Y)) = 0 >= 0 = le(X,Y)
        
        le(s(X),0()) = 0 >= 0 = false()
        
        le(0(),Y) = 0 >= 0 = true()
        
        gcd(0(),Y) = Y >= 0 = 0()
        
        gcd(s(X),0()) = X + 1 >= X + 1 = s(X)
        
        gcd(s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = if(le(Y,X),s(X),s(Y))
        
        if(true(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd(minus(X,Y),s(Y))
        
        if(false(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd(minus(Y,X),s(X))
       problem:
        DPs:
         
        TRS:
         minus(X,s(Y)) -> pred(minus(X,Y))
         minus(X,0()) -> X
         pred(s(X)) -> X
         le(s(X),s(Y)) -> le(X,Y)
         le(s(X),0()) -> false()
         le(0(),Y) -> true()
         gcd(0(),Y) -> 0()
         gcd(s(X),0()) -> s(X)
         gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
         if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
         if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))
       Qed