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