(STRATEGY
    INNERMOST)

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