YES Rewrite Rules: [ f(?x,?y) -> f(g(?x),g(?x)), g(?x) -> h(?x), F(g(?x),?x) -> F(?x,g(?x)), F(h(?x),?x) -> F(?x,h(?x)) ] Apply Direct Methods... Inner CPs: [ F(h(?x_1),?x_1) = F(?x_1,g(?x_1)) ] Outer CPs: [ ] unknown Terminating not Left-Linear, not Right-Linear unknown Gomi&Oyamaguchi&Ohta check Non-Confluence...Unknown Direct Methods: Can't judge Try Persistent Decomposition for... [ f(?x,?y) -> f(g(?x),g(?x)), g(?x) -> h(?x), F(g(?x),?x) -> F(?x,g(?x)), F(h(?x),?x) -> F(?x,h(?x)) ] Sort Assignment: F : 7*7=>16 f : 7*7=>19 g : 7=>7 h : 7=>7 maximal types: {7,16}{7,19} {7,16} (ps)Rewrite Rules: [ g(?x) -> h(?x), F(g(?x),?x) -> F(?x,g(?x)), F(h(?x),?x) -> F(?x,h(?x)) ] Apply Direct Methods... Inner CPs: [ F(h(?x),?x) = F(?x,g(?x)) ] Outer CPs: [ ] Terminating, WCR: CR {7,19} (ps)Rewrite Rules: [ f(?x,?y) -> f(g(?x),g(?x)), g(?x) -> h(?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... unknown Innermost Terminating Left-Linear, not Right-Linear Development Closed Direct Methods: CR Result by Persistent Decomposition: CR Final result: CR 2.trs: YES (12 msec.)