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