(STRATEGY
    INNERMOST)

(VAR
    x)
(DATATYPES
    A = µX.< true, false, 0, s(X) >)
(SIGNATURES
    not :: [A] -> A
    evenodd :: [A x A] -> A)
(RULES
    not(true()) -> false()
    not(false()) -> true()
    evenodd(x,0()) -> not(evenodd(x
                                 ,s(0())))
    evenodd(0(),s(0())) -> false()
    evenodd(s(x),s(0())) ->
      evenodd(x,0()))