0.00/0.50 MAYBE 0.00/0.50 0.00/0.50 Problem: 0.00/0.50 add(x, 0()) -> x 0.00/0.50 add(x, s(y)) -> z <= add(s(x), y) = z 0.00/0.50 sub(z, y) -> x <= add(x, y) = z 0.00/0.51 0.00/0.51 Proof: 0.00/0.51 ConCon could not decide confluence of the system. 0.00/0.51 0.00/0.51 EOF