0.00/0.45 MAYBE 0.00/0.45 0.00/0.45 Problem: 0.00/0.45 iadd(y) -> tp2(0(), y) 0.00/0.45 iadd(s(z)) -> tp2(s(x), y) <= iadd(z) = tp2(x, y) 0.00/0.45 imult(0()) -> tp2(0(), y) 0.00/0.45 imult(0()) -> tp2(x, 0()) 0.00/0.45 imult(s(z)) -> tp2(s(x), s(y)) <= iadd(z) = tp2(w, y), imult(w) = tp2(x, s(y)) 0.00/0.45 0.00/0.45 Proof: 0.00/0.45 ConCon could not decide confluence of the system. 0.00/0.45 \cite{SMI95}, Corollary 4.7 or 5.3 do not apply. 0.00/0.45 0.00/0.46 EOF