4.71/1.73	YES
4.71/1.73	
4.71/1.73	Problem:
4.71/1.73	pin(x) -> pout(g(x))
4.71/1.74	pin(x) -> pout(f(y)) <= pin(x) = pout(g(y))
4.71/1.74	
4.71/1.74	Proof:
4.71/1.74	This system is confluent.
4.71/1.74	By \cite{SMI95}, Corollary 4.7 or 5.3.
4.71/1.74	This system is oriented.
4.71/1.74	This system is of type 3 or smaller.
4.71/1.74	This system is right-stable.
4.71/1.74	This system is properly oriented.
4.71/1.74	This is an overlay system.
4.71/1.74	This system is left-linear.
4.71/1.74	All 2 critical pairs are trivial or infeasible.
4.71/1.74	CP: pout(g(x)) = pout(f(y)) <= pin(x) = pout(g(y)):
4.71/1.74	This critical pair is infeasible.
4.71/1.74	This critical pair is conditional.
4.71/1.74	This critical pair has some non-trivial conditions.
4.71/1.74	usable rules
4.71/1.74	inverse system
4.71/1.74	growing approximation
4.71/1.74	pout(g(x)) -> pin(z)
4.71/1.74	pout(f(y)) -> pin(x)
4.71/1.74	'\Sigma(pout(g(y))) \cap (->^*_R^-1)[\Sigma(REN(pin(x)))]' is empty.
4.71/1.74	CP: pout(f(x)) = pout(g(z)) <= pin(z) = pout(g(x)):
4.71/1.74	This critical pair is infeasible.
4.71/1.74	This critical pair is conditional.
4.71/1.74	This critical pair has some non-trivial conditions.
4.71/1.74	usable rules
4.71/1.74	inverse system
4.71/1.74	growing approximation
4.71/1.74	pout(g(x)) -> pin(z)
4.71/1.74	pout(f(y)) -> pin(x)
4.71/1.74	'\Sigma(pout(g(x))) \cap (->^*_R^-1)[\Sigma(REN(pin(z)))]' is empty.
4.71/1.74	
5.71/1.95	EOF