(STRATEGY
    INNERMOST)

(VAR
    m n u v x y)
(DATATYPES
    A = µX.< true, s(X), 0, false >)
(SIGNATURES
    f :: [A x A x A] -> A
    gt :: [A x A] -> A
    and :: [A x A] -> A
    plus :: [A x A] -> A
    double :: [A] -> A)
(RULES
    f(true(),x,y) -> f(and(gt(x,y)
                          ,gt(y,s(s(0()))))
                      ,plus(s(0()),x)
                      ,double(y))
    gt(0(),v) -> false()
    gt(s(u),0()) -> true()
    gt(s(u),s(v)) -> gt(u,v)
    and(x,true()) -> x
    and(x,false()) -> false()
    plus(n,0()) -> n
    plus(n,s(m)) -> s(plus(n,m))
    double(0()) -> 0()
    double(s(x)) -> s(s(double(x))))