7.03/2.45	MAYBE
7.03/2.45	
7.03/2.45	Problem:
7.03/2.45	gcd(z, y) -> gcd(x, y) <= iadd(z) = tp2(x, y)
7.03/2.45	gcd(y, z) -> gcd(x, y) <= iadd(z) = tp2(x, y)
7.03/2.45	gcd(x, 0()) -> x
7.03/2.45	gcd(0(), x) -> x
7.03/2.45	iadd(y) -> tp2(0(), y)
7.03/2.45	iadd(s(z)) -> tp2(s(x), y) <= iadd(z) = tp2(x, y)
7.03/2.45	iadd(add(x, y)) -> tp2(x, y)
7.03/2.45	
7.03/2.45	Proof:
7.03/2.45	ConCon could not decide confluence of the system.
7.03/2.45	\cite{ALS94}, Theorem 4.1 does not apply.
7.03/2.45	ConCon could not decide whether all 16 critical pairs are joinable or not.
7.03/2.45	CP: x = gcd(y, 0()) <= iadd(x) = tp2(y, 0()):
7.03/2.45	ConCon could not decide infeasibility of this critical pair.
7.03/2.45	ConCon could not decide if this system is quasi-decreasing.
7.03/2.45	\cite{O02}, p. 214, Proposition 7.2.50 does not apply.
7.03/2.45	
7.03/2.46	EOF