(STRATEGY
    INNERMOST)

(VAR
    X)
(DATATYPES
    A = µX.< s(X), a(X), c(X) >)
(SIGNATURES
    f :: [A x A] -> A)
(RULES
    f(s(X),X) -> f(X,a(X))
    f(X,c(X)) -> f(s(X),X)
    f(X,X) -> c(X))