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)) ADG 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)) SCC Processor: #sccs: 1 #rules: 3 #arcs: 7/9 DPs: f#(c(x),y) -> f#(x,a(y)) f#(d(x),y) -> f#(x,b(y)) f#(x,a(b(y))) -> f#(c(d(x)),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)) Open