(0) Obligation:

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

app(app(rec, h), app(g, 0)) → g
app(app(rec, h), app(g, app(s, x))) → app(app(h, x), app(app(rec, h), app(g, x)))

Q is empty.