MAYBE
TRS:
 {          lt(x, 0()) -> false(),
         lt(0(), s(x)) -> true(),
        lt(s(x), s(y)) -> lt(x, y),
         times(0(), y) -> 0(),
        times(s(x), y) -> plus(y, times(x, y)),
          plus(0(), y) -> y,
         plus(s(x), y) -> s(plus(x, y)),
         loop(x, c, y) -> if(lt(x, c), x, c, y),
                fac(x) -> loop(x, s(0()), s(0())),
   if(true(), x, c, y) -> y,
  if(false(), x, c, y) -> loop(x, s(c), times(y, s(c)))}
 DP:
  Strict:
   {      lt#(s(x), s(y)) -> lt#(x, y),
          times#(s(x), y) -> times#(x, y),
          times#(s(x), y) -> plus#(y, times(x, y)),
           plus#(s(x), y) -> plus#(x, y),
           loop#(x, c, y) -> lt#(x, c),
           loop#(x, c, y) -> if#(lt(x, c), x, c, y),
                  fac#(x) -> loop#(x, s(0()), s(0())),
    if#(false(), x, c, y) -> times#(y, s(c)),
    if#(false(), x, c, y) -> loop#(x, s(c), times(y, s(c)))}
  Weak:
  {          lt(x, 0()) -> false(),
          lt(0(), s(x)) -> true(),
         lt(s(x), s(y)) -> lt(x, y),
          times(0(), y) -> 0(),
         times(s(x), y) -> plus(y, times(x, y)),
           plus(0(), y) -> y,
          plus(s(x), y) -> s(plus(x, y)),
          loop(x, c, y) -> if(lt(x, c), x, c, y),
                 fac(x) -> loop(x, s(0()), s(0())),
    if(true(), x, c, y) -> y,
   if(false(), x, c, y) -> loop(x, s(c), times(y, s(c)))}
  EDG:
   {(lt#(s(x), s(y)) -> lt#(x, y), lt#(s(x), s(y)) -> lt#(x, y))
    (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y))
    (times#(s(x), y) -> plus#(y, times(x, y)), plus#(s(x), y) -> plus#(x, y))
    (if#(false(), x, c, y) -> loop#(x, s(c), times(y, s(c))), loop#(x, c, y) -> if#(lt(x, c), x, c, y))
    (if#(false(), x, c, y) -> loop#(x, s(c), times(y, s(c))), loop#(x, c, y) -> lt#(x, c))
    (if#(false(), x, c, y) -> times#(y, s(c)), times#(s(x), y) -> times#(x, y))
    (if#(false(), x, c, y) -> times#(y, s(c)), times#(s(x), y) -> plus#(y, times(x, y)))
    (fac#(x) -> loop#(x, s(0()), s(0())), loop#(x, c, y) -> lt#(x, c))
    (fac#(x) -> loop#(x, s(0()), s(0())), loop#(x, c, y) -> if#(lt(x, c), x, c, y))
    (loop#(x, c, y) -> if#(lt(x, c), x, c, y), if#(false(), x, c, y) -> times#(y, s(c)))
    (loop#(x, c, y) -> if#(lt(x, c), x, c, y), if#(false(), x, c, y) -> loop#(x, s(c), times(y, s(c))))
    (times#(s(x), y) -> times#(x, y), times#(s(x), y) -> times#(x, y))
    (times#(s(x), y) -> times#(x, y), times#(s(x), y) -> plus#(y, times(x, y)))
    (loop#(x, c, y) -> lt#(x, c), lt#(s(x), s(y)) -> lt#(x, y))}
   SCCS:
    Scc:
     {       loop#(x, c, y) -> if#(lt(x, c), x, c, y),
      if#(false(), x, c, y) -> loop#(x, s(c), times(y, s(c)))}
    Scc:
     {plus#(s(x), y) -> plus#(x, y)}
    Scc:
     {times#(s(x), y) -> times#(x, y)}
    Scc:
     {lt#(s(x), s(y)) -> lt#(x, y)}
    SCC:
     Strict:
      {       loop#(x, c, y) -> if#(lt(x, c), x, c, y),
       if#(false(), x, c, y) -> loop#(x, s(c), times(y, s(c)))}
     Weak:
     {          lt(x, 0()) -> false(),
             lt(0(), s(x)) -> true(),
            lt(s(x), s(y)) -> lt(x, y),
             times(0(), y) -> 0(),
            times(s(x), y) -> plus(y, times(x, y)),
              plus(0(), y) -> y,
             plus(s(x), y) -> s(plus(x, y)),
             loop(x, c, y) -> if(lt(x, c), x, c, y),
                    fac(x) -> loop(x, s(0()), s(0())),
       if(true(), x, c, y) -> y,
      if(false(), x, c, y) -> loop(x, s(c), times(y, s(c)))}
     Fail
    SCC:
     Strict:
      {plus#(s(x), y) -> plus#(x, y)}
     Weak:
     {          lt(x, 0()) -> false(),
             lt(0(), s(x)) -> true(),
            lt(s(x), s(y)) -> lt(x, y),
             times(0(), y) -> 0(),
            times(s(x), y) -> plus(y, times(x, y)),
              plus(0(), y) -> y,
             plus(s(x), y) -> s(plus(x, y)),
             loop(x, c, y) -> if(lt(x, c), x, c, y),
                    fac(x) -> loop(x, s(0()), s(0())),
       if(true(), x, c, y) -> y,
      if(false(), x, c, y) -> loop(x, s(c), times(y, s(c)))}
     SPSC:
      Simple Projection:
       pi(plus#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {times#(s(x), y) -> times#(x, y)}
     Weak:
     {          lt(x, 0()) -> false(),
             lt(0(), s(x)) -> true(),
            lt(s(x), s(y)) -> lt(x, y),
             times(0(), y) -> 0(),
            times(s(x), y) -> plus(y, times(x, y)),
              plus(0(), y) -> y,
             plus(s(x), y) -> s(plus(x, y)),
             loop(x, c, y) -> if(lt(x, c), x, c, y),
                    fac(x) -> loop(x, s(0()), s(0())),
       if(true(), x, c, y) -> y,
      if(false(), x, c, y) -> loop(x, s(c), times(y, s(c)))}
     SPSC:
      Simple Projection:
       pi(times#) = 0
      Strict:
       {}
      Qed
    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),
             times(0(), y) -> 0(),
            times(s(x), y) -> plus(y, times(x, y)),
              plus(0(), y) -> y,
             plus(s(x), y) -> s(plus(x, y)),
             loop(x, c, y) -> if(lt(x, c), x, c, y),
                    fac(x) -> loop(x, s(0()), s(0())),
       if(true(), x, c, y) -> y,
      if(false(), x, c, y) -> loop(x, s(c), times(y, s(c)))}
     SPSC:
      Simple Projection:
       pi(lt#) = 0
      Strict:
       {}
      Qed