YES (ignored inputs)COMMENT doi:10.1006/jsco.1994.1003 [26] p. 27 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama Rewrite Rules: [ f(f(?x)) -> f(g(f(?x))) ] Apply Direct Methods... Inner CPs: [ f(f(g(f(?x)))) = f(g(f(f(?x)))) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR Combined result: CR 90.trs: Success(CR) (0 msec.)