2.32/1.73 MAYBE 2.32/1.73 2.32/1.73 Problem: 2.32/1.73 lte(0(), x) -> true() 2.32/1.73 lte(s(x), 0()) -> false() 2.32/1.73 lte(s(x), s(y)) -> lte(x, y) 2.32/1.73 lte(x, x) -> true() 2.32/1.73 lte(x, s(x)) -> true() 2.32/1.73 lte(x, s(y)) -> true() <= lte(x, y) = true() 2.32/1.73 lte(y, x) -> true() <= lte(x, y) = false() 2.32/1.73 lte(x, z) -> true() <= lte(x, y) = true(), lte(y, z) = true() 2.32/1.73 2.32/1.74 Proof: 2.32/1.74 ConCon could not decide confluence of the system. 2.32/1.74 2.32/1.74 EOF