YES
TRS:
 {                    0() -> n__0(),
         minus(n__0(), Y) -> 0(),
  minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
              activate(X) -> X,
         activate(n__0()) -> 0(),
        activate(n__s(X)) -> s(X),
           geq(X, n__0()) -> true(),
     geq(n__0(), n__s(Y)) -> false(),
    geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
        div(0(), n__s(Y)) -> 0(),
       div(s(X), n__s(Y)) -> if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
         if(true(), X, Y) -> activate(X),
        if(false(), X, Y) -> activate(Y),
                     s(X) -> n__s(X)}
 DP:
  Strict:
   {       minus#(n__0(), Y) -> 0#(),
    minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)),
    minus#(n__s(X), n__s(Y)) -> activate#(Y),
    minus#(n__s(X), n__s(Y)) -> activate#(X),
           activate#(n__0()) -> 0#(),
          activate#(n__s(X)) -> s#(X),
      geq#(n__s(X), n__s(Y)) -> activate#(Y),
      geq#(n__s(X), n__s(Y)) -> activate#(X),
      geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)),
         div#(s(X), n__s(Y)) -> minus#(X, activate(Y)),
         div#(s(X), n__s(Y)) -> activate#(Y),
         div#(s(X), n__s(Y)) -> geq#(X, activate(Y)),
         div#(s(X), n__s(Y)) -> div#(minus(X, activate(Y)), n__s(activate(Y))),
         div#(s(X), n__s(Y)) -> if#(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
           if#(true(), X, Y) -> activate#(X),
          if#(false(), X, Y) -> activate#(Y)}
  Weak:
  {                    0() -> n__0(),
          minus(n__0(), Y) -> 0(),
   minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
               activate(X) -> X,
          activate(n__0()) -> 0(),
         activate(n__s(X)) -> s(X),
            geq(X, n__0()) -> true(),
      geq(n__0(), n__s(Y)) -> false(),
     geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
         div(0(), n__s(Y)) -> 0(),
        div(s(X), n__s(Y)) -> if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
          if(true(), X, Y) -> activate(X),
         if(false(), X, Y) -> activate(Y),
                      s(X) -> n__s(X)}
  EDG:
   {(minus#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (minus#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__0()) -> 0#())
    (geq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (geq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__0()) -> 0#())
    (minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)), minus#(n__s(X), n__s(Y)) -> activate#(X))
    (minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)), minus#(n__s(X), n__s(Y)) -> activate#(Y))
    (minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)), minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)))
    (minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)), minus#(n__0(), Y) -> 0#())
    (div#(s(X), n__s(Y)) -> minus#(X, activate(Y)), minus#(n__s(X), n__s(Y)) -> activate#(X))
    (div#(s(X), n__s(Y)) -> minus#(X, activate(Y)), minus#(n__s(X), n__s(Y)) -> activate#(Y))
    (div#(s(X), n__s(Y)) -> minus#(X, activate(Y)), minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y)))
    (div#(s(X), n__s(Y)) -> minus#(X, activate(Y)), minus#(n__0(), Y) -> 0#())
    (div#(s(X), n__s(Y)) -> if#(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()), if#(false(), X, Y) -> activate#(Y))
    (div#(s(X), n__s(Y)) -> if#(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()), if#(true(), X, Y) -> activate#(X))
    (geq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__s(X)) -> s#(X))
    (geq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__0()) -> 0#())
    (if#(false(), X, Y) -> activate#(Y), activate#(n__s(X)) -> s#(X))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__0()) -> 0#())
    (div#(s(X), n__s(Y)) -> activate#(Y), activate#(n__0()) -> 0#())
    (div#(s(X), n__s(Y)) -> activate#(Y), activate#(n__s(X)) -> s#(X))
    (minus#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__0()) -> 0#())
    (minus#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__s(X)) -> s#(X))
    (div#(s(X), n__s(Y)) -> geq#(X, activate(Y)), geq#(n__s(X), n__s(Y)) -> activate#(Y))
    (div#(s(X), n__s(Y)) -> geq#(X, activate(Y)), geq#(n__s(X), n__s(Y)) -> activate#(X))
    (div#(s(X), n__s(Y)) -> geq#(X, activate(Y)), geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)))
    (geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)), geq#(n__s(X), n__s(Y)) -> activate#(Y))
    (geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)), geq#(n__s(X), n__s(Y)) -> activate#(X))
    (geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)), geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y)))
    (if#(true(), X, Y) -> activate#(X), activate#(n__0()) -> 0#())
    (if#(true(), X, Y) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (div#(s(X), n__s(Y)) -> div#(minus(X, activate(Y)), n__s(activate(Y))), div#(s(X), n__s(Y)) -> minus#(X, activate(Y)))
    (div#(s(X), n__s(Y)) -> div#(minus(X, activate(Y)), n__s(activate(Y))), div#(s(X), n__s(Y)) -> activate#(Y))
    (div#(s(X), n__s(Y)) -> div#(minus(X, activate(Y)), n__s(activate(Y))), div#(s(X), n__s(Y)) -> geq#(X, activate(Y)))
    (div#(s(X), n__s(Y)) -> div#(minus(X, activate(Y)), n__s(activate(Y))), div#(s(X), n__s(Y)) -> div#(minus(X, activate(Y)), n__s(activate(Y))))
    (div#(s(X), n__s(Y)) -> div#(minus(X, activate(Y)), n__s(activate(Y))), div#(s(X), n__s(Y)) -> if#(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()))}
   SCCS:
    Scc:
     {div#(s(X), n__s(Y)) -> div#(minus(X, activate(Y)), n__s(activate(Y)))}
    Scc:
     {geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y))}
    Scc:
     {minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y))}
    SCC:
     Strict:
      {div#(s(X), n__s(Y)) -> div#(minus(X, activate(Y)), n__s(activate(Y)))}
     Weak:
     {                    0() -> n__0(),
             minus(n__0(), Y) -> 0(),
      minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
                  activate(X) -> X,
             activate(n__0()) -> 0(),
            activate(n__s(X)) -> s(X),
               geq(X, n__0()) -> true(),
         geq(n__0(), n__s(Y)) -> false(),
        geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
            div(0(), n__s(Y)) -> 0(),
           div(s(X), n__s(Y)) -> if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
             if(true(), X, Y) -> activate(X),
            if(false(), X, Y) -> activate(Y),
                         s(X) -> n__s(X)}
     POLY:
      Argument Filtering:
       pi(s) = [], pi(if) = [], pi(div#) = [0], pi(div) = [], pi(false) = [], pi(geq) = [], pi(true) = [], pi(n__s) = [], pi(activate) = [], pi(n__0) = [], pi(minus) = [], pi(0) = []
      Usable Rules:
       {}
      Interpretation:
       [div#](x0) = x0 + 1,
       [minus] = 0,
       [s] = 1
      Strict:
       {}
      Weak:
       {                    0() -> n__0(),
               minus(n__0(), Y) -> 0(),
        minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
                    activate(X) -> X,
               activate(n__0()) -> 0(),
              activate(n__s(X)) -> s(X),
                 geq(X, n__0()) -> true(),
           geq(n__0(), n__s(Y)) -> false(),
          geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
              div(0(), n__s(Y)) -> 0(),
             div(s(X), n__s(Y)) -> if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
               if(true(), X, Y) -> activate(X),
              if(false(), X, Y) -> activate(Y),
                           s(X) -> n__s(X)}
      Qed
    SCC:
     Strict:
      {geq#(n__s(X), n__s(Y)) -> geq#(activate(X), activate(Y))}
     Weak:
     {                    0() -> n__0(),
             minus(n__0(), Y) -> 0(),
      minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
                  activate(X) -> X,
             activate(n__0()) -> 0(),
            activate(n__s(X)) -> s(X),
               geq(X, n__0()) -> true(),
         geq(n__0(), n__s(Y)) -> false(),
        geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
            div(0(), n__s(Y)) -> 0(),
           div(s(X), n__s(Y)) -> if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
             if(true(), X, Y) -> activate(X),
            if(false(), X, Y) -> activate(Y),
                         s(X) -> n__s(X)}
     POLY:
      Argument Filtering:
       pi(s) = [0], pi(if) = [], pi(div) = [], pi(false) = [], pi(geq#) = 1, pi(geq) = [], pi(true) = [], pi(n__s) = [0], pi(activate) = 0, pi(n__0) = [], pi(minus) = [], pi(0) = []
      Usable Rules:
       {}
      Interpretation:
       [n__s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {                    0() -> n__0(),
               minus(n__0(), Y) -> 0(),
        minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
                    activate(X) -> X,
               activate(n__0()) -> 0(),
              activate(n__s(X)) -> s(X),
                 geq(X, n__0()) -> true(),
           geq(n__0(), n__s(Y)) -> false(),
          geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
              div(0(), n__s(Y)) -> 0(),
             div(s(X), n__s(Y)) -> if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
               if(true(), X, Y) -> activate(X),
              if(false(), X, Y) -> activate(Y),
                           s(X) -> n__s(X)}
      Qed
    SCC:
     Strict:
      {minus#(n__s(X), n__s(Y)) -> minus#(activate(X), activate(Y))}
     Weak:
     {                    0() -> n__0(),
             minus(n__0(), Y) -> 0(),
      minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
                  activate(X) -> X,
             activate(n__0()) -> 0(),
            activate(n__s(X)) -> s(X),
               geq(X, n__0()) -> true(),
         geq(n__0(), n__s(Y)) -> false(),
        geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
            div(0(), n__s(Y)) -> 0(),
           div(s(X), n__s(Y)) -> if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
             if(true(), X, Y) -> activate(X),
            if(false(), X, Y) -> activate(Y),
                         s(X) -> n__s(X)}
     POLY:
      Argument Filtering:
       pi(s) = [0], pi(if) = [], pi(div) = [], pi(false) = [], pi(geq) = [], pi(true) = [], pi(n__s) = [0], pi(activate) = 0, pi(n__0) = [], pi(minus#) = 1, pi(minus) = [], pi(0) = []
      Usable Rules:
       {}
      Interpretation:
       [n__s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {                    0() -> n__0(),
               minus(n__0(), Y) -> 0(),
        minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
                    activate(X) -> X,
               activate(n__0()) -> 0(),
              activate(n__s(X)) -> s(X),
                 geq(X, n__0()) -> true(),
           geq(n__0(), n__s(Y)) -> false(),
          geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
              div(0(), n__s(Y)) -> 0(),
             div(s(X), n__s(Y)) -> if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()),
               if(true(), X, Y) -> activate(X),
              if(false(), X, Y) -> activate(Y),
                           s(X) -> n__s(X)}
      Qed