MAYBE MAYBE TRS: { app(app(app(comp(), f), g), x) -> app(f, app(g, x)), app(app(map(), f), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(twice(), f) -> app(app(comp(), f), f) } DUP: We consider a duplicating system. Trs: { app(app(app(comp(), f), g), x) -> app(f, app(g, x)), app(app(map(), f), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(twice(), f) -> app(app(comp(), f), f) } Fail