MAYBE
TRS:
 {                    minus(x, x) -> 0(),
                    minus(x, 0()) -> x,
                    minus(0(), x) -> 0(),
                minus(s(x), s(y)) -> minus(x, y),
                       le(0(), y) -> true(),
                    le(s(x), 0()) -> false(),
                   le(s(x), s(y)) -> le(x, y),
         if_quot(x, y, true(), z) -> divByZeroError(),
   if_quot(x, y, false(), true()) -> s(quot(x, y)),
  if_quot(x, y, false(), false()) -> 0(),
                       quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))}
 DP:
  Strict:
   {             minus#(s(x), s(y)) -> minus#(x, y),
                    le#(s(x), s(y)) -> le#(x, y),
    if_quot#(x, y, false(), true()) -> quot#(x, y),
                        quot#(x, y) -> minus#(x, y),
                        quot#(x, y) -> le#(y, x),
                        quot#(x, y) -> le#(y, 0()),
                        quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x))}
  Weak:
  {                    minus(x, x) -> 0(),
                     minus(x, 0()) -> x,
                     minus(0(), x) -> 0(),
                 minus(s(x), s(y)) -> minus(x, y),
                        le(0(), y) -> true(),
                     le(s(x), 0()) -> false(),
                    le(s(x), s(y)) -> le(x, y),
          if_quot(x, y, true(), z) -> divByZeroError(),
    if_quot(x, y, false(), true()) -> s(quot(x, y)),
   if_quot(x, y, false(), false()) -> 0(),
                        quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))}
  EDG:
   {(minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x)))
    (if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> le#(y, 0()))
    (if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> le#(y, x))
    (if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> minus#(x, y))
    (quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x)), if_quot#(x, y, false(), true()) -> quot#(x, y))
    (quot#(x, y) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))
    (quot#(x, y) -> le#(y, x), le#(s(x), s(y)) -> le#(x, y))}
   SCCS:
    Scc:
     {if_quot#(x, y, false(), true()) -> quot#(x, y),
                          quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x))}
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    Scc:
     {minus#(s(x), s(y)) -> minus#(x, y)}
    SCC:
     Strict:
      {if_quot#(x, y, false(), true()) -> quot#(x, y),
                           quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x))}
     Weak:
     {                    minus(x, x) -> 0(),
                        minus(x, 0()) -> x,
                        minus(0(), x) -> 0(),
                    minus(s(x), s(y)) -> minus(x, y),
                           le(0(), y) -> true(),
                        le(s(x), 0()) -> false(),
                       le(s(x), s(y)) -> le(x, y),
             if_quot(x, y, true(), z) -> divByZeroError(),
       if_quot(x, y, false(), true()) -> s(quot(x, y)),
      if_quot(x, y, false(), false()) -> 0(),
                           quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))}
     Fail
    SCC:
     Strict:
      {le#(s(x), s(y)) -> le#(x, y)}
     Weak:
     {                    minus(x, x) -> 0(),
                        minus(x, 0()) -> x,
                        minus(0(), x) -> 0(),
                    minus(s(x), s(y)) -> minus(x, y),
                           le(0(), y) -> true(),
                        le(s(x), 0()) -> false(),
                       le(s(x), s(y)) -> le(x, y),
             if_quot(x, y, true(), z) -> divByZeroError(),
       if_quot(x, y, false(), true()) -> s(quot(x, y)),
      if_quot(x, y, false(), false()) -> 0(),
                           quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {minus#(s(x), s(y)) -> minus#(x, y)}
     Weak:
     {                    minus(x, x) -> 0(),
                        minus(x, 0()) -> x,
                        minus(0(), x) -> 0(),
                    minus(s(x), s(y)) -> minus(x, y),
                           le(0(), y) -> true(),
                        le(s(x), 0()) -> false(),
                       le(s(x), s(y)) -> le(x, y),
             if_quot(x, y, true(), z) -> divByZeroError(),
       if_quot(x, y, false(), true()) -> s(quot(x, y)),
      if_quot(x, y, false(), false()) -> 0(),
                           quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {}
      Qed