(VAR X) (RULES c(b(a(X))) -> a(a(b(b(c(c(X)))))) a(X) -> e b(X) -> e c(X) -> e )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend