(0) Obligation:

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

app(app(mapbt, f), app(leaf, x)) → app(leaf, app(f, x))
app(app(mapbt, f), app(app(app(branch, x), l), r)) → app(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))

Q is empty.