YES

Problem:
 le(0(),y) -> true()
 le(s(x),0()) -> false()
 le(s(x),s(y)) -> le(x,y)
 minus(x,0()) -> x
 minus(0(),x) -> 0()
 minus(s(x),s(y)) -> minus(x,y)
 gcd(0(),y) -> y
 gcd(s(x),0()) -> s(x)
 gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
 if_gcd(true(),x,y) -> gcd(minus(x,y),y)
 if_gcd(false(),x,y) -> gcd(minus(y,x),x)

Proof:
 DP Processor:
  DPs:
   le#(s(x),s(y)) -> le#(x,y)
   minus#(s(x),s(y)) -> minus#(x,y)
   gcd#(s(x),s(y)) -> le#(y,x)
   gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y))
   if_gcd#(true(),x,y) -> minus#(x,y)
   if_gcd#(true(),x,y) -> gcd#(minus(x,y),y)
   if_gcd#(false(),x,y) -> minus#(y,x)
   if_gcd#(false(),x,y) -> gcd#(minus(y,x),x)
  TRS:
   le(0(),y) -> true()
   le(s(x),0()) -> false()
   le(s(x),s(y)) -> le(x,y)
   minus(x,0()) -> x
   minus(0(),x) -> 0()
   minus(s(x),s(y)) -> minus(x,y)
   gcd(0(),y) -> y
   gcd(s(x),0()) -> s(x)
   gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
   if_gcd(true(),x,y) -> gcd(minus(x,y),y)
   if_gcd(false(),x,y) -> gcd(minus(y,x),x)
  TDG Processor:
   DPs:
    le#(s(x),s(y)) -> le#(x,y)
    minus#(s(x),s(y)) -> minus#(x,y)
    gcd#(s(x),s(y)) -> le#(y,x)
    gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y))
    if_gcd#(true(),x,y) -> minus#(x,y)
    if_gcd#(true(),x,y) -> gcd#(minus(x,y),y)
    if_gcd#(false(),x,y) -> minus#(y,x)
    if_gcd#(false(),x,y) -> gcd#(minus(y,x),x)
   TRS:
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    minus(x,0()) -> x
    minus(0(),x) -> 0()
    minus(s(x),s(y)) -> minus(x,y)
    gcd(0(),y) -> y
    gcd(s(x),0()) -> s(x)
    gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
    if_gcd(true(),x,y) -> gcd(minus(x,y),y)
    if_gcd(false(),x,y) -> gcd(minus(y,x),x)
   graph:
    if_gcd#(false(),x,y) -> gcd#(minus(y,x),x) ->
    gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y))
    if_gcd#(false(),x,y) -> gcd#(minus(y,x),x) ->
    gcd#(s(x),s(y)) -> le#(y,x)
    if_gcd#(false(),x,y) -> minus#(y,x) ->
    minus#(s(x),s(y)) -> minus#(x,y)
    if_gcd#(true(),x,y) -> gcd#(minus(x,y),y) ->
    gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y))
    if_gcd#(true(),x,y) -> gcd#(minus(x,y),y) ->
    gcd#(s(x),s(y)) -> le#(y,x)
    if_gcd#(true(),x,y) -> minus#(x,y) ->
    minus#(s(x),s(y)) -> minus#(x,y)
    gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) ->
    if_gcd#(false(),x,y) -> gcd#(minus(y,x),x)
    gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) ->
    if_gcd#(false(),x,y) -> minus#(y,x)
    gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) ->
    if_gcd#(true(),x,y) -> gcd#(minus(x,y),y)
    gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) ->
    if_gcd#(true(),x,y) -> minus#(x,y)
    gcd#(s(x),s(y)) -> le#(y,x) -> le#(s(x),s(y)) -> le#(x,y)
    minus#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y)
    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
   SCC Processor:
    #sccs: 3
    #rules: 5
    #arcs: 13/64
    DPs:
     if_gcd#(false(),x,y) -> gcd#(minus(y,x),x)
     gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y))
     if_gcd#(true(),x,y) -> gcd#(minus(x,y),y)
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     minus(x,0()) -> x
     minus(0(),x) -> 0()
     minus(s(x),s(y)) -> minus(x,y)
     gcd(0(),y) -> y
     gcd(s(x),0()) -> s(x)
     gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
     if_gcd(true(),x,y) -> gcd(minus(x,y),y)
     if_gcd(false(),x,y) -> gcd(minus(y,x),x)
    Extended Uncurrying Processor:
     application symbol: le
     symbol table:
      if_gcd# ==> if_gcd{0,#}/3
      gcd# ==> gcd{0,#}/2
      if_gcd ==> if_gcd0/3
      gcd ==> gcd0/2
      minus ==> minus0/2
      false ==> false0/0
      s ==> s0/1 s1/2
      true ==> true0/0
      0 ==> 00/0 01/1
      
     uncurry-rules:
      le(00(),x18) -> 01(x18)
      le(s0(x21),x22) -> s1(x21,x22)
     eta-rules:
      
     problem:
      DPs:
       if_gcd{0,#}(false0(),x,y) -> gcd{0,#}(minus0(y,x),x)
       gcd{0,#}(s0(x),s0(y)) -> if_gcd{0,#}(le(y,x),s0(x),s0(y))
       if_gcd{0,#}(true0(),x,y) -> gcd{0,#}(minus0(x,y),y)
      TRS:
       01(y) -> true0()
       s1(x,00()) -> false0()
       s1(x,s0(y)) -> le(x,y)
       minus0(x,00()) -> x
       minus0(00(),x) -> 00()
       minus0(s0(x),s0(y)) -> minus0(x,y)
       gcd0(00(),y) -> y
       gcd0(s0(x),00()) -> s0(x)
       gcd0(s0(x),s0(y)) -> if_gcd0(le(y,x),s0(x),s0(y))
       if_gcd0(true0(),x,y) -> gcd0(minus0(x,y),y)
       if_gcd0(false0(),x,y) -> gcd0(minus0(y,x),x)
       le(00(),x18) -> 01(x18)
       le(s0(x21),x22) -> s1(x21,x22)
     Extended Uncurrying Processor:
      application symbol: gcd{0,#}
      symbol table:
       if_gcd{0,#} ==> if_gcd{0,0,#}/3
       if_gcd0 ==> if_gcd{0,0}/3
       gcd0 ==> gcd{0,0}/2
       minus0 ==> minus{0,0}/2 minus0_gcd{0,#}_1#/3
       false0 ==> false{0,0}/0
       s1 ==> s{1,0}/2
       s0 ==> s{0,0}/1 s0_gcd{0,#}_1#/2
       true0 ==> true{0,0}/0
       01 ==> 0{1,0}/1
       00 ==> 0{0,0}/0
       le ==> le0/2
       
      uncurry-rules:
       gcd{0,#}(minus0(x47,x48),x49) -> minus0_gcd{0,#}_1#(x47,x48,x49)
       gcd{0,#}(s0(x45),x46) -> s0_gcd{0,#}_1#(x45,x46)
      eta-rules:
       gcd{0,#}(minus0(x,00()),x50) -> gcd{0,#}(x,x50)
       gcd{0,#}(minus0(00(),x),x51) -> gcd{0,#}(00(),x51)
       gcd{0,#}(minus0(s0(x),s0(y)),x52) -> gcd{0,#}(minus0(x,y),x52)
      problem:
       DPs:
        gcd{0,#}(minus{0,0}(x47,x48),x49) -> minus0_gcd{0,#}_1#(x47,x48,x49)
        gcd{0,#}(s{0,0}(x45),x46) -> s0_gcd{0,#}_1#(x45,x46)
        minus0_gcd{0,#}_1#(x,0{0,0}(),x50) -> gcd{0,#}(x,x50)
        minus0_gcd{0,#}_1#(0{0,0}(),x,x51) -> gcd{0,#}(0{0,0}(),x51)
        minus0_gcd{0,#}_1#(s{0,0}(x),s{0,0}(y),x52) -> minus0_gcd{0,#}_1#(x,y,x52)
        if_gcd{0,0,#}(false{0,0}(),x,y) -> minus0_gcd{0,#}_1#(y,x,x)
        s0_gcd{0,#}_1#(x,s{0,0}(y)) -> if_gcd{0,0,#}(le0(y,x),s{0,0}(x),s{0,0}(y))
        if_gcd{0,0,#}(true{0,0}(),x,y) -> minus0_gcd{0,#}_1#(x,y,y)
       TRS:
        0{1,0}(y) -> true{0,0}()
        s{1,0}(x,0{0,0}()) -> false{0,0}()
        s{1,0}(x,s{0,0}(y)) -> le0(x,y)
        minus{0,0}(x,0{0,0}()) -> x
        minus{0,0}(0{0,0}(),x) -> 0{0,0}()
        minus{0,0}(s{0,0}(x),s{0,0}(y)) -> minus{0,0}(x,y)
        gcd{0,0}(0{0,0}(),y) -> y
        gcd{0,0}(s{0,0}(x),0{0,0}()) -> s{0,0}(x)
        gcd{0,0}(s{0,0}(x),s{0,0}(y)) -> if_gcd{0,0}(le0(y,x),s{0,0}(x),s{0,0}(y))
        if_gcd{0,0}(true{0,0}(),x,y) -> gcd{0,0}(minus{0,0}(x,y),y)
        if_gcd{0,0}(false{0,0}(),x,y) -> gcd{0,0}(minus{0,0}(y,x),x)
        le0(0{0,0}(),x18) -> 0{1,0}(x18)
        le0(s{0,0}(x21),x22) -> s{1,0}(x21,x22)
      Usable Rule Processor:
       DPs:
        gcd{0,#}(minus{0,0}(x47,x48),x49) -> minus0_gcd{0,#}_1#(x47,x48,x49)
        gcd{0,#}(s{0,0}(x45),x46) -> s0_gcd{0,#}_1#(x45,x46)
        minus0_gcd{0,#}_1#(x,0{0,0}(),x50) -> gcd{0,#}(x,x50)
        minus0_gcd{0,#}_1#(0{0,0}(),x,x51) -> gcd{0,#}(0{0,0}(),x51)
        minus0_gcd{0,#}_1#(s{0,0}(x),s{0,0}(y),x52) -> minus0_gcd{0,#}_1#(x,y,x52)
        if_gcd{0,0,#}(false{0,0}(),x,y) -> minus0_gcd{0,#}_1#(y,x,x)
        s0_gcd{0,#}_1#(x,s{0,0}(y)) -> if_gcd{0,0,#}(le0(y,x),s{0,0}(x),s{0,0}(y))
        if_gcd{0,0,#}(true{0,0}(),x,y) -> minus0_gcd{0,#}_1#(x,y,y)
       TRS:
        le0(0{0,0}(),x18) -> 0{1,0}(x18)
        le0(s{0,0}(x21),x22) -> s{1,0}(x21,x22)
        0{1,0}(y) -> true{0,0}()
        s{1,0}(x,0{0,0}()) -> false{0,0}()
        s{1,0}(x,s{0,0}(y)) -> le0(x,y)
       Matrix Interpretation Processor: dim=3
        
        usable rules:
         le0(0{0,0}(),x18) -> 0{1,0}(x18)
         le0(s{0,0}(x21),x22) -> s{1,0}(x21,x22)
         0{1,0}(y) -> true{0,0}()
         s{1,0}(x,0{0,0}()) -> false{0,0}()
         s{1,0}(x,s{0,0}(y)) -> le0(x,y)
        interpretation:
         [if_gcd{0,0,#}](x0, x1, x2) = [0 0 1]x1 + [0 0 1]x2,
         
         [minus0_gcd{0,#}_1#](x0, x1, x2) = [0 0 1]x0 + [0 0 1]x2,
         
                                [0 0 0]     [0 0 0]     [0]
         [minus{0,0}](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
                                [1 1 1]     [0 1 0]     [1],
         
                        [1]
         [false{0,0}] = [0]
                        [0],
         
                            [0 0 0]     [1 0 0]     [0]
         [s{1,0}](x0, x1) = [1 1 0]x0 + [0 0 0]x1 + [1]
                            [0 0 0]     [0 0 0]     [0],
         
         [s0_gcd{0,#}_1#](x0, x1) = [1 0 1]x0 + [0 0 1]x1,
         
                        [1 1 1]     [1]
         [s{0,0}](x0) = [0 0 0]x0 + [1]
                        [1 0 1]     [0],
         
                       [0]
         [true{0,0}] = [0]
                       [0],
         
                        [1 0 0]  
         [0{1,0}](x0) = [0 0 0]x0
                        [0 0 0]  ,
         
                    [1]
         [0{0,0}] = [1]
                    [0],
         
                         [0 0 0]     [1 0 0]  
         [le0](x0, x1) = [1 1 0]x0 + [0 0 0]x1
                         [0 0 0]     [0 0 0]  ,
         
         [gcd{0,#}](x0, x1) = [0 0 1]x0 + [0 0 1]x1
        orientation:
         gcd{0,#}(minus{0,0}(x47,x48),x49) = [1 1 1]x47 + [0 1 0]x48 + [0 0 1]x49 + [1] >= [0 0 1]x47 + [0 0 1]x49 = minus0_gcd{0,#}_1#(x47,x48,x49)
         
         gcd{0,#}(s{0,0}(x45),x46) = [1 0 1]x45 + [0 0 1]x46 >= [1 0 1]x45 + [0 0 1]x46 = s0_gcd{0,#}_1#(x45,x46)
         
         minus0_gcd{0,#}_1#(x,0{0,0}(),x50) = [0 0 1]x + [0 0 1]x50 >= [0 0 1]x + [0 0 1]x50 = gcd{0,#}(x,x50)
         
         minus0_gcd{0,#}_1#(0{0,0}(),x,x51) = [0 0 1]x51 >= [0 0 1]x51 = gcd{0,#}(0{0,0}(),x51)
         
         minus0_gcd{0,#}_1#(s{0,0}(x),s{0,0}(y),x52) = [1 0 1]x + [0 0 1]x52 >= [0 0 1]x + [0 0 1]x52 = minus0_gcd{0,#}_1#(x,y,x52)
         
         if_gcd{0,0,#}(false{0,0}(),x,y) = [0 0 1]x + [0 0 1]y >= [0 0 1]x + [0 0 1]y = minus0_gcd{0,#}_1#(y,x,x)
         
         s0_gcd{0,#}_1#(x,s{0,0}(y)) = [1 0 1]x + [1 0 1]y >= [1 0 1]x + [1 0 1]y = if_gcd{0,0,#}(le0(y,x),s{0,0}(x),s{0,0}(y))
         
         if_gcd{0,0,#}(true{0,0}(),x,y) = [0 0 1]x + [0 0 1]y >= [0 0 1]x + [0 0 1]y = minus0_gcd{0,#}_1#(x,y,y)
         
                             [1 0 0]      [0]    [1 0 0]                 
         le0(0{0,0}(),x18) = [0 0 0]x18 + [2] >= [0 0 0]x18 = 0{1,0}(x18)
                             [0 0 0]      [0]    [0 0 0]                 
         
                                [0 0 0]      [1 0 0]      [0]    [0 0 0]      [1 0 0]      [0]                  
         le0(s{0,0}(x21),x22) = [1 1 1]x21 + [0 0 0]x22 + [2] >= [1 1 0]x21 + [0 0 0]x22 + [1] = s{1,0}(x21,x22)
                                [0 0 0]      [0 0 0]      [0]    [0 0 0]      [0 0 0]      [0]                  
         
                     [1 0 0]     [0]              
         0{1,0}(y) = [0 0 0]y >= [0] = true{0,0}()
                     [0 0 0]     [0]              
         
                              [0 0 0]    [1]    [1]               
         s{1,0}(x,0{0,0}()) = [1 1 0]x + [1] >= [0] = false{0,0}()
                              [0 0 0]    [0]    [0]               
         
                               [0 0 0]    [1 1 1]    [1]    [0 0 0]    [1 0 0]            
         s{1,0}(x,s{0,0}(y)) = [1 1 0]x + [0 0 0]y + [1] >= [1 1 0]x + [0 0 0]y = le0(x,y)
                               [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]            
        problem:
         DPs:
          gcd{0,#}(s{0,0}(x45),x46) -> s0_gcd{0,#}_1#(x45,x46)
          minus0_gcd{0,#}_1#(x,0{0,0}(),x50) -> gcd{0,#}(x,x50)
          minus0_gcd{0,#}_1#(0{0,0}(),x,x51) -> gcd{0,#}(0{0,0}(),x51)
          minus0_gcd{0,#}_1#(s{0,0}(x),s{0,0}(y),x52) -> minus0_gcd{0,#}_1#(x,y,x52)
          if_gcd{0,0,#}(false{0,0}(),x,y) -> minus0_gcd{0,#}_1#(y,x,x)
          s0_gcd{0,#}_1#(x,s{0,0}(y)) -> if_gcd{0,0,#}(le0(y,x),s{0,0}(x),s{0,0}(y))
          if_gcd{0,0,#}(true{0,0}(),x,y) -> minus0_gcd{0,#}_1#(x,y,y)
         TRS:
          le0(0{0,0}(),x18) -> 0{1,0}(x18)
          le0(s{0,0}(x21),x22) -> s{1,0}(x21,x22)
          0{1,0}(y) -> true{0,0}()
          s{1,0}(x,0{0,0}()) -> false{0,0}()
          s{1,0}(x,s{0,0}(y)) -> le0(x,y)
        Restore Modifier:
         DPs:
          gcd{0,#}(s{0,0}(x45),x46) -> s0_gcd{0,#}_1#(x45,x46)
          minus0_gcd{0,#}_1#(x,0{0,0}(),x50) -> gcd{0,#}(x,x50)
          minus0_gcd{0,#}_1#(0{0,0}(),x,x51) -> gcd{0,#}(0{0,0}(),x51)
          minus0_gcd{0,#}_1#(s{0,0}(x),s{0,0}(y),x52) -> minus0_gcd{0,#}_1#(x,y,x52)
          if_gcd{0,0,#}(false{0,0}(),x,y) -> minus0_gcd{0,#}_1#(y,x,x)
          s0_gcd{0,#}_1#(x,s{0,0}(y)) -> if_gcd{0,0,#}(le0(y,x),s{0,0}(x),s{0,0}(y))
          if_gcd{0,0,#}(true{0,0}(),x,y) -> minus0_gcd{0,#}_1#(x,y,y)
         TRS:
          0{1,0}(y) -> true{0,0}()
          s{1,0}(x,0{0,0}()) -> false{0,0}()
          s{1,0}(x,s{0,0}(y)) -> le0(x,y)
          minus{0,0}(x,0{0,0}()) -> x
          minus{0,0}(0{0,0}(),x) -> 0{0,0}()
          minus{0,0}(s{0,0}(x),s{0,0}(y)) -> minus{0,0}(x,y)
          gcd{0,0}(0{0,0}(),y) -> y
          gcd{0,0}(s{0,0}(x),0{0,0}()) -> s{0,0}(x)
          gcd{0,0}(s{0,0}(x),s{0,0}(y)) -> if_gcd{0,0}(le0(y,x),s{0,0}(x),s{0,0}(y))
          if_gcd{0,0}(true{0,0}(),x,y) -> gcd{0,0}(minus{0,0}(x,y),y)
          if_gcd{0,0}(false{0,0}(),x,y) -> gcd{0,0}(minus{0,0}(y,x),x)
          le0(0{0,0}(),x18) -> 0{1,0}(x18)
          le0(s{0,0}(x21),x22) -> s{1,0}(x21,x22)
         Usable Rule Processor:
          DPs:
           gcd{0,#}(s{0,0}(x45),x46) -> s0_gcd{0,#}_1#(x45,x46)
           minus0_gcd{0,#}_1#(x,0{0,0}(),x50) -> gcd{0,#}(x,x50)
           minus0_gcd{0,#}_1#(0{0,0}(),x,x51) -> gcd{0,#}(0{0,0}(),x51)
           minus0_gcd{0,#}_1#(s{0,0}(x),s{0,0}(y),x52) -> minus0_gcd{0,#}_1#(x,y,x52)
           if_gcd{0,0,#}(false{0,0}(),x,y) -> minus0_gcd{0,#}_1#(y,x,x)
           s0_gcd{0,#}_1#(x,s{0,0}(y)) -> if_gcd{0,0,#}(le0(y,x),s{0,0}(x),s{0,0}(y))
           if_gcd{0,0,#}(true{0,0}(),x,y) -> minus0_gcd{0,#}_1#(x,y,y)
          TRS:
           le0(0{0,0}(),x18) -> 0{1,0}(x18)
           le0(s{0,0}(x21),x22) -> s{1,0}(x21,x22)
           0{1,0}(y) -> true{0,0}()
           s{1,0}(x,0{0,0}()) -> false{0,0}()
           s{1,0}(x,s{0,0}(y)) -> le0(x,y)
          Matrix Interpretation Processor: dim=3
           
           usable rules:
            
           interpretation:
            [if_gcd{0,0,#}](x0, x1, x2) = [1 0 0]x1 + [1 0 0]x2,
            
            [minus0_gcd{0,#}_1#](x0, x1, x2) = [1 0 0]x0 + [1 0 0]x2,
            
                           [0]
            [false{0,0}] = [0]
                           [0],
            
                               [0]
            [s{1,0}](x0, x1) = [0]
                               [0],
            
            [s0_gcd{0,#}_1#](x0, x1) = [1 0 0]x0 + [1 0 0]x1 + [1],
            
                           [1 0 0]     [1]
            [s{0,0}](x0) = [0 0 0]x0 + [0]
                           [0 0 0]     [0],
            
                          [0]
            [true{0,0}] = [0]
                          [0],
            
                           [0]
            [0{1,0}](x0) = [0]
                           [0],
            
                       [0]
            [0{0,0}] = [0]
                       [0],
            
                            [0]
            [le0](x0, x1) = [0]
                            [0],
            
            [gcd{0,#}](x0, x1) = [1 0 0]x0 + [1 0 0]x1
           orientation:
            gcd{0,#}(s{0,0}(x45),x46) = [1 0 0]x45 + [1 0 0]x46 + [1] >= [1 0 0]x45 + [1 0 0]x46 + [1] = s0_gcd{0,#}_1#(x45,x46)
            
            minus0_gcd{0,#}_1#(x,0{0,0}(),x50) = [1 0 0]x + [1 0 0]x50 >= [1 0 0]x + [1 0 0]x50 = gcd{0,#}(x,x50)
            
            minus0_gcd{0,#}_1#(0{0,0}(),x,x51) = [1 0 0]x51 >= [1 0 0]x51 = gcd{0,#}(0{0,0}(),x51)
            
            minus0_gcd{0,#}_1#(s{0,0}(x),s{0,0}(y),x52) = [1 0 0]x + [1 0 0]x52 + [1] >= [1 0 0]x + [1 0 0]x52 = minus0_gcd{0,#}_1#(x,y,x52)
            
            if_gcd{0,0,#}(false{0,0}(),x,y) = [1 0 0]x + [1 0 0]y >= [1 0 0]x + [1 0 0]y = minus0_gcd{0,#}_1#(y,x,x)
            
            s0_gcd{0,#}_1#(x,s{0,0}(y)) = [1 0 0]x + [1 0 0]y + [2] >= [1 0 0]x + [1 0 0]y + [2] = if_gcd{0,0,#}(le0(y,x),s{0,0}(x),s{0,0}(y))
            
            if_gcd{0,0,#}(true{0,0}(),x,y) = [1 0 0]x + [1 0 0]y >= [1 0 0]x + [1 0 0]y = minus0_gcd{0,#}_1#(x,y,y)
            
                                [0]    [0]              
            le0(0{0,0}(),x18) = [0] >= [0] = 0{1,0}(x18)
                                [0]    [0]              
            
                                   [0]    [0]                  
            le0(s{0,0}(x21),x22) = [0] >= [0] = s{1,0}(x21,x22)
                                   [0]    [0]                  
            
                        [0]    [0]              
            0{1,0}(y) = [0] >= [0] = true{0,0}()
                        [0]    [0]              
            
                                 [0]    [0]               
            s{1,0}(x,0{0,0}()) = [0] >= [0] = false{0,0}()
                                 [0]    [0]               
            
                                  [0]    [0]           
            s{1,0}(x,s{0,0}(y)) = [0] >= [0] = le0(x,y)
                                  [0]    [0]           
           problem:
            DPs:
             gcd{0,#}(s{0,0}(x45),x46) -> s0_gcd{0,#}_1#(x45,x46)
             minus0_gcd{0,#}_1#(x,0{0,0}(),x50) -> gcd{0,#}(x,x50)
             minus0_gcd{0,#}_1#(0{0,0}(),x,x51) -> gcd{0,#}(0{0,0}(),x51)
             if_gcd{0,0,#}(false{0,0}(),x,y) -> minus0_gcd{0,#}_1#(y,x,x)
             s0_gcd{0,#}_1#(x,s{0,0}(y)) -> if_gcd{0,0,#}(le0(y,x),s{0,0}(x),s{0,0}(y))
             if_gcd{0,0,#}(true{0,0}(),x,y) -> minus0_gcd{0,#}_1#(x,y,y)
            TRS:
             le0(0{0,0}(),x18) -> 0{1,0}(x18)
             le0(s{0,0}(x21),x22) -> s{1,0}(x21,x22)
             0{1,0}(y) -> true{0,0}()
             s{1,0}(x,0{0,0}()) -> false{0,0}()
             s{1,0}(x,s{0,0}(y)) -> le0(x,y)
           Restore Modifier:
            DPs:
             gcd{0,#}(s{0,0}(x45),x46) -> s0_gcd{0,#}_1#(x45,x46)
             minus0_gcd{0,#}_1#(x,0{0,0}(),x50) -> gcd{0,#}(x,x50)
             minus0_gcd{0,#}_1#(0{0,0}(),x,x51) -> gcd{0,#}(0{0,0}(),x51)
             if_gcd{0,0,#}(false{0,0}(),x,y) -> minus0_gcd{0,#}_1#(y,x,x)
             s0_gcd{0,#}_1#(x,s{0,0}(y)) -> if_gcd{0,0,#}(le0(y,x),s{0,0}(x),s{0,0}(y))
             if_gcd{0,0,#}(true{0,0}(),x,y) -> minus0_gcd{0,#}_1#(x,y,y)
            TRS:
             0{1,0}(y) -> true{0,0}()
             s{1,0}(x,0{0,0}()) -> false{0,0}()
             s{1,0}(x,s{0,0}(y)) -> le0(x,y)
             minus{0,0}(x,0{0,0}()) -> x
             minus{0,0}(0{0,0}(),x) -> 0{0,0}()
             minus{0,0}(s{0,0}(x),s{0,0}(y)) -> minus{0,0}(x,y)
             gcd{0,0}(0{0,0}(),y) -> y
             gcd{0,0}(s{0,0}(x),0{0,0}()) -> s{0,0}(x)
             gcd{0,0}(s{0,0}(x),s{0,0}(y)) -> if_gcd{0,0}(le0(y,x),s{0,0}(x),s{0,0}(y))
             if_gcd{0,0}(true{0,0}(),x,y) -> gcd{0,0}(minus{0,0}(x,y),y)
             if_gcd{0,0}(false{0,0}(),x,y) -> gcd{0,0}(minus{0,0}(y,x),x)
             le0(0{0,0}(),x18) -> 0{1,0}(x18)
             le0(s{0,0}(x21),x22) -> s{1,0}(x21,x22)
            Usable Rule Processor:
             DPs:
              gcd{0,#}(s{0,0}(x45),x46) -> s0_gcd{0,#}_1#(x45,x46)
              minus0_gcd{0,#}_1#(x,0{0,0}(),x50) -> gcd{0,#}(x,x50)
              minus0_gcd{0,#}_1#(0{0,0}(),x,x51) -> gcd{0,#}(0{0,0}(),x51)
              if_gcd{0,0,#}(false{0,0}(),x,y) -> minus0_gcd{0,#}_1#(y,x,x)
              s0_gcd{0,#}_1#(x,s{0,0}(y)) -> if_gcd{0,0,#}(le0(y,x),s{0,0}(x),s{0,0}(y))
              if_gcd{0,0,#}(true{0,0}(),x,y) -> minus0_gcd{0,#}_1#(x,y,y)
             TRS:
              le0(0{0,0}(),x18) -> 0{1,0}(x18)
              le0(s{0,0}(x21),x22) -> s{1,0}(x21,x22)
              0{1,0}(y) -> true{0,0}()
              s{1,0}(x,0{0,0}()) -> false{0,0}()
              s{1,0}(x,s{0,0}(y)) -> le0(x,y)
             Arctic Interpretation Processor:
              dimension: 1
              usable rules:
               
              interpretation:
               [if_gcd{0,0,#}](x0, x1, x2) = x1 + x2 + 0,
               
               [minus0_gcd{0,#}_1#](x0, x1, x2) = x0 + x1 + x2,
               
               [false{0,0}] = 4,
               
               [s{1,0}](x0, x1) = 1x0 + 0,
               
               [s0_gcd{0,#}_1#](x0, x1) = x1 + 1,
               
               [s{0,0}](x0) = 0,
               
               [true{0,0}] = 0,
               
               [0{1,0}](x0) = x0 + 0,
               
               [0{0,0}] = 2,
               
               [le0](x0, x1) = x1 + 0,
               
               [gcd{0,#}](x0, x1) = x0 + x1 + 1
              orientation:
               gcd{0,#}(s{0,0}(x45),x46) = x46 + 1 >= x46 + 1 = s0_gcd{0,#}_1#(x45,x46)
               
               minus0_gcd{0,#}_1#(x,0{0,0}(),x50) = x + x50 + 2 >= x + x50 + 1 = gcd{0,#}(x,x50)
               
               minus0_gcd{0,#}_1#(0{0,0}(),x,x51) = x + x51 + 2 >= x51 + 2 = gcd{0,#}(0{0,0}(),x51)
               
               if_gcd{0,0,#}(false{0,0}(),x,y) = x + y + 0 >= x + y = minus0_gcd{0,#}_1#(y,x,x)
               
               s0_gcd{0,#}_1#(x,s{0,0}(y)) = 1 >= 0 = if_gcd{0,0,#}(le0(y,x),s{0,0}(x),s{0,0}(y))
               
               if_gcd{0,0,#}(true{0,0}(),x,y) = x + y + 0 >= x + y = minus0_gcd{0,#}_1#(x,y,y)
               
               le0(0{0,0}(),x18) = x18 + 0 >= x18 + 0 = 0{1,0}(x18)
               
               le0(s{0,0}(x21),x22) = x22 + 0 >= 1x21 + 0 = s{1,0}(x21,x22)
               
               0{1,0}(y) = y + 0 >= 0 = true{0,0}()
               
               s{1,0}(x,0{0,0}()) = 1x + 0 >= 4 = false{0,0}()
               
               s{1,0}(x,s{0,0}(y)) = 1x + 0 >= y + 0 = le0(x,y)
              problem:
               DPs:
                gcd{0,#}(s{0,0}(x45),x46) -> s0_gcd{0,#}_1#(x45,x46)
                minus0_gcd{0,#}_1#(x,0{0,0}(),x50) -> gcd{0,#}(x,x50)
                minus0_gcd{0,#}_1#(0{0,0}(),x,x51) -> gcd{0,#}(0{0,0}(),x51)
                if_gcd{0,0,#}(false{0,0}(),x,y) -> minus0_gcd{0,#}_1#(y,x,x)
                if_gcd{0,0,#}(true{0,0}(),x,y) -> minus0_gcd{0,#}_1#(x,y,y)
               TRS:
                le0(0{0,0}(),x18) -> 0{1,0}(x18)
                le0(s{0,0}(x21),x22) -> s{1,0}(x21,x22)
                0{1,0}(y) -> true{0,0}()
                s{1,0}(x,0{0,0}()) -> false{0,0}()
                s{1,0}(x,s{0,0}(y)) -> le0(x,y)
              Restore Modifier:
               DPs:
                gcd{0,#}(s{0,0}(x45),x46) -> s0_gcd{0,#}_1#(x45,x46)
                minus0_gcd{0,#}_1#(x,0{0,0}(),x50) -> gcd{0,#}(x,x50)
                minus0_gcd{0,#}_1#(0{0,0}(),x,x51) -> gcd{0,#}(0{0,0}(),x51)
                if_gcd{0,0,#}(false{0,0}(),x,y) -> minus0_gcd{0,#}_1#(y,x,x)
                if_gcd{0,0,#}(true{0,0}(),x,y) -> minus0_gcd{0,#}_1#(x,y,y)
               TRS:
                0{1,0}(y) -> true{0,0}()
                s{1,0}(x,0{0,0}()) -> false{0,0}()
                s{1,0}(x,s{0,0}(y)) -> le0(x,y)
                minus{0,0}(x,0{0,0}()) -> x
                minus{0,0}(0{0,0}(),x) -> 0{0,0}()
                minus{0,0}(s{0,0}(x),s{0,0}(y)) -> minus{0,0}(x,y)
                gcd{0,0}(0{0,0}(),y) -> y
                gcd{0,0}(s{0,0}(x),0{0,0}()) -> s{0,0}(x)
                gcd{0,0}(s{0,0}(x),s{0,0}(y)) -> if_gcd{0,0}(le0(y,x),s{0,0}(x),s{0,0}(y))
                if_gcd{0,0}(true{0,0}(),x,y) -> gcd{0,0}(minus{0,0}(x,y),y)
                if_gcd{0,0}(false{0,0}(),x,y) -> gcd{0,0}(minus{0,0}(y,x),x)
                le0(0{0,0}(),x18) -> 0{1,0}(x18)
                le0(s{0,0}(x21),x22) -> s{1,0}(x21,x22)
               Bounds Processor:
                bound: 3
                enrichment: top-dp
                automaton:
                 final states: {8,7,6}
                 transitions:
                  gcd{0,#,2}(5,5) -> 8*
                  0{0,0,2}() -> 5*
                  s0_gcd{0,#}_1{#,2}(5,5) -> 7*
                  s0_gcd{0,#}_1{#,3}(5,5) -> 8*
                  gcd{0,#,0}(5,5) -> 6*
                  s{0,0,0}(5) -> 5*
                  s0_gcd{0,#}_1{#,0}(5,5) -> 5*
                  minus0_gcd{0,#}_1{#,0}(5,5,5) -> 7*
                  0{0,0,0}() -> 5*
                  if_gcd{0,0,#,0}(5,5,5) -> 8*
                  false{0,0,0}() -> 5*
                  true{0,0,0}() -> 5*
                  0{1,0,0}(5) -> 5*
                  s{1,0,0}(5,5) -> 5*
                  le{0,0}(5,5) -> 5*
                  minus{0,0,0}(5,5) -> 5*
                  gcd{0,0,0}(5,5) -> 5*
                  if_gcd{0,0,0}(5,5,5) -> 5*
                  minus0_gcd{0,#}_1{#,1}(5,5,5) -> 8*
                  gcd{0,#,1}(5,5) -> 7*
                  0{0,0,1}() -> 5*
                  s0_gcd{0,#}_1{#,1}(5,5) -> 6*
                problem:
                 DPs:
                  
                 TRS:
                  0{1,0}(y) -> true{0,0}()
                  s{1,0}(x,0{0,0}()) -> false{0,0}()
                  s{1,0}(x,s{0,0}(y)) -> le0(x,y)
                  minus{0,0}(x,0{0,0}()) -> x
                  minus{0,0}(0{0,0}(),x) -> 0{0,0}()
                  minus{0,0}(s{0,0}(x),s{0,0}(y)) -> minus{0,0}(x,y)
                  gcd{0,0}(0{0,0}(),y) -> y
                  gcd{0,0}(s{0,0}(x),0{0,0}()) -> s{0,0}(x)
                  gcd{0,0}(s{0,0}(x),s{0,0}(y)) -> if_gcd{0,0}(le0(y,x),s{0,0}(x),s{0,0}(y))
                  if_gcd{0,0}(true{0,0}(),x,y) -> gcd{0,0}(minus{0,0}(x,y),y)
                  if_gcd{0,0}(false{0,0}(),x,y) -> gcd{0,0}(minus{0,0}(y,x),x)
                  le0(0{0,0}(),x18) -> 0{1,0}(x18)
                  le0(s{0,0}(x21),x22) -> s{1,0}(x21,x22)
                Qed
    
    DPs:
     minus#(s(x),s(y)) -> minus#(x,y)
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     minus(x,0()) -> x
     minus(0(),x) -> 0()
     minus(s(x),s(y)) -> minus(x,y)
     gcd(0(),y) -> y
     gcd(s(x),0()) -> s(x)
     gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
     if_gcd(true(),x,y) -> gcd(minus(x,y),y)
     if_gcd(false(),x,y) -> gcd(minus(y,x),x)
    Subterm Criterion Processor:
     simple projection:
      pi(minus#) = 1
     problem:
      DPs:
       
      TRS:
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       minus(x,0()) -> x
       minus(0(),x) -> 0()
       minus(s(x),s(y)) -> minus(x,y)
       gcd(0(),y) -> y
       gcd(s(x),0()) -> s(x)
       gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
       if_gcd(true(),x,y) -> gcd(minus(x,y),y)
       if_gcd(false(),x,y) -> gcd(minus(y,x),x)
     Qed
    
    DPs:
     le#(s(x),s(y)) -> le#(x,y)
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     minus(x,0()) -> x
     minus(0(),x) -> 0()
     minus(s(x),s(y)) -> minus(x,y)
     gcd(0(),y) -> y
     gcd(s(x),0()) -> s(x)
     gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
     if_gcd(true(),x,y) -> gcd(minus(x,y),y)
     if_gcd(false(),x,y) -> gcd(minus(y,x),x)
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 1
     problem:
      DPs:
       
      TRS:
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       minus(x,0()) -> x
       minus(0(),x) -> 0()
       minus(s(x),s(y)) -> minus(x,y)
       gcd(0(),y) -> y
       gcd(s(x),0()) -> s(x)
       gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
       if_gcd(true(),x,y) -> gcd(minus(x,y),y)
       if_gcd(false(),x,y) -> gcd(minus(y,x),x)
     Qed