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