(STRATEGY
    INNERMOST)

(VAR
    x x2 y)
(DATATYPES
    A = µX.< S(X), 0 >)
(SIGNATURES
    add0 :: [A x A] -> A
    + :: [A x A] -> A)
(RULES
    add0(S(x),x2) -> +(S(0())
                      ,add0(x2,x))
    add0(0(),x2) -> x2
    +(x,S(0())) ->= S(x)
    +(S(0()),y) ->= S(y))