(STRATEGY
    INNERMOST)

(VAR
    x)
(DATATYPES
    A = µX.< mark(X), no(X), X, y, c >)
(SIGNATURES
    active :: [A] -> A
    chk :: [A] -> A
    mat :: [A x A] -> A
    f :: [A] -> A
    tp :: [A] -> A)
(RULES
    active(f(x)) -> mark(f(f(x)))
    chk(no(f(x))) ->
      f(chk(mat(f(f(f(f(f(f(f(f(f(f(X()))))))))))
               ,x)))
    mat(f(x),f(y())) -> f(mat(x
                             ,y()))
    chk(no(c())) -> active(c())
    mat(f(x),c()) -> no(c())
    f(active(x)) -> active(f(x))
    f(no(x)) -> no(f(x))
    f(mark(x)) -> mark(f(x))
    tp(mark(x)) ->
      tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X()))))))))))
                ,x))))