(STRATEGY
    INNERMOST)

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