MAYBE
MAYBE
TRS:
 {
                 ge(x, 0()) -> true(),
              ge(0(), s(y)) -> false(),
             ge(s(x), s(y)) -> ge(x, y),
     if(x, true(), z, c, l) -> z,
    if(x, false(), z, c, l) -> help(s(c), l, x, z),
              length(nil()) -> 0(),
         length(cons(x, y)) -> s(length(y)),
                     rev(x) ->
  if(x, eq(0(), length(x)), nil(), 0(), length(x)),
  help(c, l, cons(x, y), z) ->
  if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l),
           append(nil(), y) -> y,
      append(cons(x, y), z) -> cons(x, append(y, z))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                   ge(x, 0()) -> true(),
                ge(0(), s(y)) -> false(),
               ge(s(x), s(y)) -> ge(x, y),
       if(x, true(), z, c, l) -> z,
      if(x, false(), z, c, l) -> help(s(c), l, x, z),
                length(nil()) -> 0(),
           length(cons(x, y)) -> s(length(y)),
                       rev(x) ->
    if(x, eq(0(), length(x)), nil(), 0(), length(x)),
    help(c, l, cons(x, y), z) ->
    if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l),
             append(nil(), y) -> y,
        append(cons(x, y), z) -> cons(x, append(y, z))
   }
  Fail