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