(STRATEGY
    INNERMOST)

(VAR
    X Y)
(DATATYPES
    A = µX.< n__0, n__s(X), true, false >)
(SIGNATURES
    minus :: [A x A] -> A
    geq :: [A x A] -> A
    div :: [A x A] -> A
    if :: [A x A x A] -> A
    0 :: [] -> A
    s :: [A] -> A
    activate :: [A] -> A)
(RULES
    minus(n__0(),Y) -> 0()
    minus(n__s(X),n__s(Y)) ->
      minus(activate(X),activate(Y))
    geq(X,n__0()) -> true()
    geq(n__0(),n__s(Y)) -> false()
    geq(n__s(X),n__s(Y)) ->
      geq(activate(X),activate(Y))
    div(0(),n__s(Y)) -> 0()
    div(s(X),n__s(Y)) -> if(geq(X
                               ,activate(Y))
                           ,n__s(div(minus(X,activate(Y))
                                    ,n__s(activate(Y))))
                           ,n__0())
    if(true(),X,Y) -> activate(X)
    if(false(),X,Y) -> activate(Y)
    0() -> n__0()
    s(X) -> n__s(X)
    activate(n__0()) -> 0()
    activate(n__s(X)) -> s(X)
    activate(X) -> X)