(STRATEGY
    INNERMOST)

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