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