0.00/0.49 NO 0.00/0.49 0.00/0.49 Problem: 0.00/0.50 iquad(y) -> tp1(x) <= itwice(y) = tp1(z), itwice(z) = tp1(x) 0.00/0.50 itwice(y) -> tp1(x) <= iadd(y) = tp2(x, x) 0.00/0.50 iadd(y) -> tp2(0(), y) 0.00/0.50 iadd(s(z)) -> tp2(s(x), y) <= iadd(z) = tp2(x, y) 0.00/0.50 imult(0()) -> tp2(0(), y) 0.00/0.50 imult(0()) -> tp2(x, 0()) 0.00/0.50 imult(s(z)) -> tp2(s(x), s(y)) <= iadd(z) = tp2(w, y), imult(w) = tp2(x, s(y)) 0.00/0.50 0.00/0.50 Proof: 0.00/0.50 This system is not confluent. 0.00/0.50 This system is oriented. 0.00/0.50 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.50 0.00/0.50 EOF