0.56/1.13 MAYBE 0.56/1.13 0.56/1.13 Problem: 0.56/1.13 plus(0(), y) -> y 0.56/1.13 plus(s(x), y) -> plus(x, s(y)) 0.56/1.13 f(x, y) -> z <= plus(x, y) = plus(z, z') 0.56/1.13 0.56/1.13 Proof: 0.56/1.13 ConCon could not decide confluence of the system. 0.56/1.13 \cite{SMI95}, Corollary 4.7 or 5.3 do not apply. 0.56/1.13 0.56/1.14 EOF