MAYBE
Trs:
 {                  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))}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open