MAYBE Problem: f(h(x),y) -> h(f(y,f(x,h(f(a(),a()))))) Proof: DP Processor: DPs: f#(h(x),y) -> f#(a(),a()) f#(h(x),y) -> f#(x,h(f(a(),a()))) f#(h(x),y) -> f#(y,f(x,h(f(a(),a())))) TRS: f(h(x),y) -> h(f(y,f(x,h(f(a(),a()))))) CDG Processor: DPs: f#(h(x),y) -> f#(a(),a()) f#(h(x),y) -> f#(x,h(f(a(),a()))) f#(h(x),y) -> f#(y,f(x,h(f(a(),a())))) TRS: f(h(x),y) -> h(f(y,f(x,h(f(a(),a()))))) graph: f#(h(x),y) -> f#(y,f(x,h(f(a(),a())))) -> f#(h(x),y) -> f#(a(),a()) f#(h(x),y) -> f#(y,f(x,h(f(a(),a())))) -> f#(h(x),y) -> f#(x,h(f(a(),a()))) f#(h(x),y) -> f#(y,f(x,h(f(a(),a())))) -> f#(h(x),y) -> f#(y,f(x,h(f(a(),a())))) f#(h(x),y) -> f#(x,h(f(a(),a()))) -> f#(h(x),y) -> f#(a(),a()) f#(h(x),y) -> f#(x,h(f(a(),a()))) -> f#(h(x),y) -> f#(x,h(f(a(),a()))) f#(h(x),y) -> f#(x,h(f(a(),a()))) -> f#(h(x),y) -> f#(y,f(x,h(f(a(),a())))) SCC Processor: #sccs: 1 #rules: 2 #arcs: 6/9 DPs: f#(h(x),y) -> f#(y,f(x,h(f(a(),a())))) f#(h(x),y) -> f#(x,h(f(a(),a()))) TRS: f(h(x),y) -> h(f(y,f(x,h(f(a(),a()))))) Open