YES
Time: 0.082380
TRS:
 {    minus(0(), Y) -> 0(),
    minus(s X, s Y) -> minus(X, Y),
        geq(X, 0()) -> true(),
      geq(0(), s Y) -> false(),
      geq(s X, s Y) -> geq(X, Y),
      div(0(), s Y) -> 0(),
      div(s X, s Y) -> if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
   if(true(), X, Y) -> X,
  if(false(), X, Y) -> Y}
 DP:
  DP:
   {minus#(s X, s Y) -> minus#(X, Y),
      geq#(s X, s Y) -> geq#(X, Y),
      div#(s X, s Y) -> minus#(X, Y),
      div#(s X, s Y) -> geq#(X, Y),
      div#(s X, s Y) -> div#(minus(X, Y), s Y),
      div#(s X, s Y) -> if#(geq(X, Y), s div(minus(X, Y), s Y), 0())}
  TRS:
  {    minus(0(), Y) -> 0(),
     minus(s X, s Y) -> minus(X, Y),
         geq(X, 0()) -> true(),
       geq(0(), s Y) -> false(),
       geq(s X, s Y) -> geq(X, Y),
       div(0(), s Y) -> 0(),
       div(s X, s Y) -> if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
    if(true(), X, Y) -> X,
   if(false(), X, Y) -> Y}
  UR:
   {    minus(0(), Y) -> 0(),
      minus(s X, s Y) -> minus(X, Y),
          geq(X, 0()) -> true(),
        geq(0(), s Y) -> false(),
        geq(s X, s Y) -> geq(X, Y),
        div(0(), s Y) -> 0(),
        div(s X, s Y) -> if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
     if(true(), X, Y) -> X,
    if(false(), X, Y) -> Y,
              a(x, y) -> x,
              a(x, y) -> y}
   EDG:
    {(minus#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> minus#(X, Y))
     (div#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> minus#(X, Y))
     (div#(s X, s Y) -> div#(minus(X, Y), s Y), div#(s X, s Y) -> if#(geq(X, Y), s div(minus(X, Y), s Y), 0()))
     (div#(s X, s Y) -> div#(minus(X, Y), s Y), div#(s X, s Y) -> div#(minus(X, Y), s Y))
     (div#(s X, s Y) -> div#(minus(X, Y), s Y), div#(s X, s Y) -> geq#(X, Y))
     (div#(s X, s Y) -> div#(minus(X, Y), s Y), div#(s X, s Y) -> minus#(X, Y))
     (div#(s X, s Y) -> geq#(X, Y), geq#(s X, s Y) -> geq#(X, Y))
     (geq#(s X, s Y) -> geq#(X, Y), geq#(s X, s Y) -> geq#(X, Y))}
    STATUS:
     arrows: 0.777778
     SCCS (3):
      Scc:
       {div#(s X, s Y) -> div#(minus(X, Y), s Y)}
      Scc:
       {geq#(s X, s Y) -> geq#(X, Y)}
      Scc:
       {minus#(s X, s Y) -> minus#(X, Y)}
      
      SCC (1):
       Strict:
        {div#(s X, s Y) -> div#(minus(X, Y), s Y)}
       Weak:
       {    minus(0(), Y) -> 0(),
          minus(s X, s Y) -> minus(X, Y),
              geq(X, 0()) -> true(),
            geq(0(), s Y) -> false(),
            geq(s X, s Y) -> geq(X, Y),
            div(0(), s Y) -> 0(),
            div(s X, s Y) -> if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
         if(true(), X, Y) -> X,
        if(false(), X, Y) -> Y}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [if](x0, x1, x2) = x0 + x1 + 1,
         
         [minus](x0, x1) = 0,
         
         [geq](x0, x1) = 0,
         
         [div](x0, x1) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [0] = 0,
         
         [true] = 1,
         
         [false] = 0,
         
         [div#](x0, x1) = x0 + 1
        Strict:
         div#(s X, s Y) -> div#(minus(X, Y), s Y)
         2 + 0Y + 1X >= 1 + 0Y + 0X
        Weak:
         if(false(), X, Y) -> Y
         1 + 0Y + 1X >= 1Y
         if(true(), X, Y) -> X
         2 + 0Y + 1X >= 1X
         div(s X, s Y) -> if(geq(X, Y), s div(minus(X, Y), s Y), 0())
         2 + 1Y + 0X >= 4 + 1Y + 0X
         div(0(), s Y) -> 0()
         2 + 1Y >= 0
         geq(s X, s Y) -> geq(X, Y)
         0 + 0Y + 0X >= 0 + 0Y + 0X
         geq(0(), s Y) -> false()
         0 + 0Y >= 0
         geq(X, 0()) -> true()
         0 + 0X >= 1
         minus(s X, s Y) -> minus(X, Y)
         0 + 0Y + 0X >= 0 + 0Y + 0X
         minus(0(), Y) -> 0()
         0 + 0Y >= 0
       Qed
     
     
     SCC (1):
      Strict:
       {geq#(s X, s Y) -> geq#(X, Y)}
      Weak:
      {    minus(0(), Y) -> 0(),
         minus(s X, s Y) -> minus(X, Y),
             geq(X, 0()) -> true(),
           geq(0(), s Y) -> false(),
           geq(s X, s Y) -> geq(X, Y),
           div(0(), s Y) -> 0(),
           div(s X, s Y) -> if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
        if(true(), X, Y) -> X,
       if(false(), X, Y) -> Y}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [if](x0, x1, x2) = x0 + x1 + 1,
        
        [minus](x0, x1) = x0 + 1,
        
        [geq](x0, x1) = x0 + 1,
        
        [div](x0, x1) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [0] = 1,
        
        [true] = 1,
        
        [false] = 0,
        
        [geq#](x0, x1) = x0 + 1
       Strict:
        geq#(s X, s Y) -> geq#(X, Y)
        2 + 0Y + 1X >= 1 + 0Y + 1X
       Weak:
        if(false(), X, Y) -> Y
        1 + 0Y + 1X >= 1Y
        if(true(), X, Y) -> X
        2 + 0Y + 1X >= 1X
        div(s X, s Y) -> if(geq(X, Y), s div(minus(X, Y), s Y), 0())
        2 + 1Y + 0X >= 5 + 2Y + 0X
        div(0(), s Y) -> 0()
        2 + 1Y >= 1
        geq(s X, s Y) -> geq(X, Y)
        2 + 1Y + 0X >= 1 + 1Y + 0X
        geq(0(), s Y) -> false()
        2 + 1Y >= 0
        geq(X, 0()) -> true()
        2 + 0X >= 1
        minus(s X, s Y) -> minus(X, Y)
        2 + 0Y + 1X >= 1 + 0Y + 1X
        minus(0(), Y) -> 0()
        2 + 0Y >= 1
      Qed
     SCC (1):
      Strict:
       {minus#(s X, s Y) -> minus#(X, Y)}
      Weak:
      {    minus(0(), Y) -> 0(),
         minus(s X, s Y) -> minus(X, Y),
             geq(X, 0()) -> true(),
           geq(0(), s Y) -> false(),
           geq(s X, s Y) -> geq(X, Y),
           div(0(), s Y) -> 0(),
           div(s X, s Y) -> if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
        if(true(), X, Y) -> X,
       if(false(), X, Y) -> Y}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [if](x0, x1, x2) = x0 + x1 + 1,
        
        [minus](x0, x1) = x0 + 1,
        
        [geq](x0, x1) = x0 + 1,
        
        [div](x0, x1) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [0] = 1,
        
        [true] = 1,
        
        [false] = 0,
        
        [minus#](x0, x1) = x0 + 1
       Strict:
        minus#(s X, s Y) -> minus#(X, Y)
        2 + 0Y + 1X >= 1 + 0Y + 1X
       Weak:
        if(false(), X, Y) -> Y
        1 + 0Y + 1X >= 1Y
        if(true(), X, Y) -> X
        2 + 0Y + 1X >= 1X
        div(s X, s Y) -> if(geq(X, Y), s div(minus(X, Y), s Y), 0())
        2 + 1Y + 0X >= 5 + 2Y + 0X
        div(0(), s Y) -> 0()
        2 + 1Y >= 1
        geq(s X, s Y) -> geq(X, Y)
        2 + 1Y + 0X >= 1 + 1Y + 0X
        geq(0(), s Y) -> false()
        2 + 1Y >= 0
        geq(X, 0()) -> true()
        2 + 0X >= 1
        minus(s X, s Y) -> minus(X, Y)
        2 + 0Y + 1X >= 1 + 0Y + 1X
        minus(0(), Y) -> 0()
        2 + 0Y >= 1
      Qed