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