MAYBE
Time: 0.000766
TRS:
 {         lt(x, 0()) -> false(),
         lt(0(), s x) -> true(),
         lt(s x, s y) -> lt(x, y),
   help(true(), x, y) -> s minus(x, s y),
  help(false(), x, y) -> 0(),
          minus(x, y) -> help(lt(y, x), x, y)}
 DP:
  DP:
   {      lt#(s x, s y) -> lt#(x, y),
    help#(true(), x, y) -> minus#(x, s y),
           minus#(x, y) -> lt#(y, x),
           minus#(x, y) -> help#(lt(y, x), x, y)}
  TRS:
  {         lt(x, 0()) -> false(),
          lt(0(), s x) -> true(),
          lt(s x, s y) -> lt(x, y),
    help(true(), x, y) -> s minus(x, s y),
   help(false(), x, y) -> 0(),
           minus(x, y) -> help(lt(y, x), x, y)}
  EDG:
   {(help#(true(), x, y) -> minus#(x, s y), minus#(x, y) -> help#(lt(y, x), x, y))
    (help#(true(), x, y) -> minus#(x, s y), minus#(x, y) -> lt#(y, x))
    (minus#(x, y) -> lt#(y, x), lt#(s x, s y) -> lt#(x, y))
    (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
    (minus#(x, y) -> help#(lt(y, x), x, y), help#(true(), x, y) -> minus#(x, s y))}
   STATUS:
    arrows: 0.687500
    SCCS (2):
     Scc:
      {help#(true(), x, y) -> minus#(x, s y),
              minus#(x, y) -> help#(lt(y, x), x, y)}
     Scc:
      {lt#(s x, s y) -> lt#(x, y)}
     
     SCC (2):
      Strict:
       {help#(true(), x, y) -> minus#(x, s y),
               minus#(x, y) -> help#(lt(y, x), x, y)}
      Weak:
      {         lt(x, 0()) -> false(),
              lt(0(), s x) -> true(),
              lt(s x, s y) -> lt(x, y),
        help(true(), x, y) -> s minus(x, s y),
       help(false(), x, y) -> 0(),
               minus(x, y) -> help(lt(y, x), x, y)}
      Open
     
     SCC (1):
      Strict:
       {lt#(s x, s y) -> lt#(x, y)}
      Weak:
      {         lt(x, 0()) -> false(),
              lt(0(), s x) -> true(),
              lt(s x, s y) -> lt(x, y),
        help(true(), x, y) -> s minus(x, s y),
       help(false(), x, y) -> 0(),
               minus(x, y) -> help(lt(y, x), x, y)}
      Open