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