YES
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:
  Strict:
   {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())}
  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}
  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))}
   SCCS:
    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:
     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:
      Argument Filtering:
       pi(if) = [], pi(div#) = 0, pi(div) = [], pi(false) = [], pi(geq) = [], pi(true) = [], pi(s) = [], pi(minus) = [], pi(0) = []
      Usable Rules:
       {}
      Interpretation:
       [minus] = 0,
       [s] = 1
      Strict:
       {}
      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}
      Qed
    SCC:
     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}
     SPSC:
      Simple Projection:
       pi(geq#) = 1
      Strict:
       {}
      Qed
    SCC:
     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}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {}
      Qed