0.00/0.48	NO
0.00/0.48	
0.00/0.48	Problem:
0.00/0.48	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	imult(0()) -> tp2(0(), y)
0.00/0.48	imult(0()) -> tp2(x, 0())
0.00/0.48	imult(s(z)) -> tp2(s(x), s(y)) <= iadd(z) = tp2(w, y), imult(w) = tp2(x, s(y))
0.00/0.48	
0.00/0.48	Proof:
0.00/0.48	This system is not confluent.
0.00/0.48	This system is oriented.
0.00/0.48	For the unconditional rule imult(0()) -> tp2(x, 0()) the variables of the right-hand side are not a subset of the variables of the left-hand side but the right-hand side is a normal form wrt R_u.
0.00/0.48	
0.00/0.49	EOF