(STRATEGY
    INNERMOST)

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