4.35/1.90	YES
4.35/1.90	
4.35/1.90	Proof:
4.35/1.90	This system is confluent.
4.35/1.90	By \cite{SMI95}, Corollary 4.7 or 5.3.
4.35/1.90	This system is oriented.
4.35/1.90	This system is of type 3 or smaller.
4.35/1.90	This system is right-stable.
4.35/1.90	This system is properly oriented.
4.35/1.90	This is an overlay system.
4.35/1.90	This system is left-linear.
4.35/1.90	All 2 critical pairs are trivial or infeasible.
4.35/1.90	Overlap: (rule1: g(y, a) -> d <= f(y, b) = b, rule2: g(a, z) -> c <= f(z, a) = a, pos: ε, mgu: {(y,a), (z,a)})
4.35/1.90	CP: c = d <= f(a, b) = b, f(a, a) = a
4.35/1.90	This critical pair is infeasible.
4.35/1.90	This critical pair is conditional.
4.35/1.90	This critical pair has some non-trivial conditions.
4.35/1.90	'\Sigma(f(a, b)) \cap (->^*_R)[\Sigma(REN(b))]' is empty by ETAC.
4.35/1.90	Overlap: (rule1: g(a, y) -> c <= f(y, a) = a, rule2: g(z, a) -> d <= f(z, b) = b, pos: ε, mgu: {(z,a), (y,a)})
4.35/1.90	CP: d = c <= f(a, a) = a, f(a, b) = b
4.35/1.90	This critical pair is infeasible.
4.35/1.90	This critical pair is conditional.
4.35/1.90	This critical pair has some non-trivial conditions.
4.35/1.90	'\Sigma(f(a, b)) \cap (->^*_R)[\Sigma(REN(b))]' is empty by ETAC.
4.35/1.90	
4.83/2.10	EOF