(STRATEGY
    INNERMOST)

(VAR
    x y z)
(DATATYPES
    A = µX.< 0, s(X), +(X, X), true, false >)
(SIGNATURES
    - :: [A x A] -> A
    * :: [A x A] -> A
    if :: [A x A x A] -> A
    odd :: [A] -> A
    half :: [A] -> A
    pow :: [A x A] -> A
    f :: [A x A x A] -> A)
(RULES
    -(x,0()) -> x
    -(s(x),s(y)) -> -(x,y)
    *(x,0()) -> 0()
    *(x,s(y)) -> +(*(x,y),x)
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    odd(0()) -> false()
    odd(s(0())) -> true()
    odd(s(s(x))) -> odd(x)
    half(0()) -> 0()
    half(s(0())) -> 0()
    half(s(s(x))) -> s(half(x))
    if(true(),x,y) -> true()
    if(false(),x,y) -> false()
    pow(x,y) -> f(x,y,s(0()))
    f(x,0(),z) -> z
    f(x,s(y),z) -> if(odd(s(y))
                     ,f(x,y,*(x,z))
                     ,f(*(x,x),half(s(y)),z)))