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())}
 DP:
  Strict:
   {  app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x),
      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(s(), x)) -> app#(app(app(app(rec(), t), u), v), x),
    app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f),
    app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(f, n()),
    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), app(lim(), f)) -> app#(app(app(app(rectuv(), t), u), v), app(f, n())),
    app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(app(rectuv(), t), u), v),
    app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(rectuv(), t), u),
    app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(rectuv(), t),
           app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(app(app(rec(), t), u), v), n()),
           app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(app(rec(), t), u), v),
           app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(rec(), t), u),
           app#(app(app(app(rectuv(), t), u), v), n()) -> app#(rec(), t)}
  Weak:
  {  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())}
  EDG:
   {
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(f, n()), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(rec(), t))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(f, n()), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(rec(), t), u))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(f, n()), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(app(rec(), t), u), v))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(f, n()), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(app(app(rec(), t), u), v), n()))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(rec(), t))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(rec(), t), u))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(app(rec(), t), u), v))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(app(app(rec(), t), u), v), n()))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(rectuv(), t))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(rectuv(), t), u))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(app(rectuv(), t), u), v))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(app(app(rectuv(), t), u), v), app(f, n())))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, 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), app(s(), x)) -> app#(u, x), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(f, n()))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x), app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(app(app(app(rec(), t), u), v), x))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x), 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(s(), x)) -> app#(u, x), app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(rec(), t))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(rec(), t), u))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(app(rec(), t), u), v))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(app(app(rec(), t), u), v), n()))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(rectuv(), t))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(rectuv(), t), u))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(app(rectuv(), t), u), v))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(app(app(rectuv(), t), u), v), app(f, n())))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f), 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), app(lim(), f)) -> app#(v, f), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(f, n()))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f), app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(app(app(app(rec(), t), u), v), x))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f), 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#(v, f), app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(app(app(rectuv(), t), u), v), app(f, n())), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(rec(), t))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(app(app(rectuv(), t), u), v), app(f, n())), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(rec(), t), u))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(app(app(rectuv(), t), u), v), app(f, n())), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(app(rec(), t), u), v))
    (app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(app(app(rectuv(), t), u), v), app(f, n())), app#(app(app(app(rectuv(), t), u), v), n()) -> app#(app(app(app(rec(), t), u), v), n()))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(app(app(app(rec(), t), u), v), x), app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(app(app(app(rec(), t), u), v), x), 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(s(), x)) -> app#(app(app(app(rec(), t), u), v), x), app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(app(app(app(rec(), t), u), v), x))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(app(app(app(rec(), t), u), v), x), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(app(app(app(rec(), t), u), v), x), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(f, n()))
    (app#(app(app(app(rec(), t), u), v), app(s(), 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), app(s(), x)) -> app#(app(app(app(rec(), t), u), v), x), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(app(app(rectuv(), t), u), v), app(f, n())))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(app(app(app(rec(), t), u), v), x), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(app(rectuv(), t), u), v))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(app(app(app(rec(), t), u), v), x), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(app(rectuv(), t), u))
    (app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(app(app(app(rec(), t), u), v), x), app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(rectuv(), t))
    (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), app(s(), x)) -> app#(u, 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), 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), app(s(), 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), app(lim(), f)) -> app#(v, f))
    (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), app(lim(), f)) -> app#(f, n()))
    (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), 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), 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), app(lim(), f)) -> app#(app(app(app(rectuv(), t), u), v), app(f, n())))
    (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), app(lim(), f)) -> app#(app(app(rectuv(), t), u), v))
    (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), app(lim(), f)) -> app#(app(rectuv(), t), u))
    (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), app(lim(), f)) -> app#(rectuv(), t))
    (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(rectuv(), t), u), v), n()) -> app#(app(app(app(rec(), t), u), v), n()))
    (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(rectuv(), t), u), v), n()) -> app#(app(app(rec(), t), u), v))
    (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(rectuv(), t), u), v), n()) -> app#(app(rec(), t), u))
    (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(rectuv(), t), u), v), n()) -> app#(rec(), t))
    (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(s(), x)) -> app#(u, x))
    (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(s(), x)) -> app#(app(u, x), app(app(app(app(rec(), t), u), v), x)))
    (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(s(), x)) -> app#(app(app(app(rec(), t), u), v), x))
    (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#(v, f))
    (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#(f, n()))
    (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), 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(app(app(rectuv(), t), u), v), app(f, n())))
    (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(app(rectuv(), t), u), v))
    (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(rectuv(), t), u))
    (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#(rectuv(), t))
    (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(rectuv(), t), u), v), n()) -> app#(app(app(app(rec(), t), u), v), n()))
    (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(rectuv(), t), u), v), n()) -> app#(app(app(rec(), t), u), v))
    (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(rectuv(), t), u), v), n()) -> app#(app(rec(), t), u))
    (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(rectuv(), t), u), v), n()) -> app#(rec(), t))
   }
   SCCS:
    Scc:
     {  app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x),
        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(s(), x)) -> app#(app(app(app(rec(), t), u), v), x),
      app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f),
      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())))}
    SCC:
     Strict:
      {  app#(app(app(app(rec(), t), u), v), app(s(), x)) -> app#(u, x),
         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(s(), x)) -> app#(app(app(app(rec(), t), u), v), x),
       app#(app(app(app(rec(), t), u), v), app(lim(), f)) -> app#(v, f),
       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())))}
     Weak:
     {  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