YES
TRS:
 {        -(x, 0()) -> x,
       -(0(), s(y)) -> 0(),
      -(s(x), s(y)) -> -(x, y),
         lt(x, 0()) -> false(),
      lt(0(), s(y)) -> true(),
     lt(s(x), s(y)) -> lt(x, y),
  if(false(), x, y) -> y,
   if(true(), x, y) -> x,
        div(x, 0()) -> 0(),
        div(0(), y) -> 0(),
    div(s(x), s(y)) -> if(lt(x, y), 0(), s(div(-(x, y), s(y))))}
 DP:
  Strict:
   {  -#(s(x), s(y)) -> -#(x, y),
     lt#(s(x), s(y)) -> lt#(x, y),
    div#(s(x), s(y)) -> -#(x, y),
    div#(s(x), s(y)) -> lt#(x, y),
    div#(s(x), s(y)) -> if#(lt(x, y), 0(), s(div(-(x, y), s(y)))),
    div#(s(x), s(y)) -> div#(-(x, y), s(y))}
  Weak:
  {        -(x, 0()) -> x,
        -(0(), s(y)) -> 0(),
       -(s(x), s(y)) -> -(x, y),
          lt(x, 0()) -> false(),
       lt(0(), s(y)) -> true(),
      lt(s(x), s(y)) -> lt(x, y),
   if(false(), x, y) -> y,
    if(true(), x, y) -> x,
         div(x, 0()) -> 0(),
         div(0(), y) -> 0(),
     div(s(x), s(y)) -> if(lt(x, y), 0(), s(div(-(x, y), s(y))))}
  EDG:
   {(lt#(s(x), s(y)) -> lt#(x, y), lt#(s(x), s(y)) -> lt#(x, y))
    (div#(s(x), s(y)) -> lt#(x, y), lt#(s(x), s(y)) -> lt#(x, y))
    (div#(s(x), s(y)) -> div#(-(x, y), s(y)), div#(s(x), s(y)) -> -#(x, y))
    (div#(s(x), s(y)) -> div#(-(x, y), s(y)), div#(s(x), s(y)) -> lt#(x, y))
    (div#(s(x), s(y)) -> div#(-(x, y), s(y)), div#(s(x), s(y)) -> if#(lt(x, y), 0(), s(div(-(x, y), s(y)))))
    (div#(s(x), s(y)) -> div#(-(x, y), s(y)), div#(s(x), s(y)) -> div#(-(x, y), s(y)))
    (div#(s(x), s(y)) -> -#(x, y), -#(s(x), s(y)) -> -#(x, y))
    (-#(s(x), s(y)) -> -#(x, y), -#(s(x), s(y)) -> -#(x, y))}
   SCCS:
    Scc:
     {div#(s(x), s(y)) -> div#(-(x, y), s(y))}
    Scc:
     {lt#(s(x), s(y)) -> lt#(x, y)}
    Scc:
     {-#(s(x), s(y)) -> -#(x, y)}
    SCC:
     Strict:
      {div#(s(x), s(y)) -> div#(-(x, y), s(y))}
     Weak:
     {        -(x, 0()) -> x,
           -(0(), s(y)) -> 0(),
          -(s(x), s(y)) -> -(x, y),
             lt(x, 0()) -> false(),
          lt(0(), s(y)) -> true(),
         lt(s(x), s(y)) -> lt(x, y),
      if(false(), x, y) -> y,
       if(true(), x, y) -> x,
            div(x, 0()) -> 0(),
            div(0(), y) -> 0(),
        div(s(x), s(y)) -> if(lt(x, y), 0(), s(div(-(x, y), s(y))))}
     POLY:
      Argument Filtering:
       pi(div#) = 0, pi(div) = [], pi(if) = [], pi(true) = [], pi(lt) = [], pi(false) = [], pi(s) = [0], pi(0) = [], pi(-) = 0
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {        -(x, 0()) -> x,
             -(0(), s(y)) -> 0(),
            -(s(x), s(y)) -> -(x, y),
               lt(x, 0()) -> false(),
            lt(0(), s(y)) -> true(),
           lt(s(x), s(y)) -> lt(x, y),
        if(false(), x, y) -> y,
         if(true(), x, y) -> x,
              div(x, 0()) -> 0(),
              div(0(), y) -> 0(),
          div(s(x), s(y)) -> if(lt(x, y), 0(), s(div(-(x, y), s(y))))}
      Qed
    SCC:
     Strict:
      {lt#(s(x), s(y)) -> lt#(x, y)}
     Weak:
     {        -(x, 0()) -> x,
           -(0(), s(y)) -> 0(),
          -(s(x), s(y)) -> -(x, y),
             lt(x, 0()) -> false(),
          lt(0(), s(y)) -> true(),
         lt(s(x), s(y)) -> lt(x, y),
      if(false(), x, y) -> y,
       if(true(), x, y) -> x,
            div(x, 0()) -> 0(),
            div(0(), y) -> 0(),
        div(s(x), s(y)) -> if(lt(x, y), 0(), s(div(-(x, y), s(y))))}
     SPSC:
      Simple Projection:
       pi(lt#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {-#(s(x), s(y)) -> -#(x, y)}
     Weak:
     {        -(x, 0()) -> x,
           -(0(), s(y)) -> 0(),
          -(s(x), s(y)) -> -(x, y),
             lt(x, 0()) -> false(),
          lt(0(), s(y)) -> true(),
         lt(s(x), s(y)) -> lt(x, y),
      if(false(), x, y) -> y,
       if(true(), x, y) -> x,
            div(x, 0()) -> 0(),
            div(0(), y) -> 0(),
        div(s(x), s(y)) -> if(lt(x, y), 0(), s(div(-(x, y), s(y))))}
     SPSC:
      Simple Projection:
       pi(-#) = 0
      Strict:
       {}
      Qed