(VAR X Y X1 X2 X3) (RULES a__f(X) -> a__if(mark(X),c,f(true)) a__if(true,X,Y) -> mark(X) a__if(false,X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c) -> c mark(true) -> true mark(false) -> false a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) )