MAYBE
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:
  Strict:
   {          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)}
  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)}
  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))
    (length#(cons(x, l)) -> length#(l), length#(cons(x, l)) -> length#(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))
    (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) -> head#(l))
    (rev#(x, l, accu, orig) -> lt#(x, length(orig)), lt#(s(x), s(y)) -> lt#(x, y))
    (reverse#(l) -> rev#(0(), l, nil(), l), rev#(x, l, accu, orig) -> length#(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) -> if#(lt(x, length(orig)), x, l, accu, orig))
    (lt#(s(x), s(y)) -> lt#(x, y), lt#(s(x), s(y)) -> lt#(x, y))
    (rev#(x, l, accu, orig) -> length#(orig), length#(cons(x, l)) -> length#(l))}
   SCCS:
    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:
     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)}
     Fail
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(lt#) = 0
      Strict:
       {}
      Qed
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(length#) = 0
      Strict:
       {}
      Qed