MAYBE Problem: app(f(),a()) -> app(f(),b()) app(g(),b()) -> app(g(),a()) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) Proof: DP Processor: DPs: app#(f(),a()) -> app#(f(),b()) app#(g(),b()) -> app#(g(),a()) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(map(),fun),xs) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(cons(),app(fun,x)) app#(app(map(),fun),app(app(cons(),x),xs)) -> app#(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(fun,x) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(filter2(),app(fun,x)) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(filter2(),app(fun,x)),fun) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(fun,x)),fun),x) app#(app(filter(),fun),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(fun,x)),fun),x),xs) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(filter(),fun) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(filter(),fun),xs) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(cons(),x) app#(app(app(app(filter2(),true()),fun),x),xs) -> app#(app(cons(),x),app(app(filter(),fun),xs)) app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(filter(),fun) app#(app(app(app(filter2(),false()),fun),x),xs) -> app#(app(filter(),fun),xs) TRS: app(f(),a()) -> app(f(),b()) app(g(),b()) -> app(g(),a()) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) Open