1.01/1.10 NO 1.01/1.10 1.01/1.10 Problem: 1.01/1.10 f(g(f(x))) -> x 1.01/1.10 f(g(x)) -> g(f(x)) 1.01/1.10 1.01/1.10 Proof: 1.01/1.10 Nonconfluence Processor: 1.01/1.10 terms: g(f(f(x5))) *<- f(g(f(f(g(f(x5)))))) ->* x5 1.01/1.10 Qed 1.01/1.10 EOF