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