(VAR x) (RULES w(r(x)) -> r(w(x)) b(r(x)) -> r(b(x)) b(w(x)) -> w(b(x)) ) (COMMENT Example 7 in \cite{D33})
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend