(VAR x y z) (RULES *(x,*(y,z)) -> *(*(x,y),z) *(x,x) -> x ) (COMMENT Example 4.8 (Idempotent Semigroup) in \cite{SK90})
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend