YES af/ONE-SORTED/84.trs Input rules: [ a -> b, f(a) -> g(a), f(b) -> g(b) ] Sorts having no ground terms: Rules applicable to ground terms: [ a -> b, f(a) -> g(a), f(b) -> g(b) ] Constructor pattern: [b,f(?x_1),g(?x_1)] Defined pattern: [a] Constructor subsystem: [ f(b) -> g(b) ] Modified Constructor subsystem: [ f(b) -> g(b) ] candidate for a: [ a -> b ] Find a quasi-ordering ... order successfully found Precedence: g : Mul, f : Mul; a : Mul; b : Mul; Rules: [ a -> b, f(b) -> g(b) ] Check confluence of constructor subsystem... Check Termination... unknown Terminating, Linear, Oostrom: CR Conjectures: [ f(a) = g(a) ] STEP 0 ES: [ f(a) = g(a) ] HS: [ ] ES0: [ f(b) = g(b) ] HS0: [ ] ES1: [ ] HS1: [ ] : Success(GCR) (3 msec.) 0.02