MAYBE
Time: 0.001248
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)}
  UR:
   {  lt(x, 0()) -> false(),
    lt(0(), s x) -> true(),
    lt(s x, s y) -> lt(x, y),
         a(z, w) -> z,
         a(z, w) -> w}
   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