MAYBE
TRS:
 {             le(0(), y) -> true(),
            le(s(x), 0()) -> false(),
           le(s(x), s(y)) -> le(x, y),
            minus(x, 0()) -> x,
         minus(0(), s(y)) -> 0(),
        minus(s(x), s(y)) -> minus(x, y),
             plus(x, 0()) -> x,
            plus(x, s(y)) -> s(plus(x, y)),
             mod(x, s(y)) -> help(x, s(y), 0()),
           mod(s(x), 0()) -> 0(),
         help(x, s(y), c) -> if(le(c, x), x, s(y), c),
   if(true(), x, s(y), c) -> help(x, s(y), plus(c, s(y))),
  if(false(), x, s(y), c) -> minus(x, minus(c, s(y)))}
 DP:
  Strict:
   {         le#(s(x), s(y)) -> le#(x, y),
          minus#(s(x), s(y)) -> minus#(x, y),
              plus#(x, s(y)) -> plus#(x, y),
               mod#(x, s(y)) -> help#(x, s(y), 0()),
           help#(x, s(y), c) -> le#(c, x),
           help#(x, s(y), c) -> if#(le(c, x), x, s(y), c),
     if#(true(), x, s(y), c) -> plus#(c, s(y)),
     if#(true(), x, s(y), c) -> help#(x, s(y), plus(c, s(y))),
    if#(false(), x, s(y), c) -> minus#(x, minus(c, s(y))),
    if#(false(), x, s(y), c) -> minus#(c, s(y))}
  Weak:
  {             le(0(), y) -> true(),
             le(s(x), 0()) -> false(),
            le(s(x), s(y)) -> le(x, y),
             minus(x, 0()) -> x,
          minus(0(), s(y)) -> 0(),
         minus(s(x), s(y)) -> minus(x, y),
              plus(x, 0()) -> x,
             plus(x, s(y)) -> s(plus(x, y)),
              mod(x, s(y)) -> help(x, s(y), 0()),
            mod(s(x), 0()) -> 0(),
          help(x, s(y), c) -> if(le(c, x), x, s(y), c),
    if(true(), x, s(y), c) -> help(x, s(y), plus(c, s(y))),
   if(false(), x, s(y), c) -> minus(x, minus(c, s(y)))}
  EDG:
   {(if#(true(), x, s(y), c) -> plus#(c, s(y)), plus#(x, s(y)) -> plus#(x, y))
    (help#(x, s(y), c) -> if#(le(c, x), x, s(y), c), if#(false(), x, s(y), c) -> minus#(c, s(y)))
    (help#(x, s(y), c) -> if#(le(c, x), x, s(y), c), if#(false(), x, s(y), c) -> minus#(x, minus(c, s(y))))
    (help#(x, s(y), c) -> if#(le(c, x), x, s(y), c), if#(true(), x, s(y), c) -> help#(x, s(y), plus(c, s(y))))
    (help#(x, s(y), c) -> if#(le(c, x), x, s(y), c), if#(true(), x, s(y), c) -> plus#(c, s(y)))
    (help#(x, s(y), c) -> le#(c, x), le#(s(x), s(y)) -> le#(x, y))
    (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (mod#(x, s(y)) -> help#(x, s(y), 0()), help#(x, s(y), c) -> if#(le(c, x), x, s(y), c))
    (mod#(x, s(y)) -> help#(x, s(y), 0()), help#(x, s(y), c) -> le#(c, x))
    (plus#(x, s(y)) -> plus#(x, y), plus#(x, s(y)) -> plus#(x, y))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))
    (if#(true(), x, s(y), c) -> help#(x, s(y), plus(c, s(y))), help#(x, s(y), c) -> le#(c, x))
    (if#(true(), x, s(y), c) -> help#(x, s(y), plus(c, s(y))), help#(x, s(y), c) -> if#(le(c, x), x, s(y), c))
    (if#(false(), x, s(y), c) -> minus#(c, s(y)), minus#(s(x), s(y)) -> minus#(x, y))
    (if#(false(), x, s(y), c) -> minus#(x, minus(c, s(y))), minus#(s(x), s(y)) -> minus#(x, y))}
   SCCS:
    Scc:
     {      help#(x, s(y), c) -> if#(le(c, x), x, s(y), c),
      if#(true(), x, s(y), c) -> help#(x, s(y), plus(c, s(y)))}
    Scc:
     {plus#(x, s(y)) -> plus#(x, y)}
    Scc:
     {minus#(s(x), s(y)) -> minus#(x, y)}
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    SCC:
     Strict:
      {      help#(x, s(y), c) -> if#(le(c, x), x, s(y), c),
       if#(true(), x, s(y), c) -> help#(x, s(y), plus(c, s(y)))}
     Weak:
     {             le(0(), y) -> true(),
                le(s(x), 0()) -> false(),
               le(s(x), s(y)) -> le(x, y),
                minus(x, 0()) -> x,
             minus(0(), s(y)) -> 0(),
            minus(s(x), s(y)) -> minus(x, y),
                 plus(x, 0()) -> x,
                plus(x, s(y)) -> s(plus(x, y)),
                 mod(x, s(y)) -> help(x, s(y), 0()),
               mod(s(x), 0()) -> 0(),
             help(x, s(y), c) -> if(le(c, x), x, s(y), c),
       if(true(), x, s(y), c) -> help(x, s(y), plus(c, s(y))),
      if(false(), x, s(y), c) -> minus(x, minus(c, s(y)))}
     Fail
    SCC:
     Strict:
      {plus#(x, s(y)) -> plus#(x, y)}
     Weak:
     {             le(0(), y) -> true(),
                le(s(x), 0()) -> false(),
               le(s(x), s(y)) -> le(x, y),
                minus(x, 0()) -> x,
             minus(0(), s(y)) -> 0(),
            minus(s(x), s(y)) -> minus(x, y),
                 plus(x, 0()) -> x,
                plus(x, s(y)) -> s(plus(x, y)),
                 mod(x, s(y)) -> help(x, s(y), 0()),
               mod(s(x), 0()) -> 0(),
             help(x, s(y), c) -> if(le(c, x), x, s(y), c),
       if(true(), x, s(y), c) -> help(x, s(y), plus(c, s(y))),
      if(false(), x, s(y), c) -> minus(x, minus(c, s(y)))}
     SPSC:
      Simple Projection:
       pi(plus#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {minus#(s(x), s(y)) -> minus#(x, y)}
     Weak:
     {             le(0(), y) -> true(),
                le(s(x), 0()) -> false(),
               le(s(x), s(y)) -> le(x, y),
                minus(x, 0()) -> x,
             minus(0(), s(y)) -> 0(),
            minus(s(x), s(y)) -> minus(x, y),
                 plus(x, 0()) -> x,
                plus(x, s(y)) -> s(plus(x, y)),
                 mod(x, s(y)) -> help(x, s(y), 0()),
               mod(s(x), 0()) -> 0(),
             help(x, s(y), c) -> if(le(c, x), x, s(y), c),
       if(true(), x, s(y), c) -> help(x, s(y), plus(c, s(y))),
      if(false(), x, s(y), c) -> minus(x, minus(c, s(y)))}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {le#(s(x), s(y)) -> le#(x, y)}
     Weak:
     {             le(0(), y) -> true(),
                le(s(x), 0()) -> false(),
               le(s(x), s(y)) -> le(x, y),
                minus(x, 0()) -> x,
             minus(0(), s(y)) -> 0(),
            minus(s(x), s(y)) -> minus(x, y),
                 plus(x, 0()) -> x,
                plus(x, s(y)) -> s(plus(x, y)),
                 mod(x, s(y)) -> help(x, s(y), 0()),
               mod(s(x), 0()) -> 0(),
             help(x, s(y), c) -> if(le(c, x), x, s(y), c),
       if(true(), x, s(y), c) -> help(x, s(y), plus(c, s(y))),
      if(false(), x, s(y), c) -> minus(x, minus(c, s(y)))}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed