MAYBE Problem: f(x,a(b(y))) -> f(c(d(x)),y) f(c(x),y) -> f(x,a(y)) f(d(x),y) -> f(x,b(y)) Proof: DP Processor: DPs: f#(x,a(b(y))) -> f#(c(d(x)),y) f#(c(x),y) -> f#(x,a(y)) f#(d(x),y) -> f#(x,b(y)) TRS: f(x,a(b(y))) -> f(c(d(x)),y) f(c(x),y) -> f(x,a(y)) f(d(x),y) -> f(x,b(y)) EDG Processor: DPs: f#(x,a(b(y))) -> f#(c(d(x)),y) f#(c(x),y) -> f#(x,a(y)) f#(d(x),y) -> f#(x,b(y)) TRS: f(x,a(b(y))) -> f(c(d(x)),y) f(c(x),y) -> f(x,a(y)) f(d(x),y) -> f(x,b(y)) graph: f#(c(x),y) -> f#(x,a(y)) -> f#(x,a(b(y))) -> f#(c(d(x)),y) f#(c(x),y) -> f#(x,a(y)) -> f#(c(x),y) -> f#(x,a(y)) f#(c(x),y) -> f#(x,a(y)) -> f#(d(x),y) -> f#(x,b(y)) f#(d(x),y) -> f#(x,b(y)) -> f#(c(x),y) -> f#(x,a(y)) f#(d(x),y) -> f#(x,b(y)) -> f#(d(x),y) -> f#(x,b(y)) f#(x,a(b(y))) -> f#(c(d(x)),y) -> f#(x,a(b(y))) -> f#(c(d(x)),y) f#(x,a(b(y))) -> f#(c(d(x)),y) -> f#(c(x),y) -> f#(x,a(y)) Open