(VAR x y z) (RULES *(x,+(y,z)) -> +(*(x,y),*(x,z)) ) (COMMENT Example 18 in \cite{D33})
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend