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)) EDG 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)) graph: app#(app(mapbt(),f),app(leaf(),x)) -> app#(f,x) -> app#(app(mapbt(),f),app(leaf(),x)) -> app#(f,x) 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(leaf(),x)) -> app#(f,x) -> app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(app(mapbt(),f),r) app#(app(mapbt(),f),app(leaf(),x)) -> app#(f,x) -> app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(app(mapbt(),f),l) app#(app(mapbt(),f),app(leaf(),x)) -> app#(f,x) -> app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(f,x) app#(app(mapbt(),f),app(leaf(),x)) -> app#(f,x) -> app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(branch(),app(f,x)) app#(app(mapbt(),f),app(leaf(),x)) -> 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(leaf(),x)) -> 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)) app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(app(mapbt(),f),r) -> app#(app(mapbt(),f),app(leaf(),x)) -> app#(f,x) app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(app(mapbt(),f),r) -> 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),r) 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#(app(mapbt(),f),r) -> 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#(app(mapbt(),f),r) -> 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(mapbt(),f),r) -> 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(mapbt(),f),r) -> 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)) app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(app(mapbt(),f),l) -> app#(app(mapbt(),f),app(leaf(),x)) -> app#(f,x) app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(app(mapbt(),f),l) -> 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),l) -> 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#(app(mapbt(),f),l) 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#(app(mapbt(),f),l) -> 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(mapbt(),f),l) -> 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(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)) app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> app#(f,x) -> app#(app(mapbt(),f),app(leaf(),x)) -> app#(f,x) app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> 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#(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#(f,x) -> 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#(f,x) 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#(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#(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: 4 #arcs: 32/64 DPs: app#(app(mapbt(),f),app(leaf(),x)) -> app#(f,x) 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#(app(mapbt(),f),l) app#(app(mapbt(),f),app(app(app(branch(),x),l),r)) -> 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