MAYBE
MAYBE
TRS:
 {
                 app(app(app(compose(), f), g), x) -> app(g, app(f, x)),
  app(app(reverse2(), app(app(cons(), x), xs)), l) ->
  app(app(reverse2(), xs), app(app(cons(), x), l)),
                    app(app(reverse2(), nil()), l) -> l,
                                 app(reverse(), l) ->
  app(app(reverse2(), l), nil()),
                app(hd(), app(app(cons(), x), xs)) -> x,
                app(tl(), app(app(cons(), x), xs)) -> xs,
                                            last() ->
  app(app(compose(), hd()), reverse()),
                                            init() ->
  app(app(compose(), reverse()), app(app(compose(), tl()), reverse()))
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
                   app(app(app(compose(), f), g), x) -> app(g, app(f, x)),
    app(app(reverse2(), app(app(cons(), x), xs)), l) ->
    app(app(reverse2(), xs), app(app(cons(), x), l)),
                      app(app(reverse2(), nil()), l) -> l,
                                   app(reverse(), l) ->
    app(app(reverse2(), l), nil()),
                  app(hd(), app(app(cons(), x), xs)) -> x,
                  app(tl(), app(app(cons(), x), xs)) -> xs,
                                              last() ->
    app(app(compose(), hd()), reverse()),
                                              init() ->
    app(app(compose(), reverse()), app(app(compose(), tl()), reverse()))
   }
  Fail