(VAR X Y) (RULES f(X) -> if(X,c,f(true)) if(true,X,Y) -> X if(false,X,Y) -> Y )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend