(STRATEGY
    INNERMOST)

(VAR
    u x y z)
(DATATYPES
    A = µX.< 0, zero, s(X), odd, even >)
(SIGNATURES
    check :: [A] -> A
    half :: [A] -> A
    plus :: [A x A] -> A
    times :: [A x A] -> A
    timesIter :: [A x A x A] -> A
    p :: [A] -> A
    if :: [A x A x A x A x A] -> A)
(RULES
    check(0()) -> zero()
    check(s(0())) -> odd()
    check(s(s(0()))) -> even()
    check(s(s(s(x)))) -> check(s(x))
    half(0()) -> 0()
    half(s(0())) -> 0()
    half(s(s(x))) -> s(half(x))
    plus(0(),y) -> y
    plus(s(x),y) -> s(plus(x,y))
    times(x,y) -> timesIter(x,y,0())
    timesIter(x,y,z) -> if(check(x)
                          ,x
                          ,y
                          ,z
                          ,plus(z,y))
    p(s(x)) -> x
    p(0()) -> 0()
    if(zero(),x,y,z,u) -> z
    if(odd(),x,y,z,u) ->
      timesIter(p(x),y,u)
    if(even(),x,y,z,u) ->
      plus(timesIter(half(x)
                    ,y
                    ,half(z))
          ,timesIter(half(x)
                    ,y
                    ,half(s(z)))))