MAYBE
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:
  Strict:
   {  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))}
  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())}
  EDG:
   {(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))
    (help#(x, c) -> if#(lt(c, x), x, c), if#(true(), x, c) -> help#(x, s(c)))
    (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) -> lt#(c, 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))}
   SCCS:
    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:
     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:
     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())}
     SPSC:
      Simple Projection:
       pi(lt#) = 0
      Strict:
       {}
      Qed