YES Problem: f(a(),y) -> f(y,g(y)) g(a()) -> b() g(b()) -> b() Proof: DP Processor: DPs: f#(a(),y) -> g#(y) f#(a(),y) -> f#(y,g(y)) TRS: f(a(),y) -> f(y,g(y)) g(a()) -> b() g(b()) -> b() TDG Processor: DPs: f#(a(),y) -> g#(y) f#(a(),y) -> f#(y,g(y)) TRS: f(a(),y) -> f(y,g(y)) g(a()) -> b() g(b()) -> b() graph: f#(a(),y) -> f#(y,g(y)) -> f#(a(),y) -> f#(y,g(y)) f#(a(),y) -> f#(y,g(y)) -> f#(a(),y) -> g#(y) SCC Processor: #sccs: 1 #rules: 1 #arcs: 2/4 DPs: f#(a(),y) -> f#(y,g(y)) TRS: f(a(),y) -> f(y,g(y)) g(a()) -> b() g(b()) -> b() Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = -7x0 + 1x1 + 0, [b] = 0, [g](x0) = -7x0 + 1, [f](x0, x1) = -7x0 + -1x1 + 0, [a] = 14 orientation: f#(a(),y) = 1y + 7 >= -6y + 2 = f#(y,g(y)) f(a(),y) = -1y + 7 >= -7y + 0 = f(y,g(y)) g(a()) = 7 >= 0 = b() g(b()) = 1 >= 0 = b() problem: DPs: TRS: f(a(),y) -> f(y,g(y)) g(a()) -> b() g(b()) -> b() Qed