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