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