YES Problem: f(f(g(g(x)))) -> f(a()) g(a()) -> a() f(a()) -> a() f(f(f(x))) -> a() f(f(a())) -> a() Proof: AT confluence processor Complete TRS T' of input TRS: f(f(g(g(x)))) -> f(a()) g(a()) -> a() f(a()) -> a() f(f(f(x))) -> a() f(f(a())) -> a() T' = (P union S) with TRS P: TRS S:f(f(g(g(x)))) -> f(a()) g(a()) -> a() f(a()) -> a() f(f(f(x))) -> a() f(f(a())) -> a() S is linear and P is reversible. CP(S,S) = f(f(a())) = a(), f(f(f(a()))) = a(), f(f(g(a()))) = f(a()), f(a()) = a() CP(S,P union P^-1) = CP(P union P^-1,S) = We have to check termination of S: Matrix Interpretation Processor: dim=1 interpretation: [f](x0) = x0 + 2, [g](x0) = 2x0 + 6, [a] = 0 orientation: f(f(g(g(x)))) = 4x + 22 >= 2 = f(a()) g(a()) = 6 >= 0 = a() f(a()) = 2 >= 0 = a() f(f(f(x))) = x + 6 >= 0 = a() f(f(a())) = 4 >= 0 = a() problem: Qed