MAYBE MAYBE TRS: { app(app(app(app(filter2(), true()), fun), x), xs) -> app(app(cons(), x), app(app(filter(), fun), xs)), app(app(app(app(filter2(), false()), fun), x), xs) -> app(app(filter(), fun), xs), app(app(app(f(), x), y), app(s(), z)) -> app(s(), app(app(app(f(), 0()), 1()), z)), app(app(app(f(), 0()), 1()), x) -> app(app(app(f(), app(s(), x)), x), x), app(app(map(), fun), app(app(cons(), x), xs)) -> app(app(cons(), app(fun, x)), app(app(map(), fun), xs)), app(app(map(), fun), nil()) -> nil(), app(app(filter(), fun), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(fun, x)), fun), x), xs), app(app(filter(), fun), nil()) -> nil() } DUP: We consider a duplicating system. Trs: { app(app(app(app(filter2(), true()), fun), x), xs) -> app(app(cons(), x), app(app(filter(), fun), xs)), app(app(app(app(filter2(), false()), fun), x), xs) -> app(app(filter(), fun), xs), app(app(app(f(), x), y), app(s(), z)) -> app(s(), app(app(app(f(), 0()), 1()), z)), app(app(app(f(), 0()), 1()), x) -> app(app(app(f(), app(s(), x)), x), x), app(app(map(), fun), app(app(cons(), x), xs)) -> app(app(cons(), app(fun, x)), app(app(map(), fun), xs)), app(app(map(), fun), nil()) -> nil(), app(app(filter(), fun), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(fun, x)), fun), x), xs), app(app(filter(), fun), nil()) -> nil() } Fail