(STRATEGY
    INNERMOST)

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