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