MAYBE Problem: f(x,h(y)) -> h(f(f(h(a()),y),x)) Proof: DP Processor: DPs: f#(x,h(y)) -> f#(h(a()),y) f#(x,h(y)) -> f#(f(h(a()),y),x) TRS: f(x,h(y)) -> h(f(f(h(a()),y),x)) Restore Modifier: DPs: f#(x,h(y)) -> f#(h(a()),y) f#(x,h(y)) -> f#(f(h(a()),y),x) TRS: f(x,h(y)) -> h(f(f(h(a()),y),x)) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 DPs: f#(x,h(y)) -> f#(h(a()),y) f#(x,h(y)) -> f#(f(h(a()),y),x) TRS: f(x,h(y)) -> h(f(f(h(a()),y),x)) Open