0.00/0.63 MAYBE 0.00/0.63 0.00/0.63 Problem: 0.00/0.63 gcd(add(x, y), y) -> gcd(x, y) 0.00/0.63 gcd(y, add(x, y)) -> gcd(x, y) 0.00/0.63 gcd(x, 0()) -> x 0.00/0.64 gcd(0(), x) -> x 0.00/0.64 gcd(x, y) -> gcd(y, x) <= leq(y, x) = false() 0.00/0.64 add(0(), y) -> y 0.00/0.64 add(s(x), y) -> s(add(x, y)) 0.00/0.64 0.00/0.64 Proof: 0.00/0.64 ConCon could not decide confluence of the system. 0.00/0.64 \cite{ALS94}, Theorem 4.1 does not apply. 0.00/0.64 ConCon could not decide whether all 18 critical pairs are joinable or not. 0.00/0.64 CP: add(x, 0()) = gcd(x, 0()): 0.00/0.64 0.00/0.64 EOF