(VAR x y ) (RULES a -> a' h(x,a',y) -> h(x,y,y) h(x,y,a') -> h(x,y,y) g -> f h(f,a,a) -> h(g,a,a) h(g,a,a) -> h(f,a,a) h(f,a',a) -> h(g,a,a) h(g,a',a) -> h(f,a,a) h(f,a,a') -> h(g,a,a) h(g,a,a') -> h(f,a,a) h(f,a',a) -> h(f,a,a) h(f,a',a') -> h(g,a,a) h(g,a',a') -> h(f,a,a) h(f,a,a') -> h(f,a,a) h(f,a',a') -> h(f,a,a) )