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