(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

ap(ap(g, x), y) → y
ap(f, x) → ap(f, app(g, x))

Q is empty.