(VAR x y) (RULES f(g(x,y), f(y,y)) -> f(g(y,x), y) ) (COMMENT Example 1 in \cite{G96}. )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend