0.00/0.46 MAYBE 0.00/0.46 0.00/0.46 Problem: 0.00/0.47 lt(x, 0()) -> false() 0.00/0.47 lt(0(), s(x)) -> true() 0.00/0.47 lt(s(x), s(y)) -> lt(x, y) 0.00/0.47 m(0(), s(y)) -> 0() 0.00/0.47 m(x, 0()) -> x 0.00/0.47 m(s(x), s(y)) -> m(x, y) 0.00/0.47 gcd(x, x) -> x 0.00/0.47 gcd(s(x), 0()) -> s(x) 0.00/0.47 gcd(0(), s(y)) -> s(y) 0.00/0.47 gcd(s(x), s(y)) -> gcd(m(x, y), s(y)) <= lt(y, x) = true() 0.00/0.47 gcd(s(x), s(y)) -> gcd(s(x), m(y, x)) <= lt(x, y) = true() 0.00/0.47 0.00/0.47 Proof: 0.00/0.47 ConCon could not decide confluence of the system. 0.00/0.47 \cite{GNG13}, Theorem 9 does not apply. 0.00/0.47 0.00/0.47 EOF