YES Problem: f(x,y) -> g1(x,x,y) f(x,y) -> g1(y,x,x) f(x,y) -> g2(x,y,y) f(x,y) -> g2(y,y,x) g1(x,x,y) -> h(x,y) g1(y,x,x) -> h(x,y) g2(x,y,y) -> h(x,y) g2(y,y,x) -> h(x,y) h(x,x) -> x Proof: DP Processor: DPs: f#(x,y) -> g1#(x,x,y) f#(x,y) -> g1#(y,x,x) f#(x,y) -> g2#(x,y,y) f#(x,y) -> g2#(y,y,x) g1#(x,x,y) -> h#(x,y) g1#(y,x,x) -> h#(x,y) g2#(x,y,y) -> h#(x,y) g2#(y,y,x) -> h#(x,y) TRS: f(x,y) -> g1(x,x,y) f(x,y) -> g1(y,x,x) f(x,y) -> g2(x,y,y) f(x,y) -> g2(y,y,x) g1(x,x,y) -> h(x,y) g1(y,x,x) -> h(x,y) g2(x,y,y) -> h(x,y) g2(y,y,x) -> h(x,y) h(x,x) -> x Usable Rule Processor: DPs: f#(x,y) -> g1#(x,x,y) f#(x,y) -> g1#(y,x,x) f#(x,y) -> g2#(x,y,y) f#(x,y) -> g2#(y,y,x) g1#(x,x,y) -> h#(x,y) g1#(y,x,x) -> h#(x,y) g2#(x,y,y) -> h#(x,y) g2#(y,y,x) -> h#(x,y) TRS: f8(x,y) -> x f8(x,y) -> y CDG Processor: DPs: f#(x,y) -> g1#(x,x,y) f#(x,y) -> g1#(y,x,x) f#(x,y) -> g2#(x,y,y) f#(x,y) -> g2#(y,y,x) g1#(x,x,y) -> h#(x,y) g1#(y,x,x) -> h#(x,y) g2#(x,y,y) -> h#(x,y) g2#(y,y,x) -> h#(x,y) TRS: f8(x,y) -> x f8(x,y) -> y graph: f#(x,y) -> g2#(y,y,x) -> g2#(x,y,y) -> h#(x,y) f#(x,y) -> g2#(y,y,x) -> g2#(y,y,x) -> h#(x,y) f#(x,y) -> g2#(x,y,y) -> g2#(x,y,y) -> h#(x,y) f#(x,y) -> g2#(x,y,y) -> g2#(y,y,x) -> h#(x,y) f#(x,y) -> g1#(y,x,x) -> g1#(x,x,y) -> h#(x,y) f#(x,y) -> g1#(y,x,x) -> g1#(y,x,x) -> h#(x,y) f#(x,y) -> g1#(x,x,y) -> g1#(x,x,y) -> h#(x,y) f#(x,y) -> g1#(x,x,y) -> g1#(y,x,x) -> h#(x,y) Restore Modifier: DPs: f#(x,y) -> g1#(x,x,y) f#(x,y) -> g1#(y,x,x) f#(x,y) -> g2#(x,y,y) f#(x,y) -> g2#(y,y,x) g1#(x,x,y) -> h#(x,y) g1#(y,x,x) -> h#(x,y) g2#(x,y,y) -> h#(x,y) g2#(y,y,x) -> h#(x,y) TRS: f(x,y) -> g1(x,x,y) f(x,y) -> g1(y,x,x) f(x,y) -> g2(x,y,y) f(x,y) -> g2(y,y,x) g1(x,x,y) -> h(x,y) g1(y,x,x) -> h(x,y) g2(x,y,y) -> h(x,y) g2(y,y,x) -> h(x,y) h(x,x) -> x SCC Processor: #sccs: 0 #rules: 0 #arcs: 8/64