( VAR x y ) ( RULES f (f (x, a), y) -> f (y, f(x, y)) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend