1.25/1.35	YES
1.25/1.35	
1.25/1.35	Problem:
1.25/1.35	 H(I(x)) -> K(J(x))
1.25/1.35	 J(x) -> K(J(x))
1.25/1.35	 I(x) -> I(J(x))
1.25/1.35	 J(x) -> J(K(J(x)))
1.25/1.35	
1.25/1.35	Proof:
1.25/1.35	 Qed (right-reducible TRS)
1.25/1.35	EOF