0.00/0.47	MAYBE
0.00/0.47	
0.00/0.47	Problem:
0.00/0.47	ihalf(0()) -> tp1(0())
0.00/0.47	ihalf(s(y)) -> tp1(s(s(x))) <= ihalf(y) = tp(x)
0.00/0.47	ihalf(half(x)) -> tp1(x)
0.00/0.47	iadd(y) -> tp2(0(), y)
0.00/0.48	iadd(s(z)) -> tp2(s(x), y) <= iadd(z) = tp2(x, y)
0.00/0.48	iadd(add(x, y)) -> tp2(x, y)
0.00/0.48	imul(0()) -> tp2(0(), y)
0.00/0.48	imul(0()) -> tp2(x, 0())
0.00/0.48	imul(s(z)) -> tp2(s(x), s(y)) <= iadd(z) = tp2(w, y), imul(w) = tp2(x, s(y))
0.00/0.48	imul(mul(x, y)) -> tp2(x, y)
0.00/0.48	imh(y) -> tp1(x) <= imul(y) = tp2(x, z), ihalf(z) = tp1(s(x))
0.00/0.48	imh(mh(x)) -> tp1(x)
0.00/0.48	
0.00/0.48	Proof:
0.00/0.48	ConCon could not decide confluence of the system.
0.00/0.48	\cite{SMI95}, Corollary 4.7 or 5.3 do not apply.
0.00/0.48	
0.00/0.48	EOF