(STRATEGY
    INNERMOST)

(VAR
    X X1 X2 X3)
(DATATYPES
    A = µX.< e, l, m, d, A, a, b, c, k, z(X, X), f(X), h(X, X), g(X, X, X) >)
(SIGNATURES
    a__a :: [] -> A
    a__b :: [] -> A
    a__c :: [] -> A
    a__k :: [] -> A
    a__d :: [] -> A
    a__A :: [] -> A
    a__h :: [A x A] -> A
    a__g :: [A x A x A] -> A
    a__f :: [A] -> A
    a__z :: [A x A] -> A
    mark :: [A] -> A)
(RULES
    a__a() -> a__c()
    a__b() -> a__c()
    a__c() -> e()
    a__k() -> l()
    a__d() -> m()
    a__a() -> a__d()
    a__b() -> a__d()
    a__c() -> l()
    a__k() -> m()
    a__A() -> a__h(a__f(a__a())
                  ,a__f(a__b()))
    a__h(X,X) -> a__g(mark(X)
                     ,mark(X)
                     ,a__f(a__k()))
    a__g(d(),X,X) -> a__A()
    a__f(X) -> a__z(mark(X),X)
    a__z(e(),X) -> mark(X)
    mark(A()) -> a__A()
    mark(a()) -> a__a()
    mark(b()) -> a__b()
    mark(c()) -> a__c()
    mark(d()) -> a__d()
    mark(k()) -> a__k()
    mark(z(X1,X2)) -> a__z(mark(X1)
                          ,X2)
    mark(f(X)) -> a__f(mark(X))
    mark(h(X1,X2)) -> a__h(mark(X1)
                          ,mark(X2))
    mark(g(X1,X2,X3)) ->
      a__g(mark(X1),mark(X2),mark(X3))
    mark(e()) -> e()
    mark(l()) -> l()
    mark(m()) -> m()
    a__A() -> A()
    a__a() -> a()
    a__b() -> b()
    a__c() -> c()
    a__d() -> d()
    a__k() -> k()
    a__z(X1,X2) -> z(X1,X2)
    a__f(X) -> f(X)
    a__h(X1,X2) -> h(X1,X2)
    a__g(X1,X2,X3) -> g(X1,X2,X3))