(VAR x y )
(STRATEGY INNERMOST)
(RULES 
        -(x,0) -> x
        -(0,s(y)) -> 0
        -(s(x),s(y)) -> -(x,y)
        f(0) -> 0
        f(s(x)) -> -(s(x),g(f(x)))
        g(0) -> s(0)
        g(s(x)) -> -(s(x),f(g(x)))
        
)