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