YES
Time: 0.011060
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:
  DP:
   {  -#(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)}
  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))}
  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 (3):
    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 (1):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if](x0, x1, x2) = x0 + 1,
       
       [-](x0, x1) = x0,
       
       [lt](x0, x1) = 0,
       
       [div](x0, x1) = 0,
       
       [s](x0) = x0 + 1,
       
       [0] = 0,
       
       [false] = 1,
       
       [true] = 1,
       
       [div#](x0, x1) = x0 + 1
      Strict:
       div#(s x, s y) -> div#(-(x, y), s y)
       2 + 1x + 0y >= 1 + 1x + 0y
      Weak:
       
     Qed
   SCC (1):
    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#) = 1
     Strict:
      {}
     Qed
   SCC (1):
    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(-#) = 1
     Strict:
      {}
     Qed