(STRATEGY
    INNERMOST)

(VAR
    X X1 X2 X3 Y)
(DATATYPES
    A = µX.< mark(X), c, true, false, ok(X) >)
(SIGNATURES
    active :: [A] -> A
    f :: [A] -> A
    if :: [A x A x A] -> A
    proper :: [A] -> A
    top :: [A] -> A)
(RULES
    active(f(X)) -> mark(if(X
                           ,c()
                           ,f(true())))
    active(if(true(),X,Y)) ->
      mark(X)
    active(if(false(),X,Y)) ->
      mark(Y)
    active(f(X)) -> f(active(X))
    active(if(X1,X2,X3)) ->
      if(active(X1),X2,X3)
    active(if(X1,X2,X3)) -> if(X1
                              ,active(X2)
                              ,X3)
    f(mark(X)) -> mark(f(X))
    if(mark(X1),X2,X3) -> mark(if(X1
                                 ,X2
                                 ,X3))
    if(X1,mark(X2),X3) -> mark(if(X1
                                 ,X2
                                 ,X3))
    proper(f(X)) -> f(proper(X))
    proper(if(X1,X2,X3)) ->
      if(proper(X1)
        ,proper(X2)
        ,proper(X3))
    proper(c()) -> ok(c())
    proper(true()) -> ok(true())
    proper(false()) -> ok(false())
    f(ok(X)) -> ok(f(X))
    if(ok(X1),ok(X2),ok(X3)) ->
      ok(if(X1,X2,X3))
    top(mark(X)) -> top(proper(X))
    top(ok(X)) -> top(active(X)))