(STRATEGY
    INNERMOST)

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