MAYBE
Time: 0.004254
TRS:
 {                 length nil() -> 0(),
              length cons(x, l) -> s length l,
                     lt(x, 0()) -> false(),
                   lt(0(), s y) -> true(),
                   lt(s x, s y) -> lt(x, y),
                     head nil() -> undefined(),
                head cons(x, l) -> x,
                     tail nil() -> nil(),
                tail cons(x, l) -> l,
          rev(x, l, accu, orig) -> if(lt(x, length orig), x, l, accu, orig),
                      reverse l -> rev(0(), l, nil(), l),
  if(false(), x, l, accu, orig) -> accu,
   if(true(), x, l, accu, orig) -> rev(s x, tail l, cons(head l, accu), orig)}
 DP:
  DP:
   {           length# cons(x, l) -> length# l,
                    lt#(s x, s y) -> lt#(x, y),
           rev#(x, l, accu, orig) -> length# orig,
           rev#(x, l, accu, orig) -> lt#(x, length orig),
           rev#(x, l, accu, orig) -> if#(lt(x, length orig), x, l, accu, orig),
                       reverse# l -> rev#(0(), l, nil(), l),
    if#(true(), x, l, accu, orig) -> head# l,
    if#(true(), x, l, accu, orig) -> tail# l,
    if#(true(), x, l, accu, orig) -> rev#(s x, tail l, cons(head l, accu), orig)}
  TRS:
  {                 length nil() -> 0(),
               length cons(x, l) -> s length l,
                      lt(x, 0()) -> false(),
                    lt(0(), s y) -> true(),
                    lt(s x, s y) -> lt(x, y),
                      head nil() -> undefined(),
                 head cons(x, l) -> x,
                      tail nil() -> nil(),
                 tail cons(x, l) -> l,
           rev(x, l, accu, orig) -> if(lt(x, length orig), x, l, accu, orig),
                       reverse l -> rev(0(), l, nil(), l),
   if(false(), x, l, accu, orig) -> accu,
    if(true(), x, l, accu, orig) -> rev(s x, tail l, cons(head l, accu), orig)}
  EDG:
   {(if#(true(), x, l, accu, orig) -> rev#(s x, tail l, cons(head l, accu), orig), rev#(x, l, accu, orig) -> if#(lt(x, length orig), x, l, accu, orig))
    (if#(true(), x, l, accu, orig) -> rev#(s x, tail l, cons(head l, accu), orig), rev#(x, l, accu, orig) -> lt#(x, length orig))
    (if#(true(), x, l, accu, orig) -> rev#(s x, tail l, cons(head l, accu), orig), rev#(x, l, accu, orig) -> length# orig)
    (reverse# l -> rev#(0(), l, nil(), l), rev#(x, l, accu, orig) -> if#(lt(x, length orig), x, l, accu, orig))
    (reverse# l -> rev#(0(), l, nil(), l), rev#(x, l, accu, orig) -> lt#(x, length orig))
    (reverse# l -> rev#(0(), l, nil(), l), rev#(x, l, accu, orig) -> length# orig)
    (rev#(x, l, accu, orig) -> length# orig, length# cons(x, l) -> length# l)
    (rev#(x, l, accu, orig) -> lt#(x, length orig), lt#(s x, s y) -> lt#(x, y))
    (rev#(x, l, accu, orig) -> if#(lt(x, length orig), x, l, accu, orig), if#(true(), x, l, accu, orig) -> head# l)
    (rev#(x, l, accu, orig) -> if#(lt(x, length orig), x, l, accu, orig), if#(true(), x, l, accu, orig) -> tail# l)
    (rev#(x, l, accu, orig) -> if#(lt(x, length orig), x, l, accu, orig), if#(true(), x, l, accu, orig) -> rev#(s x, tail l, cons(head l, accu), orig))
    (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
    (length# cons(x, l) -> length# l, length# cons(x, l) -> length# l)}
   STATUS:
    arrows: 0.839506
    SCCS (3):
     Scc:
      {       rev#(x, l, accu, orig) -> if#(lt(x, length orig), x, l, accu, orig),
       if#(true(), x, l, accu, orig) -> rev#(s x, tail l, cons(head l, accu), orig)}
     Scc:
      {lt#(s x, s y) -> lt#(x, y)}
     Scc:
      {length# cons(x, l) -> length# l}
     
     
     SCC (2):
      Strict:
       {       rev#(x, l, accu, orig) -> if#(lt(x, length orig), x, l, accu, orig),
        if#(true(), x, l, accu, orig) -> rev#(s x, tail l, cons(head l, accu), orig)}
      Weak:
      {                 length nil() -> 0(),
                   length cons(x, l) -> s length l,
                          lt(x, 0()) -> false(),
                        lt(0(), s y) -> true(),
                        lt(s x, s y) -> lt(x, y),
                          head nil() -> undefined(),
                     head cons(x, l) -> x,
                          tail nil() -> nil(),
                     tail cons(x, l) -> l,
               rev(x, l, accu, orig) -> if(lt(x, length orig), x, l, accu, orig),
                           reverse l -> rev(0(), l, nil(), l),
       if(false(), x, l, accu, orig) -> accu,
        if(true(), x, l, accu, orig) -> rev(s x, tail l, cons(head l, accu), orig)}
      Open
     
     SCC (1):
      Strict:
       {lt#(s x, s y) -> lt#(x, y)}
      Weak:
      {                 length nil() -> 0(),
                   length cons(x, l) -> s length l,
                          lt(x, 0()) -> false(),
                        lt(0(), s y) -> true(),
                        lt(s x, s y) -> lt(x, y),
                          head nil() -> undefined(),
                     head cons(x, l) -> x,
                          tail nil() -> nil(),
                     tail cons(x, l) -> l,
               rev(x, l, accu, orig) -> if(lt(x, length orig), x, l, accu, orig),
                           reverse l -> rev(0(), l, nil(), l),
       if(false(), x, l, accu, orig) -> accu,
        if(true(), x, l, accu, orig) -> rev(s x, tail l, cons(head l, accu), orig)}
      Open
     
     
     
     SCC (1):
      Strict:
       {length# cons(x, l) -> length# l}
      Weak:
      {                 length nil() -> 0(),
                   length cons(x, l) -> s length l,
                          lt(x, 0()) -> false(),
                        lt(0(), s y) -> true(),
                        lt(s x, s y) -> lt(x, y),
                          head nil() -> undefined(),
                     head cons(x, l) -> x,
                          tail nil() -> nil(),
                     tail cons(x, l) -> l,
               rev(x, l, accu, orig) -> if(lt(x, length orig), x, l, accu, orig),
                           reverse l -> rev(0(), l, nil(), l),
       if(false(), x, l, accu, orig) -> accu,
        if(true(), x, l, accu, orig) -> rev(s x, tail l, cons(head l, accu), orig)}
      Open