(from AG01 4.34) (VAR x y) (RULES f(0) -> true f(1) -> false f(s(x)) -> f(x) if(true,x,y) -> x if(false,x,y) -> y g(s(x),s(y)) -> if(f(x),s(x),s(y)) g(x,c(y)) -> g(x,g(s(c(y)),y)))