(STRATEGY
    INNERMOST)

(VAR
    x y z)
(DATATYPES
    A = µX.< b, c, mark(X), d, m(X), ok(X) >)
(SIGNATURES
    active :: [A] -> A
    f :: [A x A x A] -> A
    proper :: [A] -> A
    top :: [A] -> A)
(RULES
    active(f(b(),c(),x)) -> mark(f(x
                                  ,x
                                  ,x))
    active(f(x,y,z)) -> f(x
                         ,y
                         ,active(z))
    active(d()) -> m(b())
    f(x,y,mark(z)) -> mark(f(x,y,z))
    active(d()) -> mark(c())
    proper(b()) -> ok(b())
    proper(c()) -> ok(c())
    proper(d()) -> ok(d())
    proper(f(x,y,z)) -> f(proper(x)
                         ,proper(y)
                         ,proper(z))
    f(ok(x),ok(y),ok(z)) -> ok(f(x
                                ,y
                                ,z))
    top(mark(x)) -> top(proper(x))
    top(ok(x)) -> top(active(x)))