(COMMENT 

  Claude Marché

  Factorial, hard version

)

(VAR y  x)
(RULES

+(x,0) -> x 
+(x,s(y)) -> s(+(x,y)) 
*(x,0) -> 0 
*(x,s(y)) -> +(*(x,y),x) 
ge(x,0) -> true 
ge(0,s(y)) -> false 
ge(s(x),s(y)) -> ge(x,y) 
-(x,0) -> x 
-(s(x),s(y)) -> -(x,y) 
fact(x) -> iffact(x,ge(x,s(s(0)))) 
iffact(x,true) -> *(x,fact(-(x,s(0)))) 
iffact(x,false) -> s(0) 

)