YES Problem: f(x,y) -> x g(a()) -> h(a(),b(),a()) i(x) -> f(x,x) h(x,x,y) -> g(x) Proof: DP Processor: DPs: g#(a()) -> h#(a(),b(),a()) i#(x) -> f#(x,x) h#(x,x,y) -> g#(x) TRS: f(x,y) -> x g(a()) -> h(a(),b(),a()) i(x) -> f(x,x) h(x,x,y) -> g(x) Usable Rule Processor: DPs: g#(a()) -> h#(a(),b(),a()) i#(x) -> f#(x,x) h#(x,x,y) -> g#(x) TRS: f10(x,y) -> x f10(x,y) -> y TDG Processor: DPs: g#(a()) -> h#(a(),b(),a()) i#(x) -> f#(x,x) h#(x,x,y) -> g#(x) TRS: f10(x,y) -> x f10(x,y) -> y graph: h#(x,x,y) -> g#(x) -> g#(a()) -> h#(a(),b(),a()) g#(a()) -> h#(a(),b(),a()) -> h#(x,x,y) -> g#(x) Restore Modifier: DPs: g#(a()) -> h#(a(),b(),a()) i#(x) -> f#(x,x) h#(x,x,y) -> g#(x) TRS: f(x,y) -> x g(a()) -> h(a(),b(),a()) i(x) -> f(x,x) h(x,x,y) -> g(x) SCC Processor: #sccs: 1 #rules: 2 #arcs: 2/9 DPs: h#(x,x,y) -> g#(x) g#(a()) -> h#(a(),b(),a()) TRS: f(x,y) -> x g(a()) -> h(a(),b(),a()) i(x) -> f(x,x) h(x,x,y) -> g(x) Matrix Interpretation Processor: dimension: 1 interpretation: [h#](x0, x1, x2) = x1, [g#](x0) = x0, [i](x0) = x0, [h](x0, x1, x2) = x1, [b] = 0, [g](x0) = 0, [a] = 1, [f](x0, x1) = x0 orientation: h#(x,x,y) = x >= x = g#(x) g#(a()) = 1 >= 0 = h#(a(),b(),a()) f(x,y) = x >= x = x g(a()) = 0 >= 0 = h(a(),b(),a()) i(x) = x >= x = f(x,x) h(x,x,y) = x >= 0 = g(x) problem: DPs: h#(x,x,y) -> g#(x) TRS: f(x,y) -> x g(a()) -> h(a(),b(),a()) i(x) -> f(x,x) h(x,x,y) -> g(x) Matrix Interpretation Processor: dimension: 1 interpretation: [h#](x0, x1, x2) = 1, [g#](x0) = 0, [i](x0) = x0, [h](x0, x1, x2) = 0, [b] = 0, [g](x0) = 0, [a] = 0, [f](x0, x1) = x0 orientation: h#(x,x,y) = 1 >= 0 = g#(x) f(x,y) = x >= x = x g(a()) = 0 >= 0 = h(a(),b(),a()) i(x) = x >= x = f(x,x) h(x,x,y) = 0 >= 0 = g(x) problem: DPs: TRS: f(x,y) -> x g(a()) -> h(a(),b(),a()) i(x) -> f(x,x) h(x,x,y) -> g(x) Qed