0.00/0.46 MAYBE 0.00/0.46 0.00/0.46 Problem: 0.00/0.46 gcd(z, y) -> gcd(x, y) <= iadd(z) = tp2(x, y) 0.00/0.46 gcd(y, z) -> gcd(x, y) <= iadd(z) = tp2(x, y) 0.00/0.46 gcd(x, 0()) -> x 0.00/0.46 gcd(0(), x) -> x 0.00/0.46 iadd(y) -> tp2(0(), y) 0.00/0.46 iadd(s(z)) -> tp2(s(x), y) <= iadd(z) = tp2(x, y) 0.00/0.46 iadd(add(x, y)) -> tp2(x, y) 0.00/0.46 0.00/0.46 Proof: 0.00/0.46 ConCon could not decide confluence of the system. 0.00/0.46 \cite{SMI95}, Corollary 4.7 or 5.3 do not apply. 0.00/0.46 0.00/0.47 EOF