(STRATEGY
    INNERMOST)

(VAR
    X Y)
(DATATYPES
    A = µX.< 0, 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)
(RULES
    minus(0(),Y) -> 0()
    minus(s(X),s(Y)) -> minus(X,Y)
    geq(X,0()) -> true()
    geq(0(),s(Y)) -> false()
    geq(s(X),s(Y)) -> geq(X,Y)
    div(0(),s(Y)) -> 0()
    div(s(X),s(Y)) -> if(geq(X,Y)
                        ,s(div(minus(X,Y),s(Y)))
                        ,0())
    if(true(),X,Y) -> X
    if(false(),X,Y) -> Y)