0.00/0.46 MAYBE 0.00/0.46 0.00/0.46 Problem: 0.00/0.46 lte(0(), x) -> true() 0.00/0.46 lte(s(x), 0()) -> false() 0.00/0.46 lte(s(x), s(y)) -> lte(x, y) 0.00/0.46 lte(x, x) -> true() 0.00/0.46 lte(x, s(x)) -> true() 0.00/0.47 lte(x, s(y)) -> true() <= lte(x, y) = true() 0.00/0.47 lte(y, x) -> true() <= lte(x, y) = false() 0.00/0.47 lte(x, z) -> true() <= lte(x, y) = true(), lte(y, z) = 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