(VAR x y z) (RULES s1(s1(s0(s0(x)))) -> s0(s0(s0(s1(s1(s1(x)))))) ) (COMMENT Example 17 in \cite{DH95})
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend