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