(VAR f x l r) (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)) )