MAYBE
Time: 0.013744
TRS:
 {       lt(x, 0()) -> false(),
       lt(0(), s x) -> true(),
       lt(s x, s y) -> lt(x, y),
         help(x, c) -> if(lt(c, x), x, c),
              fac x -> help(x, 0()),
   if(true(), x, c) -> times(s c, help(x, s c)),
  if(false(), x, c) -> s 0()}
 DP:
  DP:
   {    lt#(s x, s y) -> lt#(x, y),
          help#(x, c) -> lt#(c, x),
          help#(x, c) -> if#(lt(c, x), x, c),
               fac# x -> help#(x, 0()),
    if#(true(), x, c) -> help#(x, s c)}
  TRS:
  {       lt(x, 0()) -> false(),
        lt(0(), s x) -> true(),
        lt(s x, s y) -> lt(x, y),
          help(x, c) -> if(lt(c, x), x, c),
               fac x -> help(x, 0()),
    if(true(), x, c) -> times(s c, help(x, s c)),
   if(false(), x, c) -> s 0()}
  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#(x, c) -> lt#(c, x), lt#(s x, s y) -> lt#(x, y))
     (fac# x -> help#(x, 0()), help#(x, c) -> if#(lt(c, x), x, c))
     (fac# x -> help#(x, 0()), help#(x, c) -> lt#(c, x))
     (if#(true(), x, c) -> help#(x, s c), help#(x, c) -> lt#(c, x))
     (if#(true(), x, c) -> help#(x, s c), help#(x, c) -> if#(lt(c, x), x, c))
     (help#(x, c) -> if#(lt(c, x), x, c), if#(true(), x, c) -> help#(x, s c))
     (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))}
    STATUS:
     arrows: 0.720000
     SCCS (2):
      Scc:
       {      help#(x, c) -> if#(lt(c, x), x, c),
        if#(true(), x, c) -> help#(x, s c)}
      Scc:
       {lt#(s x, s y) -> lt#(x, y)}
      
      
      SCC (2):
       Strict:
        {      help#(x, c) -> if#(lt(c, x), x, c),
         if#(true(), x, c) -> help#(x, s c)}
       Weak:
       {       lt(x, 0()) -> false(),
             lt(0(), s x) -> true(),
             lt(s x, s y) -> lt(x, y),
               help(x, c) -> if(lt(c, x), x, c),
                    fac x -> help(x, 0()),
         if(true(), x, c) -> times(s c, help(x, s c)),
        if(false(), x, c) -> s 0()}
       Fail
      
      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(x, c) -> if(lt(c, x), x, c),
                    fac x -> help(x, 0()),
         if(true(), x, c) -> times(s c, help(x, s c)),
        if(false(), x, c) -> s 0()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [if](x0, x1, x2) = x0 + x1 + 1,
         
         [lt](x0, x1) = x0 + 1,
         
         [help](x0, x1) = x0 + 1,
         
         [times](x0, x1) = x0 + x1 + 1,
         
         [s](x0) = x0 + 1,
         
         [fac](x0) = 0,
         
         [true] = 1,
         
         [0] = 1,
         
         [false] = 0,
         
         [lt#](x0, x1) = x0 + 1
        Strict:
         lt#(s x, s y) -> lt#(x, y)
         2 + 1x + 0y >= 1 + 1x + 0y
        Weak:
         if(false(), x, c) -> s 0()
         1 + 1x + 0c >= 2
         if(true(), x, c) -> times(s c, help(x, s c))
         2 + 1x + 0c >= 4 + 0x + 2c
         fac x -> help(x, 0())
         0 + 0x >= 2 + 0x
         help(x, c) -> if(lt(c, x), x, c)
         1 + 0x + 1c >= 2 + 2x + 0c
         lt(s x, s y) -> lt(x, y)
         2 + 0x + 1y >= 1 + 0x + 1y
         lt(0(), s x) -> true()
         2 + 1x >= 1
         lt(x, 0()) -> false()
         2 + 0x >= 0
       Qed