(GOAL COMPLEXITY)
(STARTTERM CONSTRUCTORBASED)
(VAR x x' )
(STRATEGY INNERMOST)
(RULES 
        eq0(S(x'), S(x)) -> eq0(x', x)
        eq0(S(x), 0) -> 0
        eq0(0, S(x)) -> 0
        eq0(0, 0) -> S(0)
        
)