(VAR x y )
(RULES 
        g(tt,x) -> g(h(f(x,x)),s(x))
        h(f(0,y)) -> tt
        f(s(x),y) -> f(x,s(y))
        
)