MAYBE
MAYBE
TRS:
 {
    app(app(app(app(rec(), t), u), v), app(s(), x)) ->
  app(app(u, x), app(app(app(app(rec(), t), u), v), x)),
  app(app(app(app(rec(), t), u), v), app(lim(), f)) ->
  app(app(v, f), app(app(app(app(rectuv(), t), u), v), app(f, n()))),
            app(app(app(app(rec(), t), u), v), 0()) -> t,
         app(app(app(app(rectuv(), t), u), v), n()) ->
  app(app(app(app(rec(), t), u), v), n())
 }
 DUP: We consider a duplicating system.
  Trs:
   {
      app(app(app(app(rec(), t), u), v), app(s(), x)) ->
    app(app(u, x), app(app(app(app(rec(), t), u), v), x)),
    app(app(app(app(rec(), t), u), v), app(lim(), f)) ->
    app(app(v, f), app(app(app(app(rectuv(), t), u), v), app(f, n()))),
              app(app(app(app(rec(), t), u), v), 0()) -> t,
           app(app(app(app(rectuv(), t), u), v), n()) ->
    app(app(app(app(rec(), t), u), v), n())
   }
  Fail