MAYBE

Problem:
 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))

Proof:
 DP Processor:
  DPs:
   app#(app(mapbt(),f),app(leaf(),x)) -> app#(f,x)
   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(mapbt(),f),r)
   app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(app(mapbt(),f),l)
   app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(f,x)
   app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(branch(),app(f,x))
   app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) ->
   app#(app(branch(),app(f,x)),app(app(mapbt(),f),l))
   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))
  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))
  SCC Processor:
   #sccs: 1
   #rules: 8
   #arcs: 64/64
   DPs:
    app#(app(mapbt(),f),app(leaf(),x)) -> app#(f,x)
    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(mapbt(),f),r)
    app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(app(mapbt(),f),l)
    app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(f,x)
    app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(branch(),app(f,x))
    app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) ->
    app#(app(branch(),app(f,x)),app(app(mapbt(),f),l))
    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))
   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))
   Open