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