(VAR X) (RULES f(X,X) -> f(a,b) b -> c ) (STRATEGY INNERMOST)
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend