REC-SPEC OddEven SORTS Nat Bool OPS true : -> Bool false : -> Bool 0 : -> Nat s : Nat -> Nat odd : Nat -> Bool even : Nat -> Bool VARS N M : Nat RULES odd(0) -> false even(0) -> true odd(s(N)) -> true if even(N) -><- true even(s(N)) -> true if odd(N) -><- true odd(s(N)) -> false if even(N) -><- false even(s(N)) -> false if odd(N) -><- false END-SPEC get normal form for: odd(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))) % result: true get normal form for: odd(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))))))))) % result: false get normal form for: odd(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))))))))))))))