(VAR x) (RULES +(1, x) -> +(+(0, 1), x) +(0, x) -> x ) (COMMENT Hirokawa and Middeldorp)
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend