MAYBE
Time: 0.004670
TRS:
 {        lt(x, 0()) -> false(),
        lt(0(), s x) -> true(),
        lt(s x, s y) -> lt(x, y),
      ifa(true(), x) -> help(x, 1()),
     ifa(false(), x) -> logZeroError(),
         logarithm x -> ifa(lt(0(), x), x),
          help(x, y) -> ifb(lt(y, x), x, y),
   ifb(true(), x, y) -> help(half x, s y),
  ifb(false(), x, y) -> y,
            half 0() -> 0(),
          half s 0() -> 0(),
          half s s x -> s half x}
 DP:
  DP:
   {     lt#(s x, s y) -> lt#(x, y),
       ifa#(true(), x) -> help#(x, 1()),
          logarithm# x -> lt#(0(), x),
          logarithm# x -> ifa#(lt(0(), x), x),
           help#(x, y) -> lt#(y, x),
           help#(x, y) -> ifb#(lt(y, x), x, y),
    ifb#(true(), x, y) -> help#(half x, s y),
    ifb#(true(), x, y) -> half# x,
           half# s s x -> half# x}
  TRS:
  {        lt(x, 0()) -> false(),
         lt(0(), s x) -> true(),
         lt(s x, s y) -> lt(x, y),
       ifa(true(), x) -> help(x, 1()),
      ifa(false(), x) -> logZeroError(),
          logarithm x -> ifa(lt(0(), x), x),
           help(x, y) -> ifb(lt(y, x), x, y),
    ifb(true(), x, y) -> help(half x, s y),
   ifb(false(), x, y) -> y,
             half 0() -> 0(),
           half s 0() -> 0(),
           half s s x -> s half x}
  UR:
   {  lt(x, 0()) -> false(),
    lt(0(), s x) -> true(),
    lt(s x, s y) -> lt(x, y),
        half 0() -> 0(),
      half s 0() -> 0(),
      half s s x -> s half x,
         a(z, w) -> z,
         a(z, w) -> w}
   EDG:
    {(half# s s x -> half# x, half# s s x -> half# x)
     (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
     (help#(x, y) -> ifb#(lt(y, x), x, y), ifb#(true(), x, y) -> half# x)
     (help#(x, y) -> ifb#(lt(y, x), x, y), ifb#(true(), x, y) -> help#(half x, s y))
     (logarithm# x -> lt#(0(), x), lt#(s x, s y) -> lt#(x, y))
     (ifb#(true(), x, y) -> help#(half x, s y), help#(x, y) -> lt#(y, x))
     (ifb#(true(), x, y) -> help#(half x, s y), help#(x, y) -> ifb#(lt(y, x), x, y))
     (help#(x, y) -> lt#(y, x), lt#(s x, s y) -> lt#(x, y))
     (logarithm# x -> ifa#(lt(0(), x), x), ifa#(true(), x) -> help#(x, 1()))
     (ifa#(true(), x) -> help#(x, 1()), help#(x, y) -> lt#(y, x))
     (ifa#(true(), x) -> help#(x, 1()), help#(x, y) -> ifb#(lt(y, x), x, y))
     (ifb#(true(), x, y) -> half# x, half# s s x -> half# x)}
    EDG:
     {(half# s s x -> half# x, half# s s x -> half# x)
      (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
      (help#(x, y) -> ifb#(lt(y, x), x, y), ifb#(true(), x, y) -> half# x)
      (help#(x, y) -> ifb#(lt(y, x), x, y), ifb#(true(), x, y) -> help#(half x, s y))
      (ifb#(true(), x, y) -> help#(half x, s y), help#(x, y) -> lt#(y, x))
      (ifb#(true(), x, y) -> help#(half x, s y), help#(x, y) -> ifb#(lt(y, x), x, y))
      (help#(x, y) -> lt#(y, x), lt#(s x, s y) -> lt#(x, y))
      (logarithm# x -> ifa#(lt(0(), x), x), ifa#(true(), x) -> help#(x, 1()))
      (ifa#(true(), x) -> help#(x, 1()), help#(x, y) -> lt#(y, x))
      (ifa#(true(), x) -> help#(x, 1()), help#(x, y) -> ifb#(lt(y, x), x, y))
      (ifb#(true(), x, y) -> half# x, half# s s x -> half# x)}
     EDG:
      {(half# s s x -> half# x, half# s s x -> half# x)
       (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
       (help#(x, y) -> ifb#(lt(y, x), x, y), ifb#(true(), x, y) -> half# x)
       (help#(x, y) -> ifb#(lt(y, x), x, y), ifb#(true(), x, y) -> help#(half x, s y))
       (ifb#(true(), x, y) -> help#(half x, s y), help#(x, y) -> lt#(y, x))
       (ifb#(true(), x, y) -> help#(half x, s y), help#(x, y) -> ifb#(lt(y, x), x, y))
       (help#(x, y) -> lt#(y, x), lt#(s x, s y) -> lt#(x, y))
       (logarithm# x -> ifa#(lt(0(), x), x), ifa#(true(), x) -> help#(x, 1()))
       (ifa#(true(), x) -> help#(x, 1()), help#(x, y) -> lt#(y, x))
       (ifa#(true(), x) -> help#(x, 1()), help#(x, y) -> ifb#(lt(y, x), x, y))
       (ifb#(true(), x, y) -> half# x, half# s s x -> half# x)}
      EDG:
       {(half# s s x -> half# x, half# s s x -> half# x)
        (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
        (help#(x, y) -> ifb#(lt(y, x), x, y), ifb#(true(), x, y) -> half# x)
        (help#(x, y) -> ifb#(lt(y, x), x, y), ifb#(true(), x, y) -> help#(half x, s y))
        (ifb#(true(), x, y) -> help#(half x, s y), help#(x, y) -> lt#(y, x))
        (ifb#(true(), x, y) -> help#(half x, s y), help#(x, y) -> ifb#(lt(y, x), x, y))
        (help#(x, y) -> lt#(y, x), lt#(s x, s y) -> lt#(x, y))
        (logarithm# x -> ifa#(lt(0(), x), x), ifa#(true(), x) -> help#(x, 1()))
        (ifa#(true(), x) -> help#(x, 1()), help#(x, y) -> lt#(y, x))
        (ifa#(true(), x) -> help#(x, 1()), help#(x, y) -> ifb#(lt(y, x), x, y))
        (ifb#(true(), x, y) -> half# x, half# s s x -> half# x)}
       STATUS:
        arrows: 0.864198
        SCCS (3):
         Scc:
          {       help#(x, y) -> ifb#(lt(y, x), x, y),
           ifb#(true(), x, y) -> help#(half x, s y)}
         Scc:
          {lt#(s x, s y) -> lt#(x, y)}
         Scc:
          {half# s s x -> half# x}
         
         
         
         
         SCC (2):
          Strict:
           {       help#(x, y) -> ifb#(lt(y, x), x, y),
            ifb#(true(), x, y) -> help#(half x, s y)}
          Weak:
          {        lt(x, 0()) -> false(),
                 lt(0(), s x) -> true(),
                 lt(s x, s y) -> lt(x, y),
               ifa(true(), x) -> help(x, 1()),
              ifa(false(), x) -> logZeroError(),
                  logarithm x -> ifa(lt(0(), x), x),
                   help(x, y) -> ifb(lt(y, x), x, y),
            ifb(true(), x, y) -> help(half x, s y),
           ifb(false(), x, y) -> y,
                     half 0() -> 0(),
                   half s 0() -> 0(),
                   half s s x -> s half x}
          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),
               ifa(true(), x) -> help(x, 1()),
              ifa(false(), x) -> logZeroError(),
                  logarithm x -> ifa(lt(0(), x), x),
                   help(x, y) -> ifb(lt(y, x), x, y),
            ifb(true(), x, y) -> help(half x, s y),
           ifb(false(), x, y) -> y,
                     half 0() -> 0(),
                   half s 0() -> 0(),
                   half s s x -> s half x}
          Open
         
         SCC (1):
          Strict:
           {half# s s x -> half# x}
          Weak:
          {        lt(x, 0()) -> false(),
                 lt(0(), s x) -> true(),
                 lt(s x, s y) -> lt(x, y),
               ifa(true(), x) -> help(x, 1()),
              ifa(false(), x) -> logZeroError(),
                  logarithm x -> ifa(lt(0(), x), x),
                   help(x, y) -> ifb(lt(y, x), x, y),
            ifb(true(), x, y) -> help(half x, s y),
           ifb(false(), x, y) -> y,
                     half 0() -> 0(),
                   half s 0() -> 0(),
                   half s s x -> s half x}
          Open